PO.ID.Exact.VariableIntensityIV
Variable-intensity instrumental variables: directed-pair Wald identification of an average causal response over ordered treatment margins; the general multivalued-instrument population 2SLS characterization is not derived.
OrderedTreatment 8 core · 3 supporting For a treatment with ordered levels 0, 1, …, J, margin j is the step from level j to level j + 1. ★ ordered_telescope_identity
Telescoping over the margins of an ordered treatment
For a treatment with ordered levels 0, 1, …, J, margin j is the step from level j to level j + 1. A move from level a to level b ≥ a crosses margin j exactly when a ≤ j < b, and the change of any response schedule f between the two levels is the sum of its one-step increments over the crossed margins: f(b) − f(a) = Σ_j (f(j + 1) − f(j))·1{a ≤ j < b}. Taking f to be the numeric level gives b − a = the number of margins crossed. These identities turn a dose contrast into margin-specific responses in the variable-intensity instrumental-variable results.
Main definitions
lowerLevel,upperLevel,intensityValue— the endpoints of a margin and the numeric level.marginIncrement— the increment f(j + 1) − f(j) of a schedule across margin j.Crossing,crossingIndicator— whether a move from a to b crosses margin j, and its 0/1 value.normalizedWeight— a weight divided by the total weight, as inStat.Weighted.
Main results
* ordered_telescope_indicator — f(b) − f(a) as the sum of increments over crossed margins.
* ordered_telescope_identity — b − a equals the number of crossed margins.
* normalizedWeight_nonneg, sum_normalizedWeight_eq_one — normalized weights are nonnegative
and sum to one when the raw weights are nonnegative with positive total.
The lower endpoint of a treatment margin is the level immediately below that margin on a scale with the stated number of adjacent margins.
The upper endpoint of a treatment margin is the level immediately above that margin on a scale with the stated number of adjacent margins.
Numeric treatment intensity is the real-valued rank of an ordered treatment level on a scale with the stated number of margins.
Definition (Lean source)
A margin increment measures how a real response schedule changes across one adjacent treatment margin on the ordered scale.
Definition (Lean source)
A treatment move crosses a margin exactly when its initial level is below that margin and its final level is at or above it on the ordered scale.
Definition (Lean source)
The margin-crossing indicator assigns one when movement from an initial level to a final level crosses the chosen margin, and zero otherwise, on the ordered scale.
Ordered telescoping for treatment intensity. The numeric increase between two ordered treatment levels equals the number of margins crossed on a finite ordered scale, for the initial and final levels under the condition that treatment weakly increases.
Formal statement
Proof (Lean source)
A normalized finite weight is one raw weight from a finite index set, drawn from the supplied weight schedule, divided by total raw weight.
Definition (Lean source)
3 supporting declarations (lemmas, instances)
-
ordered_telescope_indicatorlemma — The change in a response schedule between two ordered treatment levels equals the sum of its increments over exactly the crossed margins for a finite ordered scale, the response schedule, the initial and final levels, and their ordering. This converts level contrasts into margin-specific causal responses.hypothesesconclusionProof (Lean source)
lemma ordered_telescope_indicator {J : ℕ} (f : Fin (J + 1) → ℝ) {a b : Fin (J + 1)} (hab : a ≤ b) : f b - f a = ∑ j : Fin J, marginIncrement f j * crossingIndicator a b j := by classical let F : ℕ → ℝ := fun n => if h : n < J + 1 then f ⟨n, h⟩ else 0 have hNat : a.val ≤ b.val := (Fin.val_fin_le).2 hab calc f b - f a = F b.val - F a.val := by have haJ : a.val ≤ J := Nat.le_of_lt_succ a.isLt have hbJ : b.val ≤ J := Nat.le_of_lt_succ b.isLt simp [F, haJ, hbJ] _ = ∑ i ∈ Ico a.val b.val, (F (i + 1) - F i) := by rw [Finset.sum_Ico_sub F hNat] _ = ∑ j : Fin J, marginIncrement f j * crossingIndicator a b j := by have hIco : Ico a.val b.val = (range J).filter (fun x => a.val ≤ x ∧ x < b.val) := by ext x simp [Finset.mem_Ico] omega rw [hIco, Finset.sum_filter, Finset.sum_fin_eq_sum_range] apply Finset.sum_congr rfl intro x hx have hxJ : x < J := by simpa using hx have hxleJ : x ≤ J := by omega simp [F, marginIncrement, lowerLevel, upperLevel, crossingIndicator_eq_ite_val, hxJ, hxleJ] -
normalizedWeight_nonneglemma — Every normalized weight is nonnegative when the finite index set carries raw weights that are all nonnegative with positive total, for the selected index.hypothesesconclusion0 ≤ normalizedWeight a iProof (Lean source)
lemma normalizedWeight_nonneg {ι : Type*} [Fintype ι] (a : ι → ℝ) (ha : ∀ i, 0 ≤ a i) (hsum : 0 < ∑ i, a i) (i : ι) : 0 ≤ normalizedWeight a i := by exact normalizedWeight_nonneg a ha hsum i -
sum_normalizedWeight_eq_onelemma — Normalized weights sum to one when the finite index set carries raw weights with positive total, so they form averaging weights.hypothesesconclusion∑ i, normalizedWeight a i = 1Proof (Lean source)
lemma sum_normalizedWeight_eq_one {ι : Type*} [Fintype ι] (a : ι → ℝ) (hsum : 0 < ∑ i, a i) : ∑ i, normalizedWeight a i = 1 := by exact sum_normalizedWeight_eq_one a hsum.ne'