PO.ID.Exact.MultipleInstrumentIV
Multiple-instrument IV: finite-support centered-score response-type algebra and positive-weight results conditional on abstract sign alignment; the generic endpoints do not establish a projected or saturated 2SLS first stage, and MTW partial monotonicity is not formalized.
FiniteIndex 18 core · 5 supporting This file develops finite algebra for an ordered support score. ★ tailCoeff_nonneg★ tailCoeff_eq_cov
Multiple-Instrument IV Finite Index Algebra
This file develops finite algebra for an ordered support score. It defines support masses, ordered scores, centered scores, tail coefficients, and a numeric matrix score adapter. The adapter performs an inverse-Gram transform but does not tie its inputs to observed random variables. Thus this file does not assert the population-projection, saturated-first-stage, or propensity-score conditions used by Mogstad, Torgovitsky, and Walters.
Adjacent thresholds are the positive positions in a finite ordered instrument support, each marking the boundary between consecutive support points.
Definition (Lean source)
The lower endpoint of an adjacent threshold is the support point immediately before that threshold in the finite ordered support.
The upper endpoint of an adjacent threshold is the threshold's own support position in the finite ordered support.
A finite ordered-score index on a finite instrument support records instrument support masses that are nonnegative and sum to one, together with a supplied real score that is weakly increasing in the displayed support order.
Definition (Lean source)
The probability mass at an instrument support point is the real-valued measure under the population law of units whose finite-valued instrument equals that point, on the measurable sample space and finite support.
Definition (Lean source)
The measure-backed ordered score index combines instrument-cell probabilities under a population law with a supplied support score that is weakly increasing in support order, for a measurable instrument on the measurable sample space and finite support.
Definition (Lean source)
The population mean score averages the supplied support score using the instrument masses in an ordered finite score index.
Definition (Lean source)
The centered score at a support point subtracts the population mean score from that point's score in an ordered finite score index.
Definition (Lean source)
The upper-tail support set contains the points at or above an adjacent threshold in a finite ordered support.
The ordered-score tail coefficient is the covariance contribution above an adjacent threshold in an ordered finite score index: upper-tail masses times centered scores. With a projected first-stage score, it is the MTW tail coefficient.
Definition (Lean source)
Every ordered-score tail coefficient is nonnegative in an ordered finite score index at an adjacent threshold, because higher support points have weakly higher scores. For a projected first stage, this is the MTW coefficient sign result.
Formal statement
Proof (Lean source)
Covariance identity. For an ordered finite score index and an adjacent threshold, the threshold's tail coefficient equals the finite-support covariance between the instrument score and the indicator for assignment at or above that threshold.
Formal statement
Proof (Lean source)
The weighted score Gram matrix is the mass-weighted second moment of supplied score vectors under supplied weights, for finite support and score dimensions.
A finite matrix score adapter, for finite support and score dimensions, stores nonnegative support weights that sum to one, support score vectors, and a numeric moment vector, together with an invertibility certificate and monotonicity of the resulting inverse-Gram score.
Definition (Lean source)
The weighted score Gram matrix is the mass-weighted second moment specified by a finite matrix score adapter.
Definition (Lean source)
An inverse-Gram transformed coefficient is the selected coordinate of the numeric transformation specified by a finite matrix score adapter, at the selected score coordinate.
Definition (Lean source)
The adapted score at a support point is the score--coefficient inner product in a finite matrix score adapter at that support point.
Definition (Lean source)
The adapted ordered-score index retains the weights from a finite matrix score adapter and uses its transformed values as the monotone score. Additional hypotheses are needed to identify the supplied weights and moment vector with population treatment moments.
Definition (Lean source)
5 supporting declarations (lemmas, instances)
-
supportMass_nonnegtheorem — Every instrument support mass is nonnegative for a measurable sample space and finite support, population measure, finite-valued instrument, and support point.hypothesesconclusion0 ≤ supportMass μ Z kProof (Lean source)
theorem supportMass_nonneg {Ω : Type*} [MeasurableSpace Ω] {K : ℕ} (μ : Measure Ω) (Z : Ω → Fin K) (k : Fin K) : 0 ≤ supportMass μ Z k := by exact ENNReal.toReal_nonneg -
supportMass_sum_eq_onetheorem — Instrument support masses sum to one under a probability measure, for a measurable finite-valued instrument on the measurable sample space and finite support. This makes the masses population weights.Proof (Lean source)
theorem supportMass_sum_eq_one {Ω : Type*} [MeasurableSpace Ω] {K : ℕ} (μ : Measure Ω) [IsProbabilityMeasure μ] (Z : Ω → Fin K) (hZ : Measurable Z) : ∑ k : Fin K, supportMass μ Z k = 1 := by have hsum : (Finset.univ).sum (fun k : Fin K => (μ (Z ⁻¹' ({k} : Set (Fin K)))).toReal) = (μ (Z ⁻¹' (Set.univ : Set (Fin K)))).toReal := by simpa [Measure.real] using (MeasureTheory.sum_measureReal_preimage_singleton (μ := μ) (s := (Finset.univ : Finset (Fin K))) (f := Z) (hf := by intro k _hk exact hZ (measurableSet_singleton k)) (h := by intro k _hk exact ne_of_lt <| lt_of_le_of_lt (measure_mono (Set.subset_univ _)) (by simp [IsProbabilityMeasure.measure_univ]))) have hpre : ∀ k : Fin K, ({ω | Z ω = k} : Set Ω) = Z ⁻¹' ({k} : Set (Fin K)) := fun _ => rfl simpa [supportMass, hpre, Set.preimage_univ] using hsum -
centered_weight_sum_zerotheorem — The support-mass-weighted centered score sums to zero for an ordered finite score index, which removes baseline components from centered-score moments.Proof (Lean source)
theorem centered_weight_sum_zero : ∑ k, I.rho k * I.centeredIndex k = 0 := by calc ∑ k, I.rho k * I.centeredIndex k = ∑ k, (I.rho k * I.dhat k - I.rho k * I.meanIndex) := by simp [centeredIndex, sub_eq_add_neg, mul_add] _ = ∑ k, I.rho k * I.dhat k - ∑ k, I.rho k * I.meanIndex := by rw [Finset.sum_sub_distrib] _ = I.meanIndex - I.meanIndex * ∑ k, I.rho k := by simp [meanIndex, Finset.sum_mul, mul_comm] _ = 0 := by simp [I.rho_sum_one] -
tail_sum_interchangetheorem — A support-point sum of cumulative margin contributions equals the tail-coefficient-weighted sum over margins for an ordered finite score index and a margin contribution schedule. This is the interchange that exposes signed causal-response weights.hypothesesProof (Lean source)
theorem tail_sum_interchange (x : Adj K → ℝ) : (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then x j else 0)) = ∑ j : Adj K, I.tailCoeff j * x j := by simp only [tailCoeff, upperTail] calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then x j else 0)) = ∑ k : Fin K, ∑ j : Adj K, if j.1.val ≤ k.val then (I.rho k * I.centeredIndex k) * x j else 0 := by simp [Finset.mul_sum, mul_ite, mul_zero, mul_assoc] _ = ∑ j : Adj K, ∑ k : Fin K, if j.1.val ≤ k.val then (I.rho k * I.centeredIndex k) * x j else 0 := by rw [Finset.sum_comm] _ = ∑ j : Adj K, x j * ∑ k : Fin K, if j.1.val ≤ k.val then I.rho k * I.centeredIndex k else 0 := by apply Finset.sum_congr rfl intro j _hj rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _hk by_cases h : j.1.val ≤ k.val · simp [h, mul_comm] · simp [h] _ = ∑ j : Adj K, (∑ k ∈ Finset.univ.filter fun k => j.1.val ≤ k.val, I.rho k * I.centeredIndex k) * x j := by simp [Finset.sum_filter, mul_comm] -
instInvertibleScoreGraminstance — The weighted score Gram matrix is invertible for a finite matrix score adapter.parametersinstancegiven byby change Invertible (weightedScoreGram S.rho S.score) exact S.gram_invertible
ResponseTypes 21 core · 7 supporting This file formalizes finite response-type algebra for a centered-score IV decomposition. ★ centeredScoreIVPopulationBridge_eq_centeredScoreIVFiniteAlgebra★ centeredScoreIVFiniteAlgebra_eq_responseTypeWeightedSum★ centeredScoreIVFiniteAlgebra_eq_positiveResponseTypeAverage_of_signAligned
Multiple-Instrument IV Response Types
This file formalizes finite response-type algebra for a centered-score IV
decomposition. The basic
objects are ResponseType, typeStep, ResponseTypeStats, the unnormalized
and normalized weights unnormTypeWeight and normalizedTypeWeight, and the
finite ratio centeredScoreIVFiniteAlgebra.
The nested PopulationBridge structure gives a finite-support
bridge from support-point outcome and treatment expansions to the response-type
ratio. Theorems firstStageMoment_eq_typeWeightDenom,
reducedFormMoment_eq_typeWeightNumerator, and
centeredScoreIVPopulationBridge_eq_centeredScoreIVFiniteAlgebra prove the algebraic
identification step. The sign-alignment results
normalizedTypeWeight_nonneg_of_signAligned,
normalizedTypeWeight_sum_eq_one_of_pos, and
centeredScoreIVFiniteAlgebra_eq_positiveResponseTypeAverage_of_signAligned explain
when the ratio is a convex response-type average under an assumed abstract sign
condition, while exists_negativeNormalizedTypeWeight
gives a concrete two-support-point counterexample with a negative normalized
weight.
The OpaqueAdjacentStepRestriction structure is only an opaque interface. It
is not a formalization of MTW partial monotonicity, and no result in this file
derives sign alignment from a behavioral monotonicity condition.
A treatment response type specifies binary uptake at every point of a finite instrument support, capturing all first-stage heterogeneity relevant to the IV design.
The real-valued treatment indicator converts binary uptake to one for treatment and zero for no treatment, so it can enter population moments.
Definition (Lean source)
An adjacent treatment-response increment measures how a response type changes across one support threshold in a finite instrument support.
Definition (Lean source)
Finite response-type statistics on a finite instrument support record the probability mass of each latent type and its average causal effect, subject to every mass being nonnegative and the masses summing to one, so the masses form a probability vector over response types.
Definition (Lean source)
The unnormalized weight on a response type is that type's population mass times its tail-coefficient-weighted treatment increments, using an ordered score and finite response-type statistics.
Definition (Lean source)
The response-type weight denominator aggregates the signed type weights generated by an ordered score and finite response-type statistics; it is the finite first-stage moment.
Definition (Lean source)
The normalized weight on a response type divides that type's signed weight by the total generated from an ordered score and finite response-type statistics.
Definition (Lean source)
The response-type estimand averages type-specific causal effects from finite response-type statistics using the normalized weights induced by an ordered score.
Definition (Lean source)
The finite-algebra centered-score IV ratio divides the signed response-type-weighted effect sum from finite response-type statistics by the corresponding first-stage weight sum induced by an ordered score.
Definition (Lean source)
A finite-support response-type bridge on a finite instrument support combines response-type masses and type-specific effects with a baseline outcome mean for each response type. The centered score cancels this baseline, leaving the adjacent treatment increments used by the finite algebra.
Definition (Lean source)
A response type's cumulative treatment change at a support point sums that type's adjacent uptake changes through the selected point of the finite instrument support.
Definition (Lean source)
The outcome mean at an instrument support point expands into baseline outcomes plus type-mass-weighted causal effects times cumulative treatment changes under the finite-support population bridge, at that point of the support.
Definition (Lean source)
The treatment-mean change from the reference support point is the type-mass-weighted cumulative uptake change under the finite-support population bridge, at the selected point of the support.
Definition (Lean source)
The population centered-score outcome moment weights support-specific outcome expansions from a finite-support bridge by centered scores from an ordered index across the finite support.
Definition (Lean source)
The population centered-score treatment moment weights support-specific treatment expansions from a finite-support bridge by centered scores from an ordered index across the finite support.
Definition (Lean source)
The population centered-score IV ratio divides the outcome moment by the treatment moment for a finite-support population bridge and ordered score index on the finite support.
Definition (Lean source)
The population centered-score IV ratio equals the finite response-type ratio for an ordered finite score index and a finite-support response-type bridge. This is the decomposition algebra; a 2SLS interpretation additionally requires a projected first-stage score.
Formal statement
Proof (Lean source)
Sign alignment requires every positive-mass response type in finite response-type statistics to have a nonnegative tail-coefficient-weighted treatment response under the ordered score. It is exactly the condition preventing negative type weights.
Definition (Lean source)
The opaque adjacent-step interface on a finite instrument support stores an arbitrary response-type selection rule together with an assumed nonnegative-step certificate for selected types. It does not itself encode an econometric monotonicity restriction.
Definition (Lean source)
The finite-algebra centered-score IV ratio equals the response-type-weighted sum of within-type causal effects for an ordered score and finite response-type statistics when the score-weight denominator is nonzero. This is the normalization algebra appearing in prop:po-estimand-mtw-response-type-form, whose 2SLS interpretation additionally fixes the score to the fitted first stage.
Formal statement
Proof (Lean source)
The centered-score IV ratio is a convex average of response-type causal effects for an ordered score and finite response-type statistics when response types are sign-aligned and the score-weight denominator is positive: every weight is nonnegative and the weights sum to one.
Formal statement
Proof (Lean source)
7 supporting declarations (lemmas, instances)
-
baselineMoment_eq_zerotheorem — The centered-score moment of the response-type baseline outcome is zero for an ordered score index and finite-support population bridge, so only causal-response increments remain in the reduced form.hypothesesconclusion(∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g))= 0Proof (Lean source)
theorem baselineMoment_eq_zero : (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g)) = 0 := by calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g)) = (∑ k : Fin K, I.rho k * I.centeredIndex k) * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g) := by rw [Finset.sum_mul] _ = 0 := by rw [I.centered_weight_sum_zero] simp -
firstStageMoment_eq_typeWeightDenomtheorem — The finite-support first-stage moment equals the aggregate response-type weight for an ordered score index and population bridge. This identifies the denominator of the response-type IV ratio.hypothesesconclusionP.firstStageMoment I = P.stats.typeWeightDenom IProof (Lean source)
theorem firstStageMoment_eq_typeWeightDenom : P.firstStageMoment I = P.stats.typeWeightDenom I := by classical unfold firstStageMoment treatmentAtSupport telescopedTypeStep ResponseTypeStats.typeWeightDenom ResponseTypeStats.unnormTypeWeight calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0))) = ∑ k : Fin K, ∑ g : ResponseType K, I.rho k * I.centeredIndex k * (P.stats.mass g * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) := by apply Finset.sum_congr rfl intro k _hk rw [Finset.mul_sum] _ = ∑ g : ResponseType K, ∑ k : Fin K, I.rho k * I.centeredIndex k * (P.stats.mass g * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) := by rw [Finset.sum_comm] _ = ∑ g : ResponseType K, P.stats.mass g * (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) := by apply Finset.sum_congr rfl intro g _hg rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _hk ring _ = ∑ g : ResponseType K, P.stats.mass g * (∑ j : Adj K, I.tailCoeff j * typeStep g j) := by apply Finset.sum_congr rfl intro g _hg rw [I.tail_sum_interchange (fun j => typeStep g j)] -
reducedFormMoment_eq_typeWeightNumeratortheorem — The finite-support reduced-form moment equals the response-type-weighted causal-effect sum for an ordered score index and population bridge. This identifies the numerator of the response-type IV ratio.hypothesesconclusionP.reducedFormMoment I= ∑ g : ResponseType K, P.stats.unnormTypeWeight I g * P.stats.effect gProof (Lean source)
theorem reducedFormMoment_eq_typeWeightNumerator : P.reducedFormMoment I = ∑ g : ResponseType K, P.stats.unnormTypeWeight I g * P.stats.effect g := by classical unfold reducedFormMoment outcomeAtSupport telescopedTypeStep ResponseTypeStats.unnormTypeWeight calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * (P.baseOutcome g + (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g))) = (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * P.baseOutcome g)) + ∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by simp only [mul_add, Finset.sum_add_distrib] _ = ∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ g : ResponseType K, P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by rw [P.baselineMoment_eq_zero I] simp _ = ∑ k : Fin K, ∑ g : ResponseType K, I.rho k * I.centeredIndex k * (P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by apply Finset.sum_congr rfl intro k _hk rw [Finset.mul_sum] _ = ∑ g : ResponseType K, ∑ k : Fin K, I.rho k * I.centeredIndex k * (P.stats.mass g * ((∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0) * P.stats.effect g)) := by rw [Finset.sum_comm] _ = ∑ g : ResponseType K, P.stats.mass g * (∑ k : Fin K, I.rho k * I.centeredIndex k * (∑ j : Adj K, if j.1.val ≤ k.val then typeStep g j else 0)) * P.stats.effect g := by apply Finset.sum_congr rfl intro g _hg simp [Finset.mul_sum, mul_assoc, mul_comm, mul_left_comm] _ = ∑ g : ResponseType K, (P.stats.mass g * (∑ j : Adj K, I.tailCoeff j * typeStep g j)) * P.stats.effect g := by apply Finset.sum_congr rfl intro g _hg rw [I.tail_sum_interchange (fun j => typeStep g j)] -
unnormTypeWeight_nonneg_of_signAlignedtheorem — Every unnormalized response-type weight is nonnegative when an ordered score and finite response-type population satisfy sign alignment, for the selected response type. Nonnegative type masses then preserve the aligned sign.hypothesesK :sharedℕhAlign :R.SignAligned Ig :conclusion0 ≤ R.unnormTypeWeight I gProof (Lean source)
theorem unnormTypeWeight_nonneg_of_signAligned (hAlign : R.SignAligned I) (g : ResponseType K) : 0 ≤ R.unnormTypeWeight I g := by unfold unnormTypeWeight by_cases hpos : 0 < R.mass g · exact mul_nonneg (R.mass_nonneg g) (hAlign g hpos) · have hle : R.mass g ≤ 0 := le_of_not_gt hpos have hmass : R.mass g = 0 := le_antisymm hle (R.mass_nonneg g) simp [hmass] -
normalizedTypeWeight_nonneg_of_signAlignedtheorem — Each normalized response-type weight is nonnegative when an ordered score and finite response-type population satisfy sign alignment and have a positive score-weight denominator, for the selected response type. The paper-facing 2SLS claim needs additional first-stage and behavioral conditions.hypothesesK :sharedℕhAlign :R.SignAligned Ihden :0 < R.typeWeightDenom Ig :conclusion0 ≤ R.normalizedTypeWeight I gProof (Lean source)
theorem normalizedTypeWeight_nonneg_of_signAligned (hAlign : R.SignAligned I) (hden : 0 < R.typeWeightDenom I) (g : ResponseType K) : 0 ≤ R.normalizedTypeWeight I g := by exact normalizedWeight_nonneg (R.unnormTypeWeight I) (R.unnormTypeWeight_nonneg_of_signAligned I hAlign) hden g -
normalizedTypeWeight_sum_eq_one_of_postheorem — The normalized response-type weights sum to one for an ordered score and finite response-type population when the first-stage weight denominator is positive.hypothesesconclusion∑ g : ResponseType K, R.normalizedTypeWeight I g = 1Proof (Lean source)
theorem normalizedTypeWeight_sum_eq_one_of_pos (hden : 0 < R.typeWeightDenom I) : ∑ g : ResponseType K, R.normalizedTypeWeight I g = 1 := by exact sum_normalizedWeight_eq_one (R.unnormTypeWeight I) hden.ne' -
exists_negativeNormalizedTypeWeighttheorem — Negative-weights theorem. There exists a finite-support instrument index, a response-type population, and a response type such that, with two support points and a 3/4-defier population, that type has positive mass yet a negative normalized response-type weight (equal to −1/2).conclusionconclusion 10 < R.mass gconclusion 2R.normalizedTypeWeight I g < 0Proof (Lean source)
theorem exists_negativeNormalizedTypeWeight : ∃ (I : FiniteIndex 2) (R : ResponseTypeStats 2) (g : ResponseType 2), 0 < R.mass g ∧ R.normalizedTypeWeight I g < 0 := by refine ⟨exIndex, exStats, gComplier, ?_, ?_⟩ · -- mass of complier type = 1/4 > 0 rw [exStats_mass, exMass_complier]; norm_num · -- normalized weight = (3/64) / (-3/32) = -1/2 < 0 rw [ResponseTypeStats.normalizedTypeWeight, normalizedWeight] change exStats.unnormTypeWeight exIndex gComplier / (∑ k, exStats.unnormTypeWeight exIndex k) < 0 rw [← ResponseTypeStats.typeWeightDenom, exStats_unnorm_complier, exStats_denom] norm_num
Population 6 core · 5 supporting This file connects an observed centered-score IV moment ratio for a finite instrument to the response-type finite algebra. ★ observedCenteredScoreIV_eq_centeredScoreIVFiniteAlgebra
Multiple-Instrument IV Population Bridge
This file connects an observed centered-score IV moment ratio for a finite
instrument to the response-type finite algebra. It defines
the observed moments observedReducedFormMoment, observedFirstStageMoment,
and observedCenteredScoreIV; rewrites the first two as finite sums over instrument
cells; and packages the assumptions needed for the measure-backed bridge in
ObservedBridge.
The main results are ObservedBridge.observedReducedFormMoment_eq_reducedFormMoment,
ObservedBridge.observedFirstStageMoment_eq_firstStageMoment,
ObservedBridge.observedCenteredScoreIV_eq_centeredScoreIVPopulationBridge, and the
end-to-end theorem ObservedBridge.observedCenteredScoreIV_eq_centeredScoreIVFiniteAlgebra.
They show that the observable population ratio E[h(Z)Y] / E[h(Z)D] agrees
with the finite response-type algebra once the observed conditional means are
linked to the bridge. A separate projected-score premise is needed to call
this ratio population 2SLS.
An instrument cell selects units in a sample space whose finite-valued instrument equals one support point in the finite support.
The observed centered-score outcome moment averages outcome times the centered score from an ordered index, evaluated at the instrument under the population measure on the measurable sample space and finite support.
Definition (Lean source)
The observed centered-score treatment moment averages binary treatment times the centered score from an ordered index, evaluated at the instrument under the population measure on the measurable sample space and finite support.
Definition (Lean source)
The observed centered-score IV ratio divides the centered-score moment of the outcome by that of binary treatment, using an instrument, ordered score index, and population measure on the measurable sample space and finite support.
Definition (Lean source)
An observed-data response-type bridge on a measurable population space with finite instrument support connects a population law, a finite-valued instrument, a binary treatment, and a real-valued outcome to an ordered score index and a response-type population expansion. It requires the law to be a probability measure, index masses to match observed instrument-cell probabilities, conditional outcome means to match the response-type expansion, and conditional treatment means to follow the response-type expansion around a common baseline.
Definition (Lean source)
The observed centered-score IV ratio equals the finite response-type algebra ratio under a measure, instrument, treatment, outcome, ordered score, and observed-data bridge, when the instrument is measurable, the weighted outcome and weighted treatment are integrable.
Formal statement
Proof (Lean source)
5 supporting declarations (lemmas, instances)
-
observedReducedFormMoment_eq_sum_eventCondExptheorem — The centered-score outcome moment equals the support-mass-weighted sum of instrument-cell outcome means under a finite population law, for a measurable instrument, outcome, ordered score index, and integrability of the weighted outcome. This is the finite-support law of total expectation.hypothesesΩ :sharedType u_1K :sharedℕμ :Z :Ω → Fin KhZ :Y :Ω → ℝI :hInt :Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μconclusionobservedReducedFormMoment μ Z Y I= ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * normalizedRestrictedIntegral μ (zEvent Z k) YProof (Lean source)
theorem observedReducedFormMoment_eq_sum_eventCondExp (μ : Measure Ω) [IsFiniteMeasure μ] (Z : Ω → Fin K) (hZ : Measurable Z) (Y : Ω → ℝ) (I : FiniteIndex K) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) : observedReducedFormMoment μ Z Y I = ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * normalizedRestrictedIntegral μ (zEvent Z k) Y := by unfold observedReducedFormMoment rw [integral_eq_sum_measure_mul_eventCondExp (μ := μ) (A := zEvent Z) (hmeas := zEvent_measurable Z hZ) (hdisj := zEvent_pairwise_disjoint Z) (hcov := zEvent_iUnion Z) (f := fun ω => I.centeredIndex (Z ω) * Y ω) hInt] refine Finset.sum_congr rfl ?_ intro k _hk rw [eventCondExp_centered_mul_eq μ Z hZ Y I k] ring -
observedFirstStageMoment_eq_sum_eventCondExptheorem — The centered-score treatment moment equals the support-mass-weighted sum of instrument-cell treatment means under a finite population law, for a measurable instrument, binary treatment, ordered score index, and integrability of the weighted treatment.hypothesesΩ :sharedType u_1K :sharedℕμ :Z :Ω → Fin KhZ :D :Ω → BoolI :hInt :Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μconclusionobservedFirstStageMoment μ Z D I= ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * normalizedRestrictedIntegral μ (zEvent Z k) (fun ω => boolToReal (D ω))Proof (Lean source)
theorem observedFirstStageMoment_eq_sum_eventCondExp (μ : Measure Ω) [IsFiniteMeasure μ] (Z : Ω → Fin K) (hZ : Measurable Z) (D : Ω → Bool) (I : FiniteIndex K) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedFirstStageMoment μ Z D I = ∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * normalizedRestrictedIntegral μ (zEvent Z k) (fun ω => boolToReal (D ω)) := by exact observedReducedFormMoment_eq_sum_eventCondExp (μ := μ) (Z := Z) hZ (Y := fun ω => boolToReal (D ω)) I hInt -
observedReducedFormMoment_eq_reducedFormMomenttheorem — The observed centered-score outcome moment equals its finite response-type expansion when the observed-data bridge holds, the instrument is measurable, and the weighted outcome is integrable.hypothesesΩ :sharedType u_1K :sharedℕY :sharedΩ → ℝB :ObservedBridge μ Z D Y I PhZ :hInt :Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μconclusionobservedReducedFormMoment μ Z Y I = P.reducedFormMoment IProof (Lean source)
theorem observedReducedFormMoment_eq_reducedFormMoment (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) : observedReducedFormMoment μ Z Y I = P.reducedFormMoment I := by rw [observedReducedFormMoment_eq_sum_eventCondExp μ Z hZ Y I hInt] unfold reducedFormMoment refine Finset.sum_congr rfl ?_ intro k _hk rw [← B.rho_eq_zMass k, B.outcome_cell k] -
observedFirstStageMoment_eq_firstStageMomenttheorem — The observed centered-score treatment moment equals its finite response-type expansion when the observed-data bridge holds, the instrument is measurable, and the weighted treatment is integrable.hypothesesΩ :sharedType u_1K :sharedℕY :sharedΩ → ℝB :ObservedBridge μ Z D Y I PhZ :hInt :Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μconclusionobservedFirstStageMoment μ Z D I = P.firstStageMoment IProof (Lean source)
theorem observedFirstStageMoment_eq_firstStageMoment (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedFirstStageMoment μ Z D I = P.firstStageMoment I := by rw [observedFirstStageMoment_eq_sum_eventCondExp μ Z hZ D I hInt] unfold firstStageMoment calc (∑ k : Fin K, (μ (zEvent Z k)).toReal * I.centeredIndex k * normalizedRestrictedIntegral μ (zEvent Z k) (fun ω => boolToReal (D ω))) = ∑ k : Fin K, I.rho k * I.centeredIndex k * (B.baseTreatment + P.treatmentAtSupport k) := by refine Finset.sum_congr rfl ?_ intro k _hk rw [← B.rho_eq_zMass k, B.treatment_cell k] _ = (∑ k : Fin K, I.rho k * I.centeredIndex k) * B.baseTreatment + ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by calc (∑ k : Fin K, I.rho k * I.centeredIndex k * (B.baseTreatment + P.treatmentAtSupport k)) = ∑ k : Fin K, (I.rho k * I.centeredIndex k * B.baseTreatment + I.rho k * I.centeredIndex k * P.treatmentAtSupport k) := by refine Finset.sum_congr rfl ?_ intro k _hk ring _ = (∑ k : Fin K, I.rho k * I.centeredIndex k * B.baseTreatment) + ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by rw [Finset.sum_add_distrib] _ = (∑ k : Fin K, I.rho k * I.centeredIndex k) * B.baseTreatment + ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by rw [Finset.sum_mul] _ = ∑ k : Fin K, I.rho k * I.centeredIndex k * P.treatmentAtSupport k := by rw [I.centered_weight_sum_zero] simp -
observedCenteredScoreIV_eq_centeredScoreIVPopulationBridgetheorem — The observed centered-score IV ratio equals the finite-support population-bridge ratio under a measure, instrument, treatment, outcome, ordered score, and observed-data bridge, when the instrument is measurable, the weighted outcome and weighted treatment are integrable.hypothesesΩ :sharedType u_1K :sharedℕY :sharedΩ → ℝB :ObservedBridge μ Z D Y I PhZ :hYInt :Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μhDInt :Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μconclusionobservedCenteredScoreIV μ Z D Y I = P.centeredScoreIVPopulationBridge IProof (Lean source)
theorem observedCenteredScoreIV_eq_centeredScoreIVPopulationBridge (B : ObservedBridge μ Z D Y I P) [IsFiniteMeasure μ] (hZ : Measurable Z) (hYInt : Integrable (fun ω => I.centeredIndex (Z ω) * Y ω) μ) (hDInt : Integrable (fun ω => I.centeredIndex (Z ω) * boolToReal (D ω)) μ) : observedCenteredScoreIV μ Z D Y I = P.centeredScoreIVPopulationBridge I := by unfold observedCenteredScoreIV centeredScoreIVPopulationBridge rw [B.observedReducedFormMoment_eq_reducedFormMoment hZ hYInt, B.observedFirstStageMoment_eq_firstStageMoment hZ hDInt]
Main 5 core · 2 supporting This file provides the public finite-support facade for an abstract multiple-instrument response-type algebra. ★ centeredScoreIVPopulationBridge_eq_responseTypeWeightedSum★ centeredScoreIVPopulationBridge_eq_positiveResponseTypeAverage_of_signAligned★ observedCenteredScoreIV_eq_responseTypeWeightedSum
Multiple-Instrument IV Main Facade
This file provides the public finite-support facade for an abstract multiple-instrument response-type algebra. It exposes the signed adjacent ratio, the response-type weighted-sum form, positivity under an assumed sign- alignment condition, and the corresponding population bridge statements. It does not provide the behavioral or empirical conditions in the full MTW multiple-instrument characterization.
The signed adjacent outcome numerator aggregates within-type causal effects from finite response-type statistics using the unnormalized weights induced by an ordered score.
Definition (Lean source)
The signed adjacent treatment denominator aggregates all unnormalized type weights induced by an ordered score and finite response-type statistics.
Definition (Lean source)
The population-bridge centered-score IV ratio equals the response-type-weighted sum of within-type causal effects for an ordered score and finite-support population bridge, provided the score-weight denominator is nonzero.
Formal statement
Proof (Lean source)
The population-bridge centered-score IV ratio is a convex response-type average for an ordered score and finite-support population bridge when response types are sign-aligned and the score-weight denominator is positive.
Formal statement
Proof (Lean source)
The observed centered-score IV ratio equals the response-type-weighted sum of within-type causal effects when an observed-data bridge links instrument, treatment, and outcome to the response-type population, the instrument is measurable, the weighted outcome and weighted treatment are integrable, and the observed first stage is nonzero.
Formal statement
Proof (Lean source)
2 supporting declarations (lemmas, instances)
-
centeredScoreIVFiniteAlgebra_eq_signedAdjacentRatiotheorem — The finite-algebra centered-score IV ratio is the signed adjacent outcome numerator divided by the treatment denominator for an ordered score and finite response-type statistics, provided that denominator is nonzero.hypothesesK :sharedℕ_hden :R.signedAdjacentDenominator I ≠ 0conclusionR.centeredScoreIVFiniteAlgebra I= R.signedAdjacentNumerator I / R.signedAdjacentDenominator IProof (Lean source)
theorem centeredScoreIVFiniteAlgebra_eq_signedAdjacentRatio (_hden : R.signedAdjacentDenominator I ≠ 0) : R.centeredScoreIVFiniteAlgebra I = R.signedAdjacentNumerator I / R.signedAdjacentDenominator I := by rfl -
centeredScoreIVPopulationBridge_eq_signedAdjacentRatiotheorem — The population-bridge centered-score IV ratio equals the signed adjacent outcome numerator divided by its treatment denominator for an ordered score and finite-support population bridge, provided the denominator is nonzero.hypothesesK :sharedℕhden :P.stats.signedAdjacentDenominator I ≠ 0conclusionP.centeredScoreIVPopulationBridge I= P.stats.signedAdjacentNumerator I / P.stats.signedAdjacentDenominator IProof (Lean source)
theorem centeredScoreIVPopulationBridge_eq_signedAdjacentRatio (hden : P.stats.signedAdjacentDenominator I ≠ 0) : P.centeredScoreIVPopulationBridge I = P.stats.signedAdjacentNumerator I / P.stats.signedAdjacentDenominator I := by rw [P.centeredScoreIVPopulationBridge_eq_centeredScoreIVFiniteAlgebra I] exact P.stats.centeredScoreIVFiniteAlgebra_eq_signedAdjacentRatio I hden
POBridge 27 core · 24 supporting This file grounds a multiple-instrument finite response-type algebra in a potential-outcome system. ★ POMultipleIVSystem★ observedCenteredScoreIV_eq_responseTypeWeightedSum
Multiple-Instrument IV Potential-Outcome Bridge
This file grounds a multiple-instrument finite response-type algebra in a
potential-outcome system. The structure POMultipleIVSystem records a finite
instrument, binary treatment, and real outcome; responseType, mass,
effect, toStats, and toPopulationBridge turn its counterfactual response
types into the finite response-type algebra.
The bridge lemmas treatmentDrop and outcomeDrop derive instrument-cell
conditional means from consistency and instrument independence. The definitions
toObservedBridge and theorem
observedCenteredScoreIV_eq_responseTypeWeightedSum assemble those derived cell
identities into an observed finite-support centered-score response-type identity. The
behavioral and empirical conditions of the full MTW characterization are not
formalized here, nor is the supplied score proved to be a first-stage fit.
A multiple-instrument IV potential-outcome subsystem within a potential-outcome system and finite instrument support records an instrument node with that support, a binary treatment node, and a real-valued outcome node, subject to the three nodes being pairwise distinct.
Definition (Lean source)
The finite-valued instrument variable exposes the assignment node of a multiple-instrument IV subsystem inside the potential-outcome system on its finite support.
Definition (Lean source)
The binary treatment variable exposes uptake from a multiple-instrument IV subsystem inside the potential-outcome system with finite instrument support.
Definition (Lean source)
The real-valued outcome variable exposes the response from a multiple-instrument IV subsystem inside the potential-outcome system with finite instrument support.
Definition (Lean source)
Potential treatment records binary uptake in a multiple-instrument IV subsystem of the potential-outcome system under a fixed instrument support point from the finite support.
Definition (Lean source)
Potential outcome records the response in a multiple-instrument IV subsystem of the potential-outcome system under a fixed treatment arm, with exclusion encoded structurally over the finite instrument support.
Definition (Lean source)
The observed instrument records realized assignment in a multiple-instrument IV subsystem of the potential-outcome system on the finite support.
Definition (Lean source)
The observed treatment records realized binary uptake in a multiple-instrument IV subsystem of the potential-outcome system with finite instrument support.
Definition (Lean source)
The observed outcome records realized response in a multiple-instrument IV subsystem of the potential-outcome system with finite instrument support.
Definition (Lean source)
The treatment response-type map collects each unit's potential uptake at every point of the finite instrument support in a multiple-instrument IV subsystem of the potential-outcome system.
Definition (Lean source)
A response-type subgroup selects units in a multiple-instrument IV subsystem of the potential-outcome system whose treatment-response vector equals the chosen type on the finite support.
Definition (Lean source)
An observed instrument cell selects units in a multiple-instrument IV subsystem of the potential-outcome system assigned to one support point in the finite support.
Definition (Lean source)
Outcome under instrument-induced treatment selects the treated or untreated potential outcome in a multiple-instrument IV subsystem of the potential-outcome system according to uptake induced by one support point in the finite support.
Definition (Lean source)
The regimed treatment response couples potential uptake in a multiple-instrument IV subsystem of the potential-outcome system with the support point fixed from the finite instrument support.
Definition (Lean source)
The regimed outcome response couples potential outcome in a multiple-instrument IV subsystem of the potential-outcome system with the fixed treatment arm, over the finite instrument support.
Definition (Lean source)
The support-point counterfactual cell bundles potential treatment under one instrument value with both treatment-arm outcomes in a multiple-instrument IV subsystem of the potential-outcome system on the finite support.
Definition (Lean source)
Local multi-instrument bridge assumptions. A multiple-instrument subsystem in a potential-outcome system with finite instrument support assumes the observed treatment and outcome equal the potential treatment and outcome realized under the actual instrument value, and at each support point the instrument is independent of the potential treatment there and both treatment-arm potential outcomes.
Definition (Lean source)
Consistency (SUTVA): observed D/Y equal the realized potential
treatment/outcome.
Instrument independence (IV exogeneity): for each support point, the
instrument is independent of the counterfactual cell (D(zᵏ), Y(1), Y(0)).
This is implied by (and weaker than) full joint independence of Z from all
potential outcomes; it is exactly what the cell-conditional-mean derivations
below consume.
A response-type mass is the population probability of the selected treatment-response type in a multiple-instrument IV subsystem of the potential-outcome system on the finite support.
Definition (Lean source)
The within-type causal effect averages the treated-minus-untreated outcome contrast among units of one response type in a multiple-instrument IV subsystem of the potential-outcome system on the finite support.
Definition (Lean source)
The reference instrument value is the first point of a nonempty finite support for a multiple-instrument IV subsystem in the potential-outcome system.
Definition (Lean source)
A response type's baseline outcome is its mean outcome under treatment induced by the first point of a nonempty finite support, for the selected type in a multiple-instrument IV subsystem of the potential-outcome system.
Definition (Lean source)
The baseline treatment mean is average uptake induced by the first point of a nonempty finite support in a multiple-instrument IV subsystem of the potential-outcome system.
Definition (Lean source)
Finite response-type statistics collect type masses and within-type causal effects from a multiple-instrument IV subsystem of the potential-outcome system on the finite support.
Definition (Lean source)
The finite-support response-type population bridge combines type statistics and baseline outcomes from a multiple-instrument IV subsystem of the potential-outcome system on a nonempty finite support.
Definition (Lean source)
The subsystem's ordered finite score index combines its instrument-cell probabilities with a supplied support score that is weakly increasing, for a multiple-instrument IV subsystem of the potential-outcome system on the finite support.
The observed population bridge links factual moments to the finite response-type representation for a multiple-instrument IV subsystem of the potential-outcome system on a nonempty support, under the local IV assumptions, a weakly increasing support score, positive instrument-cell mass, and integrable treated and untreated potential outcomes.
Definition (Lean source)
Potential-outcome finite-support centered-score IV identity. Consider a nonempty finite instrument support together with a real support score that is weakly increasing in the support order, under the local consistency and pointwise-exogeneity bundle. If every instrument-support cell has positive probability, the potential outcome under treatment and under control are integrable, the centered-instrument-weighted outcome and treatment are integrable, and the observed first-stage moment is nonzero, then the observed centered-score IV estimand equals the response-type-weighted average of within-type causal effects.
Formal statement
Proof (Lean source)
24 supporting declarations (lemmas, instances)
-
YofDofZ_deflemma — Instrument-induced outcome equals the treated potential outcome when uptake occurs and the untreated potential outcome otherwise in a multiple-instrument IV subsystem, at the chosen support point of the finite support.hypotheses -
measurable_DofZlemma — Potential treatment at an instrument support point is measurable in a multiple-instrument IV subsystem, for that point of the finite support in the potential-outcome system.hypothesesconclusionMeasurable (S.DofZ k)Proof (Lean source)
@[fun_prop] lemma measurable_DofZ (k : Fin K) : Measurable (S.DofZ k) := S.dVar.measurable_cfUnder S.zVar k -
measurable_YofDlemma — Potential outcome under a treatment arm is measurable in a multiple-instrument IV subsystem, for that arm within the potential-outcome system and finite instrument support.hypothesesconclusionMeasurable (S.YofD d)Proof (Lean source)
@[fun_prop] lemma measurable_YofD (d : Bool) : Measurable (S.YofD d) := S.yVar.measurable_cfUnder S.dVar d -
measurable_factualZlemma — The observed instrument is measurable in a multiple-instrument IV subsystem of the potential-outcome system on the finite support, making instrument cells observable.hypothesesconclusionMeasurable S.factualZProof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.zVar.measurable_factual -
measurable_factualDlemma — The observed treatment is measurable in a multiple-instrument IV subsystem of the potential-outcome system with finite instrument support.hypothesesconclusionMeasurable S.factualDProof (Lean source)
@[fun_prop] lemma measurable_factualD : Measurable S.factualD := S.dVar.measurable_factual -
measurable_factualYlemma — The observed outcome is measurable in a multiple-instrument IV subsystem of the potential-outcome system with finite instrument support, so its moments are defined.hypothesesconclusionMeasurable S.factualYProof (Lean source)
@[fun_prop] lemma measurable_factualY : Measurable S.factualY := S.yVar.measurable_factual -
measurable_responseTypelemma — The full treatment response-type map is measurable in a multiple-instrument IV subsystem of the potential-outcome system on the finite support, making latent type cells measurable.hypothesesconclusionMeasurable S.responseTypeProof (Lean source)
@[fun_prop] lemma measurable_responseType : Measurable S.responseType := measurable_pi_lambda _ (fun k => S.measurable_DofZ k) -
measurableSet_gEventlemma — Each response-type subgroup is measurable in a multiple-instrument IV subsystem, for the selected type on the finite support within the potential-outcome system.hypothesesconclusionMeasurableSet (S.gEvent g)Proof (Lean source)
lemma measurableSet_gEvent (g : ResponseType K) : MeasurableSet (S.gEvent g) := S.measurable_responseType (measurableSet_singleton g) -
measurableSet_zEventlemma — Each observed instrument cell is measurable in a multiple-instrument IV subsystem, for the selected point of the finite support within the potential-outcome system.hypothesesconclusionMeasurableSet (S.zEvent k)Proof (Lean source)
lemma measurableSet_zEvent (k : Fin K) : MeasurableSet (S.zEvent k) := S.zVar.measurableSet_event k (measurableSet_singleton k) -
measurable_YofDofZlemma — Outcome under instrument-induced treatment is measurable in a multiple-instrument IV subsystem, for the selected point of the finite support within the potential-outcome system.hypothesesconclusionMeasurable (S.YofDofZ k)Proof (Lean source)
@[fun_prop] lemma measurable_YofDofZ (k : Fin K) : Measurable (S.YofDofZ k) := by unfold YofDofZ exact Measurable.ite (S.measurable_DofZ k (MeasurableSet.singleton true)) (S.measurable_YofD true) (S.measurable_YofD false) -
DofZ_eq_factualD_on_zEventlemma — Consistency identifies potential treatment with observed treatment inside an instrument cell under the local multi-instrument assumptions, for the support point and a unit observed in its cell.hypothesesconclusionS.DofZ k ω = S.factualD ωProof (Lean source)
lemma DofZ_eq_factualD_on_zEvent (hA : S.Assumptions) (k : Fin K) {ω : P.Ω} (hω : ω ∈ S.zEvent k) : S.DofZ k ω = S.factualD ω := POVar.cf_eq_factual_on_event hA.consistency S.dVar S.zVar k S.hZD.symm hω -
factualY_eq_YofD_factualDlemma — Consistency identifies observed outcome with potential outcome under realized treatment under the local multi-instrument assumptions, for the unit being evaluated.hypothesesconclusionS.factualY ω = S.YofD (S.factualD ω) ωProof (Lean source)
lemma factualY_eq_YofD_factualD (hA : S.Assumptions) (ω : P.Ω) : S.factualY ω = S.YofD (S.factualD ω) ω := POVar.factual_eq_cfUnder_self_selected hA.consistency S.yVar S.dVar S.hDY.symm ω -
DofZ_eq_on_gEventlemma — Within a response-type subgroup, potential treatment at a support point equals that type's recorded response for the response type, support point, and unit in the type cell. This makes cell means expandable over latent types.Proof (Lean source)
lemma DofZ_eq_on_gEvent (g : ResponseType K) (k : Fin K) {ω : P.Ω} (hω : ω ∈ S.gEvent g) : S.DofZ k ω = g k := by have : S.responseType ω = g := hω calc S.DofZ k ω = S.responseType ω k := rfl _ = g k := by rw [this] -
treatmentDroptheorem — The observed treatment mean in an instrument cell equals mean potential treatment under that support value under the local multi-instrument assumptions, for the support point when its observed cell has positive mass.hypothesesconclusionnormalizedRestrictedIntegral P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω))= ∫ ω, boolToReal (S.DofZ k ω) ∂P.μProof (Lean source)
theorem treatmentDrop [IsFiniteMeasure P.μ] (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) : normalizedRestrictedIntegral P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω)) = ∫ ω, boolToReal (S.DofZ k ω) ∂P.μ := by let h_proj : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => boolToReal ((f (0 : Fin 3)) : Bool) have hh_meas : Measurable h_proj := by -- Instance search no longer unfolds `cfCell` to see `n = 3`, so supply the -- coordinate measurable-space family at index type `Fin 3` directly. let _ : ∀ i : Fin 3, MeasurableSpace ((S.cfCell k).type i) := fun i => (S.cfCell k).inst i change Measurable fun f : ∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i => boolToReal ((f (0 : Fin 3)) : Bool) exact (by fun_prop : Measurable fun b : Bool => boolToReal b).comp (measurable_pi_apply (0 : Fin 3)) have hF_eq : ∀ ω ∈ S.zVar.event k, boolToReal (S.factualD ω) = h_proj ((S.cfCell k).jointValue ω) := by intro ω hω rw [← S.DofZ_eq_factualD_on_zEvent hA k hω] dsimp [h_proj] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl rw [hJV0] change normalizedRestrictedIntegral P.μ (S.zVar.event k) (fun ω => boolToReal (S.factualD ω)) = ∫ ω, boolToReal (S.DofZ k ω) ∂P.μ rw [POSystem.eventCondExp_of_ae_eq_IndepCF (hA.instrumentIndep k) (a := S.zVar) hh_meas (measurableSet_singleton k) (ae_restrict_of_forall_mem (μ := P.μ) (S.measurableSet_zEvent k) hF_eq) hZk (measure_ne_top _ _)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω dsimp [h_proj] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl rw [hJV0] -
outcomeDroptheorem — The observed outcome mean in an instrument cell equals mean outcome under the treatment induced by that support value under the local multi-instrument assumptions, for the support point, when its cell has positive mass and treated and untreated potential outcomes are integrable.hypothesesK :sharedℕIsFiniteMeasure P.μhA :S.Assumptionsk :Fin KhZk :P.μ (S.zEvent k) ≠ 0hY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μconclusionnormalizedRestrictedIntegral P.μ (S.zEvent k) S.factualY = ∫ ω, S.YofDofZ k ω ∂P.μProof (Lean source)
theorem outcomeDrop [IsFiniteMeasure P.μ] (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) : normalizedRestrictedIntegral P.μ (S.zEvent k) S.factualY = ∫ ω, S.YofDofZ k ω ∂P.μ := by have _hY1 : Integrable (S.YofD true) P.μ := hY1 have _hY0 : Integrable (S.YofD false) P.μ := hY0 let getD : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → Bool := fun f => ((f (0 : Fin 3)) : Bool) let getY1 : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => ((f (1 : Fin 3)) : ℝ) let getY0 : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => ((f (2 : Fin 3)) : ℝ) let h_proj : (∀ i : Fin (S.cfCell k).n, (S.cfCell k).type i) → ℝ := fun f => cond (getD f) (getY1 f) (getY0 f) have hh_meas : Measurable h_proj := by -- Instance search no longer unfolds `cfCell` to see `n = 3`, so supply the -- coordinate measurable-space family at index type `Fin 3` directly. let _ : ∀ i : Fin 3, MeasurableSpace ((S.cfCell k).type i) := fun i => (S.cfCell k).inst i have hD_meas : Measurable getD := by dsimp [getD] exact measurable_pi_apply (0 : Fin 3) have hY1_meas : Measurable getY1 := by dsimp [getY1] exact measurable_pi_apply (1 : Fin 3) have hY0_meas : Measurable getY0 := by dsimp [getY0] exact measurable_pi_apply (2 : Fin 3) have hif : Measurable fun f => if getD f = true then getY1 f else getY0 f := by refine Measurable.ite ?_ ?_ ?_ · exact hD_meas (MeasurableSet.singleton true) · exact hY1_meas · exact hY0_meas simpa [h_proj, Bool.cond_eq_ite] using hif have hF_eq : ∀ ω ∈ S.zVar.event k, S.factualY ω = h_proj ((S.cfCell k).jointValue ω) := by intro ω hω rw [S.factualY_eq_YofD_factualD hA ω, ← S.DofZ_eq_factualD_on_zEvent hA k hω] dsimp [h_proj, getD, getY1, getY0] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl have hJV1 : ((S.cfCell k).jointValue ω (1 : Fin 3) : ℝ) = S.YofD true ω := rfl have hJV2 : ((S.cfCell k).jointValue ω (2 : Fin 3) : ℝ) = S.YofD false ω := rfl rw [hJV0, hJV1, hJV2] cases S.DofZ k ω <;> simp change normalizedRestrictedIntegral P.μ (S.zVar.event k) S.factualY = ∫ ω, S.YofDofZ k ω ∂P.μ rw [POSystem.eventCondExp_of_ae_eq_IndepCF (hA.instrumentIndep k) (a := S.zVar) hh_meas (measurableSet_singleton k) (ae_restrict_of_forall_mem (μ := P.μ) (S.measurableSet_zEvent k) hF_eq) hZk (measure_ne_top _ _)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω dsimp [h_proj, getD, getY1, getY0] have hJV0 : ((S.cfCell k).jointValue ω (0 : Fin 3) : Bool) = S.DofZ k ω := rfl have hJV1 : ((S.cfCell k).jointValue ω (1 : Fin 3) : ℝ) = S.YofD true ω := rfl have hJV2 : ((S.cfCell k).jointValue ω (2 : Fin 3) : ℝ) = S.YofD false ω := rfl rw [hJV0, hJV1, hJV2] unfold YofDofZ cases S.DofZ k ω <;> simp -
gEvent_pairwise_disjointlemma — Distinct response-type subgroups are disjoint in a multiple-instrument IV subsystem, so latent types form nonoverlapping population cells.hypotheses -
gEvent_iUnionlemma — The response-type subgroups cover the full population in a multiple-instrument IV subsystem, so every unit belongs to exactly one latent treatment-response type.hypothesesconclusion(⋃ g : ResponseType K, S.gEvent g) = univProof (Lean source)
-
integral_partitionlemma — A population integral equals the sum of response-type masses times within-type means in a multiple-instrument IV subsystem, for an integrable quantity. This is the finite total law used to expand observed moments.hypothesesconclusion∫ ω, f ω ∂P.μProof (Lean source)
lemma integral_partition [IsFiniteMeasure P.μ] {f : P.Ω → ℝ} (hf : Integrable f P.μ) : ∫ ω, f ω ∂P.μ = ∑ g : ResponseType K, (P.μ (S.gEvent g)).toReal * normalizedRestrictedIntegral P.μ (S.gEvent g) f := integral_eq_sum_measure_mul_eventCondExp P.μ S.gEvent S.measurableSet_gEvent S.gEvent_pairwise_disjoint S.gEvent_iUnion f hf -
mass_nonneglemma — Every response-type mass is nonnegative in a multiple-instrument IV subsystem, for the selected response type, because it is a population probability.hypothesesconclusion0 ≤ S.mass gProof (Lean source)
lemma mass_nonneg (g : ResponseType K) : 0 ≤ S.mass g := ENNReal.toReal_nonneg -
mass_sum_onelemma — Response-type masses sum to one in a multiple-instrument IV subsystem, so they form population weights over the exhaustive latent-type partition.hypothesesconclusion∑ g : ResponseType K, S.mass g = 1Proof (Lean source)
lemma mass_sum_one : ∑ g : ResponseType K, S.mass g = 1 := by have hsum : (Finset.univ).sum (fun g : ResponseType K => (P.μ (S.responseType ⁻¹' ({g} : Set (ResponseType K)))).toReal) = (P.μ (S.responseType ⁻¹' (Set.univ : Set (ResponseType K)))).toReal := by simpa [Measure.real] using (MeasureTheory.sum_measureReal_preimage_singleton (μ := P.μ) (s := (Finset.univ : Finset (ResponseType K))) (f := S.responseType) (hf := by intro g _hg exact S.measurable_responseType (measurableSet_singleton g)) (h := by intro g _hg exact measure_ne_top _ _)) simpa [mass, gEvent, Set.preimage_univ, IsProbabilityMeasure.measure_univ] using hsum -
telescoped_eqlemma — Cumulative adjacent treatment changes equal the response difference between a support point and the reference point in a multiple-instrument IV subsystem, for a nonempty support, response type, and support point.hypothesesconclusionResponseTypeStats.PopulationBridge.telescopedTypeStep g k= boolToReal (g k) - boolToReal (g (S.z0 hK))Proof (Lean source)
lemma telescoped_eq (hK : 0 < K) (g : ResponseType K) (k : Fin K) : ResponseTypeStats.PopulationBridge.telescopedTypeStep g k = boolToReal (g k) - boolToReal (g (S.z0 hK)) := by classical let a : ℕ → ℝ := fun n => if h : n < K then boolToReal (g ⟨n, h⟩) else 0 have htel : ∀ n : ℕ, (∑ r ∈ range n, (a (r + 1) - a r)) = a n - a 0 := by intro n induction n with | zero => simp | succ n ih => rw [Finset.sum_range_succ, ih] ring have hsum : (∑ j ∈ (Finset.univ.filter fun j : Adj K => j.1.val ≤ k.val), typeStep g j) = ∑ r ∈ range k.val, (a (r + 1) - a r) := by refine Finset.sum_nbij (fun j : Adj K => j.1.val - 1) ?_ ?_ ?_ ?_ · intro j hj have hjle : j.1.val ≤ k.val := by simpa using hj rw [Finset.mem_range] have hpos : 0 < j.1.val := j.2 omega · intro j1 hj1 j2 hj2 h apply Subtype.ext apply Fin.ext have hj1le : j1.1.val ≤ k.val := by simpa using hj1 have hj2le : j2.1.val ≤ k.val := by simpa using hj2 have hpos1 : 0 < j1.1.val := j1.2 have hpos2 : 0 < j2.1.val := j2.2 change j1.1.val - 1 = j2.1.val - 1 at h omega · intro r hr have hrlt : r < k.val := by simpa using hr refine ⟨⟨⟨r + 1, ?_⟩, ?_⟩, ?_, ?_⟩ · exact Nat.lt_of_le_of_lt (succ_le_of_lt hrlt) k.isLt · exact Nat.succ_pos r · refine Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩ show r + 1 ≤ k.val omega · change r + 1 - 1 = r omega · intro j hj have hjle : j.1.val ≤ k.val := by simpa using hj have hsucc : j.1.val - 1 + 1 = j.1.val := Nat.sub_add_cancel (succ_le_of_lt j.2) have hpred_lt : j.1.val - 1 < K := Nat.lt_of_le_of_lt (sub_le _ _) j.1.isLt simp [typeStep, Adj.upper, Adj.lower, a, hpred_lt, hsucc] unfold ResponseTypeStats.PopulationBridge.telescopedTypeStep rw [Finset.sum_ite] simp only [Finset.sum_const_zero, add_zero] rw [hsum, htel] have hak : a k.val = boolToReal (g k) := by simp [a, k.isLt] have ha0 : a 0 = boolToReal (g (S.z0 hK)) := by simp [a, hK, z0] rw [hak, ha0] -
treatment_cell_eqtheorem — The observed treatment mean in an instrument cell equals the common baseline treatment mean plus its response-type treatment expansion for a nonempty support, under the local IV assumptions, at a support point whose cell has positive mass.hypothesesconclusionnormalizedRestrictedIntegral P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω))= S.baseTreatment hK + (S.toPopulationBridge hK).treatmentAtSupport kProof (Lean source)
theorem treatment_cell_eq [IsFiniteMeasure P.μ] (hK : 0 < K) (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) : normalizedRestrictedIntegral P.μ (S.zEvent k) (fun ω => boolToReal (S.factualD ω)) = S.baseTreatment hK + (S.toPopulationBridge hK).treatmentAtSupport k := by have hDint : ∀ q : Fin K, Integrable (fun ω => boolToReal (S.DofZ q ω)) P.μ := by intro q have hbdd : ∀ ω, |boolToReal (S.DofZ q ω)| ≤ (1 : ℝ) := by intro ω cases S.DofZ q ω <;> simp [boolToReal] exact (MeasureTheory.integrable_const (1 : ℝ)).mono' (((by fun_prop : Measurable fun b : Bool => boolToReal b).comp (S.measurable_DofZ q)).aestronglyMeasurable) (Filter.Eventually.of_forall hbdd) have hCell : ∀ (q : Fin K) (g : ResponseType K), S.mass g * normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => boolToReal (S.DofZ q ω)) = S.mass g * boolToReal (g q) := by intro q g calc S.mass g * normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => boolToReal (S.DofZ q ω)) = normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => boolToReal (S.DofZ q ω)) * S.mass g := by ring _ = ∫ ω in S.gEvent g, boolToReal (S.DofZ q ω) ∂P.μ := by rw [mass, eventCondExp_mul_measure_toReal _ _ (measure_ne_top _ _)] _ = ∫ ω in S.gEvent g, boolToReal (g q) ∂P.μ := by refine MeasureTheory.setIntegral_congr_fun (S.measurableSet_gEvent g) ?_ intro ω hω dsimp rw [S.DofZ_eq_on_gEvent g q hω] _ = boolToReal (g q) * S.mass g := by simp [mass, Measure.real, mul_comm] _ = S.mass g * boolToReal (g q) := by ring have hInt : ∫ ω, boolToReal (S.DofZ k ω) ∂P.μ = ∑ g : ResponseType K, S.mass g * boolToReal (g k) := by rw [S.integral_partition (hDint k)] refine Finset.sum_congr rfl ?_ intro g _ simpa [mass] using hCell k g have hBase : S.baseTreatment hK = ∑ g : ResponseType K, S.mass g * boolToReal (g (S.z0 hK)) := by unfold baseTreatment rw [S.integral_partition (hDint (S.z0 hK))] refine Finset.sum_congr rfl ?_ intro g _ simpa [mass] using hCell (S.z0 hK) g have hTreat : (S.toPopulationBridge hK).treatmentAtSupport k = ∑ g : ResponseType K, S.mass g * (boolToReal (g k) - boolToReal (g (S.z0 hK))) := by unfold ResponseTypeStats.PopulationBridge.treatmentAtSupport toPopulationBridge toStats refine Finset.sum_congr rfl ?_ intro g _ rw [S.telescoped_eq hK g k] rw [S.treatmentDrop hA k hZk, hInt, hBase, hTreat] rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl ?_ intro g _ ring -
outcome_cell_eqtheorem — The observed outcome mean in an instrument cell equals its response-type outcome expansion for a nonempty support, under the local IV assumptions, at a support point whose cell has positive mass, with integrable treated and untreated potential outcomes.hypothesesK :sharedℕIsFiniteMeasure P.μhK :0 < KhA :S.Assumptionsk :Fin KhZk :P.μ (S.zEvent k) ≠ 0hY1 :Integrable (S.YofD true) P.μhY0 :Integrable (S.YofD false) P.μconclusionnormalizedRestrictedIntegral P.μ (S.zEvent k) S.factualY= (S.toPopulationBridge hK).outcomeAtSupport kProof (Lean source)
theorem outcome_cell_eq [IsFiniteMeasure P.μ] (hK : 0 < K) (hA : S.Assumptions) (k : Fin K) (hZk : P.μ (S.zEvent k) ≠ 0) (hY1 : Integrable (S.YofD true) P.μ) (hY0 : Integrable (S.YofD false) P.μ) : normalizedRestrictedIntegral P.μ (S.zEvent k) S.factualY = (S.toPopulationBridge hK).outcomeAtSupport k := by have hYDZ_bdd : ∀ q : Fin K, ∀ ω, |S.YofDofZ q ω| ≤ |S.YofD true ω| + |S.YofD false ω| := by intro q ω have h1 := abs_nonneg (S.YofD true ω) have h0 := abs_nonneg (S.YofD false ω) unfold YofDofZ cases S.DofZ q ω <;> simp [h1, h0] have hYDZ_int : ∀ q : Fin K, Integrable (S.YofDofZ q) P.μ := by intro q exact (hY1.norm.add hY0.norm).mono' (S.measurable_YofDofZ q).aestronglyMeasurable (Filter.Eventually.of_forall (hYDZ_bdd q)) have hCE : ∀ (q : Fin K) (g : ResponseType K), normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofDofZ q) = normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofD false) + boolToReal (g q) * S.effect g := by intro q g let c : ℝ := boolToReal (g q) have hcongr : normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofDofZ q) = normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => S.YofD false ω + c * (S.YofD true ω - S.YofD false ω)) := by apply eventCondExp_congr_on P.μ (S.measurableSet_gEvent g) intro ω hω unfold YofDofZ rw [S.DofZ_eq_on_gEvent g q hω] dsimp [c] cases g q <;> simp [boolToReal] calc normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofDofZ q) = normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => S.YofD false ω + c * (S.YofD true ω - S.YofD false ω)) := hcongr _ = normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofD false) + normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => c * (S.YofD true ω - S.YofD false ω)) := by change normalizedRestrictedIntegral P.μ (S.gEvent g) ((S.YofD false) + fun ω => c * (S.YofD true ω - S.YofD false ω)) = normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofD false) + normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => c * (S.YofD true ω - S.YofD false ω)) rw [eventCondExp_add] · exact hY0.integrableOn · exact (hY1.integrableOn.sub hY0.integrableOn).const_mul c _ = normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofD false) + c * normalizedRestrictedIntegral P.μ (S.gEvent g) (fun ω => S.YofD true ω - S.YofD false ω) := by rw [eventCondExp_smul] _ = normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofD false) + boolToReal (g q) * S.effect g := by rfl have hTerm : ∀ g : ResponseType K, normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofDofZ k) = S.baseOutcome hK g + ResponseTypeStats.PopulationBridge.telescopedTypeStep g k * S.effect g := by intro g unfold baseOutcome rw [hCE k g, hCE (S.z0 hK) g, S.telescoped_eq hK g k] ring have hInt : ∫ ω, S.YofDofZ k ω ∂P.μ = ∑ g : ResponseType K, S.mass g * normalizedRestrictedIntegral P.μ (S.gEvent g) (S.YofDofZ k) := by rw [S.integral_partition (hYDZ_int k)] refine Finset.sum_congr rfl ?_ intro g _ rfl rw [S.outcomeDrop hA k hZk hY1 hY0, hInt] unfold ResponseTypeStats.PopulationBridge.outcomeAtSupport toPopulationBridge toStats refine Finset.sum_congr rfl ?_ intro g _ rw [hTerm g] -
rho_eq_zMasslemma — The ordered index's support masses equal the observed instrument-cell probabilities for the supplied score, its monotonicity certificate, and the selected support point in the multiple-instrument IV subsystem.