Formalization: Graph-Adaptive Bernoulli Design for Bipartite Interference
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
Basic 36 declarations BipartiteExperiment I O bundles the known bipartite graph G_n (as the intervention neighborhoods N i = N_i(G_n)) and the fixed potential-outcome schedule Yfun i (as a function of the treatment vector, later restricted to
Environment S2 — the bipartite interference / potential-outcome world
BipartiteExperiment I O bundles the known bipartite graph G_n (as the
intervention neighborhoods N i = N_i(G_n)) and the fixed potential-outcome
schedule Yfun i (as a function of the treatment vector, later restricted to
N i by ass:bipartite-interference). The intervention index type I realizes
I_n (and m_n = card I) and the outcome index type O realizes O_n
(and n = card O).
A bipartite experiment: the known bipartite graph (via outcome-side neighborhoods) plus the fixed potential-outcome schedule.
Definition (Lean source)
All-treated potential outcome Y_i^1 = Y_i(1_{N_i}).
All-control potential outcome Y_i^0 = Y_i(0_{N_i}).
Finite-population all-treated mean μ_1 = n^{-1} ∑_i Y_i^1.
Finite-population all-control mean μ_0 = n^{-1} ∑_i Y_i^0.
Target finite-population effect τ_n = μ_1 − μ_0.
Definition (Lean source)
Potential-outcome schedule Y = ((Y_i^1, Y_i^0) : i ∈ O_n) ∈ ℝ^{2n}: the authoritative realization of the paper's fixed schedule symbol Y. Its ambient space ℝ^{2n} is carried by the pair-valued function O → ℝ × ℝ (each outcome unit i contributing the all-treated / all-control pair (Y_i^1, Y_i^0)), so the schedule's carrier O → ℝ × ℝ is (as a real vector space) ℝ^{card O} × ℝ^{card O} ≅ ℝ^{2n}.
Definition (Lean source)
All-treated exposure indicator T_i(Z) = ∏_{k∈N_i} Z_k.
Definition (Lean source)
All-control exposure indicator C_i(Z) = ∏_{k∈N_i} (1−Z_k).
All-treated exposure probability π_i^1(p) = ∏_{k∈N_i} p_k.
Definition (Lean source)
All-control exposure probability π_i^0(p) = ∏_{k∈N_i} (1−p_k).
Definition (Lean source)
Outcome-side degree d_i = |N_i(G_n)|.
Definition (Lean source)
Outcome neighborhood of an intervention unit M_k(G_n) = {i : k ∈ N_i}.
Definition (Lean source)
Intervention-side output degree s_k = |M_k(G_n)|.
Definition (Lean source)
Overlap-dependency neighbors of i: {j : S_{ij} ≠ ∅}.
Definition (Lean source)
Treated overlap load r_{ij}^1(G_n,p) = 1{S_{ij}≠∅}(∏_{k∈S_{ij}} p_k^{-1} − 1).
Definition (Lean source)
Control overlap load r_{ij}^0(G_n,p) = 1{S_{ij}≠∅}(∏_{k∈S_{ij}} (1−p_k)^{-1} − 1).
Definition (Lean source)
Cross-arm overlap load r_{ij}^{10}(G_n) = 1{S_{ij}≠∅}.
Exposure-weighted Hájek denominators (D_1, D_0) with D_1 = ∑_i T_i/π_i^1 and D_0 = ∑_i C_i/π_i^0.
Definition (Lean source)
The heterogeneous Bernoulli Hájek estimator with the explicit zero-denominator convention (each arm is 0 when its denominator vanishes).
Definition (Lean source)
First-order heterogeneous Hájek linearization η_i = (T_i/π_i^1 − 1)(Y_i^1 − μ_1) − (C_i/π_i^0 − 1)(Y_i^0 − μ_0).
Asymptotic variance scale σ²_{G_n,p}(Y) = n · Var_p(n^{-1} ∑_i η_i) under the working design D (= bernoulliDesign p by ass:independent-heterogeneous-bernoulli).
Definition (Lean source)
Probability-vector well-formedness: every coordinate of the design variable lies in the unit interval, p ∈ [0,1]^{m_n}. This pins the declared space of the design variable p — the bare carrier I → ℝ does not force the [0,1] range, and every functional of p (π_i^1, π_i^0, r_{ij}^1, r_{ij}^0) inherits its range from this constraint (the positivity floor ε ≤ p_k ≤ 1 − ε further sharpens it to the open interval (0,1)).
Definition (Lean source)
Neighborhood SUTVA: Y_i depends on the treatment vector only through its restriction to N_i(G_n).
Definition (Lean source)
The working assignment law is the independent heterogeneous Bernoulli design: D = bernoulliDesign p (each Z_k independent Bernoulli(p_k)).
Definition (Lean source)
Admissible positivity-floor domain: the global side-condition ε ∈ (0, 1/2) required by the paper's positivity floor. This pins the space of the floor symbol epsilon; without it the floor ε ≤ p_k ≤ 1 − ε fails to force p_k ∈ (0,1) and the uniform exposure-probability lower bounds ε^{d̄} > 0 are lost. Threaded into every statement that relies on strict overlap.
Definition (Lean source)
Positivity floor: ε ≤ p_k ≤ 1 − ε for every intervention unit k. Its range-pinning force for π_i^1, π_i^0, V_env, V̂_cons is only released in conjunction with EpsilonAdmissible ε (which supplies 0 < ε < 1/2).
Definition (Lean source)
Budget balance: the expected number of treated units is fixed at B_n, ∑_k p_k = B_n.
Definition (Lean source)
Admissible budget domain: B_n ∈ [m_n ε, m_n (1 − ε)]. This carries the declared space of the budget symbol B_n — BudgetBalance alone only fixes the hyperplane ∑_k p_k = B_n and leaves B_n unconstrained, whereas the feasible set is nonempty (and the constant vector B_n/m_n lies in the box [ε,1−ε]^{m_n}) exactly when B_n lies in this interval.
Definition (Lean source)
Bounded potential outcomes: |Y_i^1| ≤ 1 and |Y_i^0| ≤ 1.
Definition (Lean source)
Bounded outcome-side degree: the constant d̄ is a positive real and max_i d_i ≤ d̄.
Definition (Lean source)
Bounded overlap-dependency degree: the constant D̄ is a positive real and Δ_n ≤ D̄.
Definition (Lean source)
Nondegenerate asymptotic design variance: liminf_n σ²_n > 0, encoded as an eventual uniform positive lower bound on the variance-scale sequence.
Definition (Lean source)
Feasible heterogeneous Bernoulli designs: the probability-vector membership p ∈ [0,1]^{m_n}, the positivity floor, and the budget balance bundled over a design variable p : I → ℝ. The prob field pins the declared ambient space of the class P_{n,B_n,ε} ⊆ [0,1]^{m_n} explicitly (the bare carrier I → ℝ and PositivityFloor/BudgetBalance alone leave the [0,1] box unenforced whenever the floor ε is not itself known admissible).
Definition (Lean source)
The feasible-design class P_{n,B_n,ε} as a subset of [0,1]^{m_n} (realized over the carrier I → ℝ, with the [0,1] box pinned by the prob field of FeasibleDesign).
Definition (Lean source)
Envelope 10 declarations
Graph-only conservative variance envelope V_env = 4 n^{-1} ∑_{i,j} {r_{ij}^1 + r_{ij}^0 + 2 r_{ij}^{10}}.
Definition (Lean source)
Gradient of the normalized envelope V_env/4: g_k = n^{-1} ∑_{i,j : k∈S_{ij}} {−(∏_{ℓ∈S_{ij}} p_ℓ^{-1}) p_k^{-1} + (∏_{ℓ∈S_{ij}} (1−p_ℓ)^{-1}) (1−p_k)^{-1}}.
Definition (Lean source)
Graph-only conservative variance-scale estimator V̂_cons = V_env.
Definition (Lean source)
Observable degree-dispersion weight h_k(G_n) = n^{-1} ∑_{i,j : k∈S_{ij}} |S_{ij}|^{-1}.
Definition (Lean source)
Additive degree-dispersion surrogate objective A(p) = ∑_k h_k(G_n){p_k^{-1} + (1−p_k)^{-1}}.
Definition (Lean source)
Envelope-optimal design selector: any feasible minimizer of V_env, with a junk fallback (the homogeneous budget vector) when the argmin is empty.
Definition (Lean source)
The envelope minimum min_{p∈P} V_env(G_n,p), realized as the envelope value at the optimal design (the minimizer's value equals the minimum whenever it exists).
Definition (Lean source)
Degree-dispersion surrogate design selector: any feasible minimizer of the additive surrogate objective A, with a junk fallback when the argmin is empty.
Definition (Lean source)
Directional second-order modulus of the normalized envelope V_env/4 along a budget-feasible direction d, over the feasible set: L_d = sup_{q∈P} g_q''(0) with g_q(t) = V_env(q + t·d)/4. This realizes the observable second-order modulus L_ab used in thm:heterogeneity-separation (the paper's directional Hessian modulus sup_{q∈P} (e_b−e_a)ᵀ Hess(V_env/4)(q) (e_b−e_a) along d = e_b − e_a).
Definition (Lean source)
Observable approximation ratio α_cert = V_env(p^{deg}) / min_p V_env on the positive-minimum branch, with the no-loss convention α_cert = 1 when the envelope minimum is zero. Total and [1,∞)-valued.
Definition (Lean source)
Helpers.Denominator 3 declarations
The probability that the treated Hájek denominator is zero is bounded by the overlap-dependency and denominator-kernel bound divided by the number of outcomes.
Formal statement
Proof (Lean source)
The probability that the control Hájek denominator is zero is bounded by the overlap-dependency and denominator-kernel bound divided by the number of outcomes.
Formal statement
Proof (Lean source)
Denominator positivity (eventual sequence-level O(n⁻¹) bound). This is the note's asymptotic claim sup_{q ∈ P_{n,B_n,ε}} P_q(D_1(q,Z) = 0 ∨ D_0(q,Z) = 0) = O(n^{-1}), rendered verbatim as a Big-O statement along the paper's sequence of bipartite experiments E n: the budget sequence B n (admissible at every stage) is fixed before the constant, exactly as the note fixes B_n inside the design class P_{n,B_n,ε}; there is then a constant C ≥ 0 such that, for all sufficiently large n, every feasible design q at stage n (i.e. the supremum over the design class P_{n,B_n,ε}) satisfies P_q(D_1 = 0 ∨ D_0 = 0) ≤ C / n.
Formal statement
Proof (Lean source)
Helpers.DenominatorControl 1 declarations
The variance of the control Hájek denominator is bounded by the number of outcomes times the overlap-dependency and denominator-kernel bounds.
Formal statement
Proof (Lean source)
Helpers.DenominatorMoment 8 declarations
Uniform reciprocal-product bound for one nonempty shared-neighborhood kernel.
Definition (Lean source)
The uniform reciprocal-product bound for a shared-neighborhood kernel is nonnegative whenever the positivity floor is strictly positive.
Formal statement
Proof (Lean source)
The uniform kernel bound is decreasing in the positivity floor: for an admissible floor that is at least as large as a strictly positive reference floor, the bound at the larger floor is at most the bound at the reference floor. This lets a single bound computed at the smallest floor of interest serve uniformly over all admissible larger floors.
Formal statement
Proof (Lean source)
Under feasible floor-constrained propensities and bounded outcome degree, each treated-overlap kernel is bounded by the denominator-kernel bound.
Formal statement
Proof (Lean source)
Under feasible floor-constrained propensities and bounded outcome degree, each control-overlap kernel is bounded by the denominator-kernel bound.
Formal statement
Proof (Lean source)
The expected treated Hájek denominator equals the number of outcomes.
Formal statement
Proof (Lean source)
The expected control Hájek denominator equals the number of outcomes.
Formal statement
Proof (Lean source)
The variance of the treated Hájek denominator is bounded by the number of outcomes times the overlap-dependency and denominator-kernel bounds.
Formal statement
Proof (Lean source)
Helpers.DenominatorRate 1 declarations
If the number of outcomes diverges and the propensity floor stays eventually positive, the denominator-kernel bound divided by the number of outcomes converges to zero.
Formal statement
Proof (Lean source)
Helpers.DenominatorRatioInProb 2 declarations
The centered treated-denominator ratio D₁/card Ox − 1 vanishes in probability.
Formal statement
Proof (Lean source)
The centered control-denominator ratio D₀/card Ox − 1 vanishes in probability.
Formal statement
Proof (Lean source)
Helpers.DependencyCLT 1 declarations
Centered, uniformly bounded triangular arrays with a dependency graph of fixed maximum degree and an eventual linear variance lower bound satisfy the variance-standardized central limit theorem.
Formal statement
Proof (Lean source)
Helpers.DispersionAsymptotics 3 declarations
The number of core outcomes in the dispersion construction diverges as the construction index grows.
Formal statement
Proof (Lean source)
Eventually, a geometric lower bound controls the ratio formed by the dispersion construction's homogeneous and comparison envelope terms.
Formal statement
Proof (Lean source)
The approximation ratio of the dispersion construction diverges to infinity as the construction index grows.
Formal statement
Proof (Lean source)
Helpers.DispersionConstruction 25 declarations
The stage parameter, shifted so that every stage is nonempty.
Definition (Lean source)
The size d=t² of the growing clique.
Definition (Lean source)
Clique interventions together with 2d filler interventions.
Definition (Lean source)
d clique outcomes and t copies for each filler intervention.
Definition (Lean source)
The clique intervention block as a finset in the full intervention type.
Definition (Lean source)
Every clique intervention belongs to the clique block of the dispersion construction's intervention set.
Formal statement
Proof (Lean source)
No filler intervention belongs to the clique block of the dispersion construction's intervention set.
Formal statement
Proof (Lean source)
The clique block contains exactly as many interventions as the clique size.
Formal statement
Proof (Lean source)
The graph whose clique outcomes see every clique intervention and whose filler outcomes see their associated filler intervention only.
Definition (Lean source)
Every clique outcome is connected to the whole clique intervention block, so all clique outcomes share the same intervention neighborhood.
Formal statement
Proof (Lean source)
Every filler outcome is connected to precisely its designated filler intervention.
Formal statement
Proof (Lean source)
Every core outcome in the dispersion construction has the stated squared core-degree value.
Formal statement
Proof (Lean source)
Every filler outcome in the dispersion construction has squared degree one.
Formal statement
Proof (Lean source)
Each core intervention has the stated common exposure weight in the dispersion construction.
Formal statement
Proof (Lean source)
Each filler intervention has the stated exposure weight in the dispersion construction.
Formal statement
Proof (Lean source)
The number of core outcomes in the dispersion construction is positive.
Formal statement
Proof (Lean source)
The degree-energy of the dispersion experiment has the stated closed-form value.
Formal statement
Proof (Lean source)
The degree-energy of the dispersion experiment is strictly positive.
Formal statement
Proof (Lean source)
All interventions in the dispersion experiment have the same exposure weight.
Formal statement
Proof (Lean source)
Every intervention has strictly positive exposure weight in the dispersion experiment.
Formal statement
Proof (Lean source)
The dispersion experiment satisfies the stated bounded-outcome-degree condition.
Formal statement
Proof (Lean source)
Helpers.DispersionDesign 12 declarations
Interior homogeneous propensity used by the surrogate.
Definition (Lean source)
Filler propensity that compensates for moving clique coordinates to 1/2.
Definition (Lean source)
The homogeneous expected-treatment budget.
Definition (Lean source)
The constant propensity vector selected by the additive surrogate.
Definition (Lean source)
The feasible comparison: fair coins on the clique and compensated fillers.
Definition (Lean source)
Under an admissible positivity floor, the interior homogeneous propensity used by the surrogate lies strictly between that floor and one half, so it is an interior point of the feasible propensity range.
Formal statement
Proof (Lean source)
Under an admissible positivity floor, the compensating filler propensity likewise lies strictly between that floor and one half, so the comparison design that moves the clique coordinates to a fair coin stays interior.
Formal statement
Proof (Lean source)
The dispersion construction's homogeneous expected-treatment budget satisfies the admissibility requirements for the stated propensity floor.
Formal statement
Proof (Lean source)
The constant-propensity dispersion design is feasible for its associated budget and propensity floor.
Formal statement
Proof (Lean source)
The clique-and-filler comparison design is feasible for the same dispersion budget and propensity floor.
Formal statement
Proof (Lean source)
In the dispersion construction, the surrogate objective is a constant weight times the sum of reciprocal barriers over interventions.
Formal statement
Proof (Lean source)
The surrogate-optimal design for the dispersion construction is exactly the constant homogeneous-propensity design.
Formal statement
Proof (Lean source)
Helpers.DispersionEnvelope 6 declarations
Gives the exact variance-envelope value of the homogeneous dispersion design.
Formal statement
Proof (Lean source)
Gives the exact variance-envelope value of the clique-and-filler comparison design.
Formal statement
Proof (Lean source)
The reciprocal barrier is strictly positive for every propensity strictly between zero and one.
Formal statement
Proof (Lean source)
The minimum envelope value in the dispersion construction is strictly positive.
Formal statement
Proof (Lean source)
The dispersion approximation ratio is at least the ratio of the homogeneous design's envelope to the comparison design's envelope.
Formal statement
Proof (Lean source)
The dispersion approximation ratio admits the stated explicit lower bound.
Formal statement
Proof (Lean source)
Helpers.DispersionOptimization 6 declarations
The one-coordinate additive surrogate barrier.
Definition (Lean source)
The derivative of reciprocalBarrier at an interior point.
Definition (Lean source)
The one-coordinate reciprocal barrier lies above each of its tangent lines: at any two interior propensities, the barrier's value at the first is at least its first-order expansion around the second. This is the convexity inequality that drives the surrogate minimization.
Formal statement
Proof (Lean source)
The reciprocal barrier equals its tangent-line lower bound at the mean propensity exactly when every propensity equals that mean.
Formal statement
Proof (Lean source)
Among propensities with a fixed average, the sum of reciprocal barriers is minimized at the common mean propensity.
Formal statement
Proof (Lean source)
The common-mean propensity vector is the unique minimizer of the reciprocal-barrier sum among vectors with the same average.
Formal statement
Proof (Lean source)
Helpers.EnvelopeCalculus 19 declarations C² regularity of the floored envelope extension
C² regularity of the floored envelope extension
The floored treated-load extension is C² (it is C¹ by r1Ext_contDiff; the only input that needed strengthening is recipC, now Cⁿ for every n).
Formal statement
Proof (Lean source)
The floored control-load extension is C².
Formal statement
Proof (Lean source)
The floored envelope extension is C² on all of I → ℝ.
Formal statement
Proof (Lean source)
The NORMALIZED floored envelope extension V_env^ext / 4 is C². This is the function whose Hessian quadratic form the modulus dirModulus measures.
Formal statement
Proof (Lean source)
Directional curvature of the normalized envelope at base point q along d, i.e. Hess (V_env/4) q (d, d), computed on the globally-C² extension.
Definition (Lean source)
The curvature modulus is continuous in the base point. Combined with compactness of feasibleSet this is what makes dirModulus a genuine (bounded) supremum.
Formal statement
Proof (Lean source)
On an ε/2-ball of parameters, a line through a feasible point in a direction bounded by 1 stays in the region where recipC has saturated, so V_env and V_env^ext agree there.
Formal statement
Proof (Lean source)
The envelope line is C² on any parameter set that keeps the line inside the saturated box.
Formal statement
Proof (Lean source)
The envelope line through a feasible point is differentiable at 0.
Formal statement
Proof (Lean source)
The envelope line is differentiable at ANY parameter whose base point is feasible. Needed to feed ConvexOn.monotoneOn_deriv on the whole segment, not just at its midpoint.
Formal statement
Proof (Lean source)
The DERIVATIVE of the envelope line is itself differentiable at 0 (the line is C² there). This is the hdd hypothesis of convexOn_deriv2_nonneg.
Formal statement
Proof (Lean source)
Partial derivative of the normalized floored envelope in coordinate k, in the Pi space. This is deriv_varEnvelope_div_four_coord_line (now public in TConvexDesign) restated as an fderiv applied to the basis vector Pi.single k 1.
Formal statement
Proof (Lean source)
The directional derivative of the normalized floored envelope is the gradient-score contraction ∑ k, d k * g_k(q).
Formal statement
Proof (Lean source)
First derivative of the envelope line at 0.
Formal statement
Proof (Lean source)
Second derivative of the envelope line at 0 equals the directional curvature at the base point.
Formal statement
Proof (Lean source)
Second derivative of the envelope line at an arbitrary parameter t equals the directional curvature at the SHIFTED base point q + t·d. This is the form the EnvelopeLineC2Data curvature conjunct needs, since it quantifies over t ∈ Icc 0 T.
Formal statement
Proof (Lean source)
dirModulus is the supremum of envCurv over the feasible set: its defining body, stated with the singular V_env, agrees with envCurv at every feasible base point.
Formal statement
Proof (Lean source)
The curvature values over the feasible set are bounded above: envCurv is continuous and feasibleSet is compact. This is the BddAbove side condition of le_ciSup, and the fact whose absence stalled the original gate.
Formal statement
Proof (Lean source)
Every feasible base point's directional curvature is dominated by dirModulus.
Formal statement
Proof (Lean source)
Helpers.Kernel 4 declarations
When no relevant factor is zero, the product over a union divided by the two setwise products equals the product of inverse factors over the overlap.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the covariance of two centered treated-exposure ratios equals their treated-overlap kernel.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the covariance of two centered control-exposure ratios equals their control-overlap kernel.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the mixed treated-control centered-ratio moment equals minus the mixed overlap kernel.
Formal statement
Proof (Lean source)
Helpers.LinScoreBounds 6 declarations
Under bounded potential outcomes, the treated potential-outcome mean is bounded by one in absolute value.
Formal statement
Proof (Lean source)
Under bounded potential outcomes, the control potential-outcome mean is bounded by one in absolute value.
Formal statement
Proof (Lean source)
Each inverse treated exposure probability is bounded by one plus the denominator-kernel bound under the floor and degree conditions.
Formal statement
Proof (Lean source)
Each inverse control exposure probability is bounded by one plus the denominator-kernel bound under the floor and degree conditions.
Formal statement
Proof (Lean source)
Every linearization score is bounded in absolute value by the stated uniform denominator-kernel-based constant.
Formal statement
Proof (Lean source)
The linear-score bound only uses the probability-vector box, the positivity floor, and the outcome degree. This variant lets a stronger uniform floor ε0 control a design originally certified feasible at a possibly larger floor.
Formal statement
Proof (Lean source)
Helpers.LinScoreCLT 7 declarations
The intervention-coordinate block supporting a finite tuple of outcome-side linear scores.
Definition (Lean source)
An outcome's all-treated exposure indicator depends on the assignment vector only through the outcome's own intervention neighborhood: two assignments that agree there give the same indicator.
Formal statement
Proof (Lean source)
An outcome's all-control exposure indicator depends on the assignment vector only through the outcome's own intervention neighborhood: two assignments that agree there give the same indicator.
Formal statement
Proof (Lean source)
An outcome's linearization score depends only on the assignments in that outcome's intervention neighborhood.
Formal statement
Proof (Lean source)
If no outcome in one block is identical to or overlaps an outcome in another block, the two blocks' supporting intervention neighborhoods are disjoint.
Formal statement
Proof (Lean source)
The overlap relation is a dependency graph for linear scores under the heterogeneous Bernoulli product design.
Definition (Lean source)
The dependency-graph neighborhood of any outcome has size at most the ceiling of the overlap-dependency bound plus one.
Formal statement
Proof (Lean source)
Helpers.Linearization 7 declarations
Each outcome's Hájek linearization score has expectation zero under the heterogeneous independent Bernoulli design.
Formal statement
Proof (Lean source)
The mixed overlap kernel is symmetric in the two outcomes.
Formal statement
Proof (Lean source)
Summing the two symmetric mixed terms over all outcome pairs is equal to twice either one of them.
Formal statement
Proof (Lean source)
The joint moment of two linearization scores equals the sum of their treated, control, and mixed overlap-kernel contributions.
Formal statement
Proof (Lean source)
The variance scale is the average over all outcome pairs of the joint moments of their linearization scores.
Formal statement
Proof (Lean source)
In a double sum, symmetric mixed overlap terms can be combined into twice the one-direction mixed term.
Formal statement
Proof (Lean source)
The variance scale equals the outcome-pair average of the treated, control, and combined mixed overlap contributions.
Formal statement
Proof (Lean source)
Helpers.Moments 9 declarations
For disjoint intervention sets, the product that uses one factor on the first set and another on the second factors into the two separate products.
Formal statement
Proof (Lean source)
The product of two all-treated exposure indicators equals the all-treated indicator for the union of their intervention sets.
Formal statement
Proof (Lean source)
The product of two all-control exposure indicators equals the all-control indicator for the union of their intervention sets.
Formal statement
Proof (Lean source)
If two intervention sets overlap, their all-treated and all-control exposure indicators cannot both equal one, so their product is zero.
Formal statement
Proof (Lean source)
For disjoint sets, the product of an all-treated indicator and an all-control indicator is the indicator for that mixed assignment pattern.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the probability that all interventions in a set are treated is the product of their treatment probabilities.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the probability that all interventions in a set are controlled is the product of their control probabilities.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the expected product of two all-treated exposure indicators is the product of treatment probabilities over their union.
Formal statement
Proof (Lean source)
Under independent Bernoulli assignment, the expected product of two all-control exposure indicators is the product of control probabilities over their union.
Formal statement
Proof (Lean source)
Helpers.NumeratorMoment 8 declarations
Centered treated-arm numerator G₁(z) = ∑ᵢ (T_i(z)/π_i^1)(Y_i^1 − μ₁).
Definition (Lean source)
Centered control-arm numerator G₀(z) = ∑ᵢ (C_i(z)/π_i^0)(Y_i^0 − μ₀).
Definition (Lean source)
The treated-arm numerator has design mean zero under the Bernoulli design.
Formal statement
Proof (Lean source)
The control-arm numerator has design mean zero under the Bernoulli design.
Formal statement
Proof (Lean source)
The treated-arm numerator has design variance at most card O · (4 · D̄ · denominatorKernelBound ε d̄).
Formal statement
Proof (Lean source)
The control-arm numerator has design variance at most card O · (4 · D̄ · denominatorKernelBound ε d̄).
Formal statement
Proof (Lean source)
The √(card Ox)-scaled treated-arm numerator is bounded in probability (uniformly tight).
Formal statement
Proof (Lean source)
The √(card Ox)-scaled control-arm numerator is bounded in probability (uniformly tight).
Formal statement
Proof (Lean source)
Helpers.RatioRemainder 3 declarations
Neighborhood-SUTVA exposure identity (treated arm): T_i(z)·Y_i(z) = T_i(z)·Y_i^1, because on {T_i = 1} the treatment vector is all-treated on N_i, so Y_i(z) = Y_i^1 by interference.
Formal statement
Proof (Lean source)
Neighborhood-SUTVA exposure identity (control arm): C_i(z)·Y_i(z) = C_i(z)·Y_i^0.
Formal statement
Proof (Lean source)
Capped Hájek ratio-remainder bound. When both denominator sums are at least card O / 2 (so both Hájek arms are on their nonzero branch and card O / D_arm ≤ 2), the scaled Hájek-minus-linear-score remainder is bounded by the sum over arms of 2 · |G_arm/√(card O)| · |D_arm/card O − 1|.
Formal statement
Proof (Lean source)
Helpers.Surrogate 8 declarations
For positive factors all at least one, their arithmetic average does not exceed their product.
Formal statement
Proof (Lean source)
If removing any one nonnegative factor leaves a product bounded by a constant, the full product is bounded by that constant times the factors' average.
Formal statement
Proof (Lean source)
If every propensity is at least the design floor, the product of reciprocals after omitting one member of a set is bounded by the floor raised to minus the set size plus one.
Formal statement
Proof (Lean source)
For a nonempty set whose size is at most the degree bound, the reciprocal-power bound is no larger than the stated degree-based certificate.
Formal statement
Proof (Lean source)
The surrogate objective equals the average, over outcome pairs sharing an intervention, of the reciprocal treatment and control probabilities.
Formal statement
Proof (Lean source)
One quarter of the variance envelope equals the sum over outcome pairs of their normalized envelope kernels.
Formal statement
Proof (Lean source)
For any feasible design, the average reciprocal propensity over a pair's shared interventions is no larger than that pair's envelope kernel.
Formal statement
Proof (Lean source)
Under the degree and floor conditions, each envelope kernel is bounded by a degree-based certificate times the shared-intervention reciprocal average.
Formal statement
Proof (Lean source)
TConvexDesign 19 declarations The original envelope is singular at the coordinate hyperplanes p_k = 0 and p_k = 1.
Smooth envelope extension
The original envelope is singular at the coordinate hyperplanes p_k = 0 and p_k = 1. The cutoff
reciprocal recipC (agrees with x⁻¹ on the feasible box, globally C¹) was promoted to
Causalean.Mathlib.Analysis.SmoothReciprocal (recipC, recipC_eq_inv, recipC_contDiff, opened
via Causalean.Mathlib).
Extends the treated-overlap kernel to all propensity vectors by replacing reciprocal probabilities with a smooth cutoff reciprocal; it agrees with the original kernel away from zero.
Extends the control-overlap kernel to all propensity vectors by smoothly regularizing reciprocal control probabilities; it agrees with the original kernel away from one.
Defines a globally smooth extension of the variance envelope by combining the regularized treated and control overlap kernels.
Definition (Lean source)
When every treatment probability is at least half the cutoff, the regularized treated-overlap kernel equals the original treated kernel.
Formal statement
Proof (Lean source)
When every control probability is at least half the cutoff, the regularized control-overlap kernel equals the original control kernel.
Formal statement
Proof (Lean source)
On the interior propensity box, the smooth extended variance envelope equals the original variance envelope.
Formal statement
Proof (Lean source)
For a positive cutoff, the regularized treated-overlap kernel is continuously differentiable in all propensity coordinates.
Formal statement
Proof (Lean source)
For a positive cutoff, the regularized control-overlap kernel is continuously differentiable in all propensity coordinates.
Formal statement
Proof (Lean source)
For a positive cutoff, the smooth extended variance envelope is continuously differentiable in the propensity vector.
Formal statement
Proof (Lean source)
For a positive cutoff, the smooth extended variance envelope is differentiable in the propensity vector.
Formal statement
Proof (Lean source)
Re-expresses a propensity vector indexed by interventions as a vector in finite-dimensional Euclidean space.
Definition (Lean source)
Re-expresses a finite-dimensional Euclidean vector as a propensity vector indexed by interventions.
Definition (Lean source)
Converting a propensity vector to Euclidean coordinates and back recovers every original propensity.
Formal statement
Proof (Lean source)
Converting a Euclidean vector to a propensity vector and back recovers the original Euclidean vector.
Formal statement
Proof (Lean source)
Expresses one quarter of the smooth extended variance envelope as a function on Euclidean coordinates.
Definition (Lean source)
For a positive cutoff, the Euclidean-coordinate version of the smooth extended envelope is differentiable.
Formal statement
Proof (Lean source)
Coordinate-line derivative of the normalized envelope: the partial derivative of V_env/4 in coordinate k at a feasible p is exactly the gradient score envelopeGrad p k. Made public (was private) so the EnvelopeLineC2Data discharge in Helpers/EnvelopeCalculus can assemble the directional derivative along e_b - e_a from the two coordinate partials.
Formal statement
Proof (Lean source)
At every feasible design, the Euclidean gradient of the transported smooth envelope equals the stated envelope gradient in each intervention coordinate.
Formal statement
Proof (Lean source)
Convex design. For a feasible budget B ∈ [mε, m(1−ε)], the feasible set P_{n,B,ε} is nonempty, compact and convex, the envelope V_env is convex on it, and a minimizer exists. The multiplier/KKT certificate is kept separate because it needs a general finite-dimensional normal-cone KKT substrate theorem that is not currently available in Mathlib/Causalean.
Formal statement
Proof (Lean source)
TDispersionCertificate 1 declarations
For every admissible positivity floor, positive degree-dispersion constant, and nonvacuous weight-ratio constant, there is a sequence of finite bipartite experiments satisfying the positive-energy and first-order dispersion guards whose observable surrogate approximation ratio tends to infinity.
Formal statement
Proof (Lean source)
THeteroClt 11 declarations
The scaled Hájek-minus-linear-score remainder appearing in the first CLT conjunct.
Definition (Lean source)
Scaled Hájek ratio linearization conclusion.
Definition (Lean source)
Denominator/ratio-remainder tightness input. DISCHARGED (2026-07-09) by heteroDenominatorTightness_discharged: hetero_clt supplies it internally and does NOT assume it. It survives only as a named Prop, because the linearization lemma reads more clearly against it.
Definition (Lean source)
The first CLT conjunct is derived from the denominator/ratio-remainder tightness gate plus the disclosed denominator-kernel regularity condition.
Formal statement
Proof (Lean source)
Linear-score dependency-graph CLT input. DISCHARGED by hetero_linscore_clt_of_depgraph: hetero_clt supplies it internally and does NOT assume it. It survives only as a named Prop.
Definition (Lean source)
The second moment of the raw linear-score sum is card(O) * varScale. The statement is used on the eventual nonempty outcome-array tail supplied by hcardO.
Formal statement
Proof (Lean source)
The linear-score CDF CLT is discharged by the bounded-degree dependency-graph engine. The additional hεfloor regularity is only a uniform positivity floor: it turns the pointwise score bound into an eventual array-uniform summand bound.
Formal statement
Proof (Lean source)
Studentized Slutsky/converging-together transfer for the heterogeneous Hájek CLT. The unstudentized linearization remainder vanishes in probability; the variance nondegeneracy floor makes the studentized remainder vanish in probability; the generic finite-design CDF converging-together helper then transfers the linear-score CLT to the studentized Hájek statistic.
Formal statement
Proof (Lean source)
The scaled Hájek ratio remainder vanishes in probability. Under the design/feasibility regularity conditions and the vanishing denominator-kernel rate, the delta-method remainder √n·(τ̂_H − τ) − n^{-1/2}·∑ᵢ ηᵢ converges to zero in probability. This is the analytic core that discharges the disclosed denominator-tightness gate.
Formal statement
Proof (Lean source)
The disclosed denominator-tightness gate is discharged. Choosing the dominating product tail to be the remainder's own absolute value reduces HeteroDenominatorTightnessInput to remainder_tendstoInProb_zero.
Formal statement
Proof (Lean source)
Heterogeneous Hájek CLT. Along a sequence of feasible experiments whose design is the envelope-optimal design, √n{τ̂_H − τ_n} linearizes onto n^{-1/2} ∑_i η_i (the remainder vanishing in probability), and the studentized statistic converges in distribution to N(0,1) (in CDF form).
Formal statement
Proof (Lean source)
THeteroEnvelope 11 declarations
If every outcome-side quantity lies between minus one and one, its average also lies between minus one and one.
Formal statement
Proof (Lean source)
Under outcomes bounded by one in absolute value, the treated potential-outcome mean is bounded by one in absolute value.
Formal statement
Proof (Lean source)
Under outcomes bounded by one in absolute value, the control potential-outcome mean is bounded by one in absolute value.
Formal statement
Proof (Lean source)
Under bounded outcomes, each treated potential outcome differs from its treated mean by at most two.
Formal statement
Proof (Lean source)
Under bounded outcomes, each control potential outcome differs from its control mean by at most two.
Formal statement
Proof (Lean source)
With strictly positive treatment probabilities no greater than one, every treated-overlap kernel is nonnegative.
Formal statement
Proof (Lean source)
With control probabilities strictly positive and no greater than one, every control-overlap kernel is nonnegative.
Formal statement
Proof (Lean source)
Every mixed treatment-control overlap kernel is nonnegative.
Formal statement
Proof (Lean source)
A nonnegative weight times two quantities each bounded in absolute value by two is at most four times that weight.
Formal statement
Proof (Lean source)
Under interior assignment probabilities and bounded outcomes, each pairwise covariance contribution is no larger than four times its graph-only envelope kernel.
Formal statement
Proof (Lean source)
Heterogeneous envelope kernel. Under the independent heterogeneous Bernoulli design and bounded outcomes, the covariance of the linearization scores factors through the overlap loads, and the variance scale is dominated by the observable graph-only envelope.
Formal statement
Proof (Lean source)
THeterogeneitySeparation 11 declarations
In singleton-exposure graphs, the homogeneous-point envelope gradient reduces to the observable squared intervention-side degree summary.
Formal statement
Proof (Lean source)
The shared non-homogeneity + strict-improvement + explicit-gap conclusion of thm:heterogeneity-separation, factored so that BOTH the general gradient-spread trigger and the standalone singleton-degree trigger deliver the same conclusion. Here a/b attain the max/min gradient score at p^hom; Δg = g_a − g_b > 0 is the gradient-score spread, η_box = min{ρ−ε, 1−ε−ρ}, and L_ab = dirModulus … (e_b−e_a) is the observable directional second-order modulus. The gap admits the explicit lower bound 2 Δg min{η_box, Δg/L_ab} (read as 2 Δg η_box when L_ab = 0).
Definition (Lean source)
The one-dimensional calculus of the reciprocal-product envelope line g(s)=V_env(p^hom+s d)/4: C² regularity on the box segment, differentiability at the origin, the first derivative identity g'(0)=-(g_a-g_b), nonnegativity of the directional modulus, and the le_ciSup curvature bound by dirModulus.
Definition (Lean source)
The homogeneous design is feasible when rho = B / card I and it lies strictly inside the positivity box.
Formal statement
Proof (Lean source)
At an interior homogeneous point, KKT stationarity would force all envelope gradient coordinates to agree. Hence any gradient spread rules out optimality.
Formal statement
Proof (Lean source)
In the singleton-exposure case, unequal squared intervention-side degrees produce unequal homogeneous envelope-gradient coordinates when rho ≠ 1 / 2.
Formal statement
Proof (Lean source)
The EnvelopeLineC2Data gate is discharged. Every conjunct is now derived, so thm:heterogeneity-separation no longer assumes any one-dimensional calculus input.
Formal statement
Proof (Lean source)
General gradient-spread separation, with the one-dimensional Taylor/dirModulus gap estimate now DERIVED: the former EnvelopeLineC2Data hypothesis is supplied internally by envelopeLineC2Data_holds.
Formal statement
Proof (Lean source)
Heterogeneity separation. Set ρ = B/m and let p^hom ≡ ρ be the homogeneous feasible design (with ρ ∈ (ε,1−ε), ρ ≠ 1/2). (1) General trigger: if the gradient scores g_k(p^hom) are not all equal, then p^hom is not an envelope minimizer, every minimizer is non-homogeneous and strictly better, with the explicit 2 Δg min{η_box, Δg/L_ab} gap bound (SeparationConclusion). (2) Singleton reduction: for singleton-exposure graphs the gradient reduces to the observable degree summary g_k(p^hom) = n^{-1} s_k² ((1−ρ)^{-2} − ρ^{-2}). (3) Standalone singleton trigger: for a singleton-exposure graph whose observable degree summaries s_k² are not all equal, the SAME conclusion holds — WITHOUT assuming the gradient-spread hypothesis, which is instead derived from (2) together with ρ ≠ 1/2 (so (1−ρ)^{-2} − ρ^{-2} ≠ 0 scales unequal s_k² into unequal g_k).
Formal statement
Proof (Lean source)
THomogeneousReduction 1 declarations
Homogeneous reduction. Under the independent heterogeneous Bernoulli design, if p_k = p is a common scalar in (0,1), the treated / control overlap loads collapse to p^{-|S_{ij}|} − 1 and (1−p)^{-|S_{ij}|} − 1, and the variance scale equals the homogeneous Bernoulli Hájek overlap formula.
Formal statement
Proof (Lean source)
TPostdesignWald 1 declarations
Post-design conservative Wald coverage. Under the assumptions of the heterogeneous Hájek CLT, the conservative estimator V̂_cons = V_env dominates the variance scale, and the conservative Wald interval has asymptotic coverage ≥ 1 − α, where z is the upper 1 − α/2 standard-normal quantile.
Formal statement
Proof (Lean source)
TSurrogateCertificate 4 declarations
The additive surrogate objective is continuous on the feasible design class under strict overlap.
Formal statement
Proof (Lean source)
The envelope-optimal selector is feasible and minimizes varEnvelope on the feasible set whenever the budget domain is admissible.
Formal statement
Proof (Lean source)
The surrogate selector is feasible and minimizes surrogateObjective on the feasible set whenever the budget domain is admissible.
Formal statement
Proof (Lean source)
Surrogate certificate. With C(ε,d̄) = max{1, ε^{-(d̄-1)}}, the additive surrogate objective A and the normalized envelope V_env/4 satisfy the uniform sandwich A(p) ≤ V_env(p)/4 ≤ C(ε,d̄)·A(p) over feasible p, and consequently the observable approximation ratio is bounded by C(ε,d̄). The selector feasibility and optimality facts are derived from compact attainment under the regularity condition BudgetAdmissible ε B, rather than assumed as hypotheses.