Panel

Cells 2 core · 1 supporting This file provides the observed-cell substrate for panel regressions: a finite set of observed unit-period cells with strictly positive normalized weights. ★ balanced_weight

Observed Panel Cells

This file provides the observed-cell substrate for panel regressions: a finite set of observed unit-period cells with strictly positive normalized weights. It specializes the generic weighted-support infrastructure to panel cell indices and supplies the balanced-panel constructor. It mirrors Definition 2.1 of the projection note.

Relation to Causalean.Panel.CellBridge. Both files use the word cell, but for different objects. Here a cell is a discrete index r = (i, t) ∈ I × T carrying a positive normalized weight — a finite-weighted-support object with no measure theory. In CellBridge a cell is a measurable level set {ω | G ω = g} of an observable map on a probability space. The two share no declarations and neither imports the other; the only common substrate is Causalean.Panel.Weighted.IndicatorSpan.

abbrev Cells reviewed

Causalean.Panel

Observed cells of a panel together with positive normalized weights.

Definition (Lean source)

abbrev Cells [Fintype I] [Fintype T] [DecidableEq I] [DecidableEq T] : Type _ := WeightedSupport (I × T)

Causalean.Panel.Cells · Causalean/Panel/Cells.lean:56

lemma balanced_weight reviewed

Causalean.Panel.Cells

For any unit-period cell r, the balanced panel design assigns it weight equal to one divided by the total number of unit-period cells.

Formal statement

hypotheses

r :

I × T

conclusion

(balanced (I := I) (T := T)).weight r = (1 : ℝ) / (card I * card T)

Proof (Lean source)

@[simp] lemma balanced_weight (r : I × T) : (balanced (I := I) (T := T)).weight r = (1 : ℝ) / (card I * card T) := rfl

Causalean.Panel.Cells.balanced_weight · Causalean/Panel/Cells.lean:116 · uses balanced

1 supporting declaration (lemmas, instances)

balanced_observed lemma — The balanced panel observes every unit-period cell.

conclusion

(balanced (I := I) (T := T)).observed = univ

Proof (Lean source)

@[simp] lemma balanced_observed : (balanced (I := I) (T := T)).observed = univ := rfl

Causalean.Panel.Cells.balanced_observed · Causalean/Panel/Cells.lean:112

WeightedTwoWayPanel 11 core · 9 supporting Paper-agnostic finite-sum infrastructure for two-way panels under a general unit weight p : Unit → ℝ (a pmf: ∑ p = 1, 0 < p i) with a uniform period measure. ★ ddot_orthogonal_unit_time★ ddot_eq_residualize

Weighted Finite Two-Way Panel Helpers

Paper-agnostic finite-sum infrastructure for two-way panels under a general unit weight p : Unit → ℝ (a pmf: ∑ p = 1, 0 < p i) with a uniform period measure. This is the share-weighted generalization of the uniform two-way panel algebra used by the estimand-characterization modules:

uniform balanced panels recover the old UniformTwoWayPanel by p ≡ 1/|Unit|;
Goodman-Bacon cohort-share panels take p = cohort shares.

It provides the p-weighted unit/time/grand means, double demeaning (ddot), the p-weighted inner product, the unit/time additive nuisance class, the reconstruction identity, and the share-weighted orthogonality theorems (ddot ⟂ unit / time / additive).

Bridge to the generic `WeightedSupport` FWL tower

The closed forms above are connected to the abstract Frisch–Waugh–Lovell substrate in Causalean/Panel/Weighted/ by the Bridge section: the panel is the cell support R = Unit × Time with weight ω_{(i,t)} = p_i / |Time| (cellSupport), the p-weighted inner product is |Time| times WeightedSupport.ip (inner_eq_card_smul_ip), and ddot is the generic residual maker against the two-axis additive span (ddot_eq_residualize). The abstract FWL coefficient lemma Weighted.WeightedSupport.scalar_fwl_of_normalEqs is thus reusable through the bridge.

structure UnitWeights reviewed

Causalean.Panel.WeightedTwoWayPanel

Unit weights. A weight function p assigning each unit a share that forms a probability vector: every unit's weight is strictly positive and the weights sum to one across units.

Definition (Lean source)

parameters

Unit :

Type*

Fintype Unit

fields

p :

Unit → ℝ

pos :

∀ i, 0 < p i

sum_one :

∑ i, p i = 1

Causalean.Panel.WeightedTwoWayPanel.UnitWeights · Causalean/Panel/WeightedTwoWayPanel.lean:52

def unitMean reviewed

Causalean.Panel.WeightedTwoWayPanel

Unit mean \bar V_{i·} under the uniform period measure (weight-free in time).

Definition (Lean source)

noncomputable def unitMean (V : Unit → Time → ℝ) (i : Unit) : ℝ := (Fintype.card Time : ℝ)⁻¹ * ∑ t, V i t

Causalean.Panel.WeightedTwoWayPanel.unitMean · Causalean/Panel/WeightedTwoWayPanel.lean:62

def timeMean reviewed

Causalean.Panel.WeightedTwoWayPanel

p-weighted time mean \bar V_{·t} = ∑_i p_i V_{it}.

Definition (Lean source)

noncomputable def timeMean (w : UnitWeights Unit) (V : Unit → Time → ℝ) (t : Time) : ℝ := ∑ i, w.p i * V i t

Causalean.Panel.WeightedTwoWayPanel.timeMean · Causalean/Panel/WeightedTwoWayPanel.lean:66 · uses UnitWeights

def grandMean reviewed

Causalean.Panel.WeightedTwoWayPanel

p-weighted grand mean \bar V = ∑_i p_i \bar V_{i·}.

Definition (Lean source)

noncomputable def grandMean (w : UnitWeights Unit) (V : Unit → Time → ℝ) : ℝ := ∑ i, w.p i * unitMean V i

Causalean.Panel.WeightedTwoWayPanel.grandMean · Causalean/Panel/WeightedTwoWayPanel.lean:70 · uses UnitWeights

def ddot reviewed

Causalean.Panel.WeightedTwoWayPanel

Two-way residual / double-demeaned array under the p-weighted means.

Definition (Lean source)

noncomputable def ddot (w : UnitWeights Unit) (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ℝ := V i t - unitMean V i - timeMean w V t + grandMean w V

Causalean.Panel.WeightedTwoWayPanel.ddot · Causalean/Panel/WeightedTwoWayPanel.lean:74 · uses UnitWeights

def inner reviewed

Causalean.Panel.WeightedTwoWayPanel

p-weighted finite-panel inner product (uniform-time normalizer dropped as harmless).

Definition (Lean source)

noncomputable def inner (w : UnitWeights Unit) (V W : Unit → Time → ℝ) : ℝ := ∑ i, ∑ t, w.p i * (V i t * W i t)

Causalean.Panel.WeightedTwoWayPanel.inner · Causalean/Panel/WeightedTwoWayPanel.lean:78 · uses UnitWeights

abbrev IsUnitTimeAdditive reviewed

Causalean.Panel.WeightedTwoWayPanel

Unit-time additive nuisance class h_it = a_i + b_t (shared predicate).

Definition (Lean source)

abbrev IsUnitTimeAdditive (h : Unit → Time → ℝ) : Prop := IsUnitTimeAdditive h

Causalean.Panel.WeightedTwoWayPanel.IsUnitTimeAdditive · Causalean/Panel/WeightedTwoWayPanel.lean:83

def unitTimeProjection reviewed

Causalean.Panel.WeightedTwoWayPanel

The unit/time component removed by double demeaning.

Definition (Lean source)

noncomputable def unitTimeProjection (w : UnitWeights Unit) (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ℝ := unitMean V i + timeMean w V t - grandMean w V

Causalean.Panel.WeightedTwoWayPanel.unitTimeProjection · Causalean/Panel/WeightedTwoWayPanel.lean:87 · uses UnitWeights

theorem ddot_orthogonal_unit_time reviewed

Causalean.Panel.WeightedTwoWayPanel

Double-demeaned arrays are orthogonal to every unit/time additive nuisance function. For a probability-weighted panel of units and periods, any array that decomposes as the sum of a unit-specific term and a time-specific term is orthogonal, under the p-weighted inner product, to the double-demeaned residual of any panel array V: their weighted inner product is zero.

Formal statement

hypotheses

w :

UnitWeights Unit

V h :

Unit → Time → ℝ

hh :

IsUnitTimeAdditive h

conclusion

inner w (ddot w V) h = 0

Proof (Lean source)

theorem ddot_orthogonal_unit_time (w : UnitWeights Unit) (V h : Unit → Time → ℝ) (hh : IsUnitTimeAdditive h) : inner w (ddot w V) h = 0 := by rcases hh with ⟨a, b, hh⟩ unfold inner calc ∑ i, ∑ t, w.p i * (ddot w V i t * h i t) = ∑ i, ∑ t, w.p i * (ddot w V i t * (a i + b t)) := by simp [hh] _ = (∑ i, ∑ t, w.p i * (ddot w V i t * a i)) + (∑ i, ∑ t, w.p i * (ddot w V i t * b t)) := by simp [mul_add, Finset.sum_add_distrib] _ = 0 := by rw [ddot_orthogonal_unit w V a, ddot_orthogonal_time w V b, zero_add]

Causalean.Panel.WeightedTwoWayPanel.ddot_orthogonal_unit_time · Causalean/Panel/WeightedTwoWayPanel.lean:233 · uses IsUnitTimeAdditive , UnitWeights , ddot , inner

def cellSupport reviewed

Causalean.Panel.WeightedTwoWayPanel

The panel viewed as a cell-indexed weighted support on R = Unit × Time with the factorized weight ω_{(i,t)} = p_i / |Time| (every cell observed).

Definition (Lean source)

noncomputable def cellSupport (w : UnitWeights Unit) : WeightedSupport (Unit × Time) where observed := univ observed_nonempty := Finset.univ_nonempty weight r := w.p r.1 / (Fintype.card Time : ℝ) weight_pos := by intro r _ have hT : (0 : ℝ) < (Fintype.card Time : ℝ) := by exact_mod_cast Fintype.card_pos exact div_pos (w.pos r.1) hT weight_zero_off := by intro r hr; exact (hr (Finset.mem_univ r)).elim weight_sum_one := by have hT : (Fintype.card Time : ℝ) ≠ 0 := by have h := Fintype.card_pos (α := Time) exact_mod_cast h.ne' rw [Fintype.sum_prod_type] have hrow : ∀ i : Unit, (∑ _t : Time, w.p i / (Fintype.card Time : ℝ)) = w.p i := by intro i rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] field_simp simp_rw [hrow] exact w.sum_one

Causalean.Panel.WeightedTwoWayPanel.cellSupport · Causalean/Panel/WeightedTwoWayPanel.lean:273 · uses WeightedSupport , UnitWeights

theorem ddot_eq_residualize reviewed

Causalean.Panel.WeightedTwoWayPanel

Concrete ↔ abstract bridge. For unit weights w and an outcome array V, the closed-form two-way double-demeaned residual ddot w V i t equals the generic weighted-support residual against the two-axis additive span, evaluated at cell (i, t). Every cell is observed, so the identity holds pointwise.

Formal statement

hypotheses

w :

UnitWeights Unit

V :

Unit → Time → ℝ

i :

Unit

t :

Time

conclusion

(cellSupport w).residualize (twoAxisAdditiveSpan Unit Time) (fun r => V r.1 r.2) (i, t)

= ddot w V i t

Proof (Lean source)

theorem ddot_eq_residualize (w : UnitWeights Unit) (V : Unit → Time → ℝ) (i : Unit) (t : Time) : (cellSupport w).residualize (twoAxisAdditiveSpan Unit Time) (fun r => V r.1 r.2) (i, t) = ddot w V i t := by classical set c : WeightedSupport (Unit × Time) := cellSupport w with hc set H := twoAxisAdditiveSpan Unit Time with hH set X : Unit × Time → ℝ := fun r => V r.1 r.2 with hX set Y : Unit × Time → ℝ := fun r => unitTimeProjection w V r.1 r.2 with hY have hYmem : Y ∈ H := by rw [hH, mem_twoAxisAdditiveSpan_iff] exact unitTimeProjection_additive w V have hT : (0 : ℝ) < (Fintype.card Time : ℝ) := by exact_mod_cast Fintype.card_pos have hTne : (Fintype.card Time : ℝ) ≠ 0 := ne_of_gt hT have hXY : ∀ r : Unit × Time, (X - Y) r = ddot w V r.1 r.2 := by intro r have h := sub_ddot_eq_unitTimeProjection w V r.1 r.2 simp only [hX, hY, Pi.sub_apply] linarith [h] have horth : ∀ h ∈ H, c.ip (X - Y) h = 0 := by intro h hh have hadd : IsUnitTimeAdditive (fun i t => h (i, t)) := (mem_twoAxisAdditiveSpan_iff).mp (hH ▸ hh) have hkey : inner w (ddot w V) (fun i t => h (i, t)) = 0 := ddot_orthogonal_unit_time w V (fun i t => h (i, t)) hadd have hbridge : inner w (ddot w V) (fun i t => h (i, t)) = (Fintype.card Time : ℝ) * c.ip (fun r => ddot w V r.1 r.2) (fun r => h (r.1, r.2)) := by rw [hc] exact inner_eq_card_smul_ip w (ddot w V) (fun i t => h (i, t)) have hXYfun : (fun r : Unit × Time => ddot w V r.1 r.2) = X - Y := by funext r exact (hXY r).symm have hhfun : (fun r : Unit × Time => h (r.1, r.2)) = h := by funext r rfl rw [hXYfun, hhfun] at hbridge rw [hbridge] at hkey exact (mul_eq_zero.mp hkey).resolve_left hTne have hproj : c.proj H X (i, t) = Y (i, t) := c.proj_apply_eq_of_mem_orthogonal H X hYmem horth (i, t) (by rw [hc] exact Finset.mem_univ _) simp only [WeightedSupport.residualize_apply, Pi.sub_apply, hproj] have h := hXY (i, t) simp only [hX, hY, Pi.sub_apply] at h linarith [h]

Causalean.Panel.WeightedTwoWayPanel.ddot_eq_residualize · Causalean/Panel/WeightedTwoWayPanel.lean:349 · uses residualize , twoAxisAdditiveSpan , UnitWeights , cellSupport , ddot

9 supporting declarations (lemmas, instances)

ddot_reconstruct theorem — Reconstruction identity V_it = ddot V_it + unitMean + timeMean - grandMean.

hypotheses

w :

UnitWeights Unit

V :

Unit → Time → ℝ

i :

Unit

t :

Time

conclusion

ddot w V i t + unitMean V i + timeMean w V t - grandMean w V = V i t

Proof (Lean source)

theorem ddot_reconstruct (w : UnitWeights Unit) (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ddot w V i t + unitMean V i + timeMean w V t - grandMean w V = V i t := by unfold ddot ring

Causalean.Panel.WeightedTwoWayPanel.ddot_reconstruct · Causalean/Panel/WeightedTwoWayPanel.lean:92
unitTimeProjection_additive theorem — The removed component is itself unit/time additive.

hypotheses

w :

UnitWeights Unit

V :

Unit → Time → ℝ

conclusion

IsUnitTimeAdditive (unitTimeProjection w V)

Proof (Lean source)

theorem unitTimeProjection_additive (w : UnitWeights Unit) (V : Unit → Time → ℝ) : IsUnitTimeAdditive (unitTimeProjection w V) := by refine ⟨unitMean V, fun t => timeMean w V t - grandMean w V, ?_⟩ intro i t unfold unitTimeProjection ring

Causalean.Panel.WeightedTwoWayPanel.unitTimeProjection_additive · Causalean/Panel/WeightedTwoWayPanel.lean:98
sub_ddot_eq_unitTimeProjection theorem — Pointwise residual decomposition V - ddot V into the unit/time projection.

hypotheses

w :

UnitWeights Unit

V :

Unit → Time → ℝ

i :

Unit

t :

Time

conclusion

V i t - ddot w V i t = unitTimeProjection w V i t

Proof (Lean source)

theorem sub_ddot_eq_unitTimeProjection (w : UnitWeights Unit) (V : Unit → Time → ℝ) (i : Unit) (t : Time) : V i t - ddot w V i t = unitTimeProjection w V i t := by unfold ddot unitTimeProjection ring

Causalean.Panel.WeightedTwoWayPanel.sub_ddot_eq_unitTimeProjection · Causalean/Panel/WeightedTwoWayPanel.lean:106
ddot_orthogonal_unit theorem — Double-demeaned arrays are orthogonal (in the p-weighted inner product) to arbitrary unit-only functions.

hypotheses

w :

UnitWeights Unit

V :

Unit → Time → ℝ

a :

Unit → ℝ

conclusion

∑ i, ∑ t, w.p i * (ddot w V i t * a i) = 0

Proof (Lean source)

theorem ddot_orthogonal_unit (w : UnitWeights Unit) (V : Unit → Time → ℝ) (a : Unit → ℝ) : ∑ i, ∑ t, w.p i * (ddot w V i t * a i) = 0 := by classical cases isEmpty_or_nonempty Time with | inl h => letI : IsEmpty Time := h simp | inr h => letI : Nonempty Time := h exact ddot_orthogonal_unit_of_card_ne_zero w (by positivity) V a

Causalean.Panel.WeightedTwoWayPanel.ddot_orthogonal_unit · Causalean/Panel/WeightedTwoWayPanel.lean:176
ddot_orthogonal_time theorem — Double-demeaned arrays are orthogonal (in the p-weighted inner product) to arbitrary time-only functions: ∑_i ∑_t p_i · ddot V_{it} · b_t = 0. Per-period the p-weighted unit sum of ddot vanishes (∑ p = 1 cancels the time mean against the grand mean).

hypotheses

w :

UnitWeights Unit

V :

Unit → Time → ℝ

b :

Time → ℝ

conclusion

∑ i, ∑ t, w.p i * (ddot w V i t * b t) = 0

Proof (Lean source)

theorem ddot_orthogonal_time (w : UnitWeights Unit) (V : Unit → Time → ℝ) (b : Time → ℝ) : ∑ i, ∑ t, w.p i * (ddot w V i t * b t) = 0 := by classical have hcol : ∀ t, ∑ i, w.p i * ddot w V i t = 0 := by intro t calc ∑ i, w.p i * ddot w V i t = ∑ i, (w.p i * V i t - w.p i * unitMean V i - w.p i * timeMean w V t + w.p i * grandMean w V) := by apply Finset.sum_congr rfl intro i _hi unfold ddot ring _ = ∑ i, w.p i * V i t - ∑ i, w.p i * unitMean V i - (∑ i, w.p i) * timeMean w V t + (∑ i, w.p i) * grandMean w V := by simp only [Finset.sum_sub_distrib, Finset.sum_add_distrib, Finset.sum_mul] _ = 0 := by rw [w.sum_one] unfold timeMean grandMean ring calc ∑ i, ∑ t, w.p i * (ddot w V i t * b t) = ∑ t, (∑ i, w.p i * ddot w V i t) * b t := by rw [Finset.sum_comm] apply Finset.sum_congr rfl intro t _ht calc ∑ i, w.p i * (ddot w V i t * b t) = ∑ i, (w.p i * ddot w V i t) * b t := by apply Finset.sum_congr rfl intro i _hi ring _ = (∑ i, w.p i * ddot w V i t) * b t := by rw [Finset.sum_mul] _ = 0 := by simp [hcol]

Causalean.Panel.WeightedTwoWayPanel.ddot_orthogonal_time · Causalean/Panel/WeightedTwoWayPanel.lean:190
cellSupport_weight lemma — The cell-support bridge assigns each unit-period cell its unit weight divided equally across periods.

hypotheses

w :

UnitWeights Unit

r :

Unit × Time

conclusion

(cellSupport w).weight r = w.p r.1 / (Fintype.card Time : ℝ)

Proof (Lean source)

@[simp] lemma cellSupport_weight (w : UnitWeights Unit) (r : Unit × Time) : (cellSupport w).weight r = w.p r.1 / (Fintype.card Time : ℝ) := rfl

Causalean.Panel.WeightedTwoWayPanel.cellSupport_weight · Causalean/Panel/WeightedTwoWayPanel.lean:302
cellSupport_observed lemma — Every unit-period cell is observed in the cell-support bridge.

hypotheses

w :

UnitWeights Unit

conclusion

(cellSupport w).observed = (Finset.univ : Finset (Unit × Time))

Proof (Lean source)

@[simp] lemma cellSupport_observed (w : UnitWeights Unit) : (cellSupport w).observed = (Finset.univ : Finset (Unit × Time)) := rfl

Causalean.Panel.WeightedTwoWayPanel.cellSupport_observed · Causalean/Panel/WeightedTwoWayPanel.lean:307
mem_twoAxisAdditiveSpan_iff lemma — Membership in the two-axis additive span is exactly the panel's IsUnitTimeAdditive predicate after uncurrying.

hypotheses

h :

Unit × Time → ℝ

conclusion

h ∈ twoAxisAdditiveSpan Unit Time ↔ IsUnitTimeAdditive (fun i t => h (i, t))

Proof (Lean source)

lemma mem_twoAxisAdditiveSpan_iff {h : Unit × Time → ℝ} : h ∈ twoAxisAdditiveSpan Unit Time ↔ IsUnitTimeAdditive (fun i t => h (i, t)) := by unfold twoAxisAdditiveSpan IsUnitTimeAdditive rw [AdditiveSpan.mem_iff] constructor · rintro ⟨a, b, hab⟩ exact ⟨a, b, fun i t => hab (i, t)⟩ · rintro ⟨a, b, hab⟩ refine ⟨a, b, ?_⟩ intro r simpa using hab r.1 r.2

Causalean.Panel.WeightedTwoWayPanel.mem_twoAxisAdditiveSpan_iff · Causalean/Panel/WeightedTwoWayPanel.lean:313
inner_eq_card_smul_ip theorem — The p-weighted panel inner product is |Time| times the generic weighted-support inner product on the cell support.

hypotheses

w :

UnitWeights Unit

V W :

Unit → Time → ℝ

conclusion

inner w V W
= (Fintype.card Time : ℝ) * (cellSupport w).ip (fun r => V r.1 r.2) (fun r => W r.1 r.2)

Proof (Lean source)

theorem inner_eq_card_smul_ip (w : UnitWeights Unit) (V W : Unit → Time → ℝ) : inner w V W = (Fintype.card Time : ℝ) * (cellSupport w).ip (fun r => V r.1 r.2) (fun r => W r.1 r.2) := by have hT : (Fintype.card Time : ℝ) ≠ 0 := by have h := Fintype.card_pos (α := Time) exact_mod_cast h.ne' simp only [inner, WeightedSupport.ip_def, cellSupport_observed, cellSupport_weight] rw [Fintype.sum_prod_type, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i _ rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro t _ field_simp

Causalean.Panel.WeightedTwoWayPanel.inner_eq_card_smul_ip · Causalean/Panel/WeightedTwoWayPanel.lean:327

AdoptionPath 9 core · 9 supporting This file provides finite-period adoption-path predicates for staggered-treatment designs, including eventual treatment, never treatment, and whether adoption has occurred by a period. ★ absorbingTreatment_eq

Adoption Path Helpers

This file provides finite-period adoption-path predicates for staggered-treatment designs, including eventual treatment, never treatment, and whether adoption has occurred by a period. The never-treated path is represented as an infinite adoption date, so absorbing treatment remains zero in every finite period for such units.

These paper-agnostic helpers are shared by staggered-adoption modules: Sun-Abraham path helpers wrap these declarations, and Goodman-Bacon uses the same raw infinite-date encoding for proof stability.

def finite reviewed

Causalean.Panel.AdoptionPath

A finite adoption path, embedded in WithTop (Fin T).

Definition (Lean source)

def finite {T : ℕ} (g : Fin T) : WithTop (Fin T) := (g : WithTop (Fin T))

Causalean.Panel.AdoptionPath.finite · Causalean/Panel/AdoptionPath.lean:35

def le reviewed

Causalean.Panel.AdoptionPath

Adoption-date predicate A ≤ t, i.e. adoption has occurred by period t.

Definition (Lean source)

def le {T : ℕ} (a : WithTop (Fin T)) (t : Fin T) : Prop := a ≤ (t : WithTop (Fin T))

Causalean.Panel.AdoptionPath.le · Causalean/Panel/AdoptionPath.lean:44

def lt reviewed

Causalean.Panel.AdoptionPath

Adoption-date predicate t < A, i.e. the path is untreated at period t.

Definition (Lean source)

def lt {T : ℕ} (a : WithTop (Fin T)) (t : Fin T) : Prop := (t : WithTop (Fin T)) < a

Causalean.Panel.AdoptionPath.lt · Causalean/Panel/AdoptionPath.lean:53

def isFinite reviewed

Causalean.Panel.AdoptionPath

The path is finite, i.e. eventually treated.

Definition (Lean source)

def isFinite {T : ℕ} (a : WithTop (Fin T)) : Prop := a ≠ ⊤

Causalean.Panel.AdoptionPath.isFinite · Causalean/Panel/AdoptionPath.lean:62

def isInfinite reviewed

Causalean.Panel.AdoptionPath

The path is infinite, i.e. never treated.

Definition (Lean source)

def isInfinite {T : ℕ} (a : WithTop (Fin T)) : Prop := a = ⊤

Causalean.Panel.AdoptionPath.isInfinite · Causalean/Panel/AdoptionPath.lean:70

def isNeverTreated reviewed

Causalean.Panel.AdoptionPath

A path is never treated when its adoption date is infinite.

Definition (Lean source)

def isNeverTreated {T : ℕ} (h : WithTop (Fin T)) : Prop := isInfinite h

Causalean.Panel.AdoptionPath.isNeverTreated · Causalean/Panel/AdoptionPath.lean:78

def isEventuallyTreated reviewed

Causalean.Panel.AdoptionPath

h < ∞, the path is eventually treated.

Definition (Lean source)

def isEventuallyTreated {T : ℕ} (h : WithTop (Fin T)) : Prop := isFinite h

Causalean.Panel.AdoptionPath.isEventuallyTreated · Causalean/Panel/AdoptionPath.lean:87

def absorbingTreatment reviewed

Causalean.Panel.AdoptionPath

Absorbing treatment path 1{h < ∞ and h ≤ t}. Since ⊤ ≤ t is false, the never-treated path is untreated in every finite period.

Definition (Lean source)

noncomputable def absorbingTreatment {T : ℕ} (h : WithTop (Fin T)) (t : Fin T) : ℝ := if le h t then 1 else 0

Causalean.Panel.AdoptionPath.absorbingTreatment · Causalean/Panel/AdoptionPath.lean:97

theorem absorbingTreatment_eq reviewed

Causalean.Panel.AdoptionPath

For an adoption date h and period t within a horizon of T periods, the absorbing treatment indicator equals one exactly when adoption has occurred by that period, and zero otherwise.

Formal statement

hypotheses

T :

ℕ

h :

WithTop (Fin T)

t :

Fin T

conclusion

absorbingTreatment h t = if h ≤ (t : WithTop (Fin T)) then 1 else 0

Proof (Lean source)

@[simp] theorem absorbingTreatment_eq {T : ℕ} (h : WithTop (Fin T)) (t : Fin T) : absorbingTreatment h t = if h ≤ (t : WithTop (Fin T)) then 1 else 0 := by unfold absorbingTreatment le by_cases hle : h ≤ (t : WithTop (Fin T)) <;> simp [hle]

Causalean.Panel.AdoptionPath.absorbingTreatment_eq · Causalean/Panel/AdoptionPath.lean:102 · uses absorbingTreatment

9 supporting declarations (lemmas, instances)

finite_eq theorem — Embedding a finite adoption period into the shared adoption-path type is definitionally the ordinary finite-period inclusion.

hypotheses

T :

ℕ

g :

Fin T

conclusion

finite g = (g : WithTop (Fin T))

Proof (Lean source)

@[simp] theorem finite_eq {T : ℕ} (g : Fin T) : finite g = (g : WithTop (Fin T)) := rfl

Causalean.Panel.AdoptionPath.finite_eq · Causalean/Panel/AdoptionPath.lean:39
le_eq theorem — The treated-by-period predicate is exactly the order comparison with the finite period viewed as an adoption date.

hypotheses

T :

ℕ

a :

WithTop (Fin T)

t :

Fin T

conclusion

le a t = (a ≤ (t : WithTop (Fin T)))

Proof (Lean source)

@[simp] theorem le_eq {T : ℕ} (a : WithTop (Fin T)) (t : Fin T) : le a t = (a ≤ (t : WithTop (Fin T))) := rfl

Causalean.Panel.AdoptionPath.le_eq · Causalean/Panel/AdoptionPath.lean:48
lt_eq theorem — The untreated-before-adoption predicate is exactly the strict order comparison with the finite period viewed as an adoption date.

hypotheses

T :

ℕ

a :

WithTop (Fin T)

t :

Fin T

conclusion

lt a t = ((t : WithTop (Fin T)) < a)

Proof (Lean source)

@[simp] theorem lt_eq {T : ℕ} (a : WithTop (Fin T)) (t : Fin T) : lt a t = ((t : WithTop (Fin T)) < a) := rfl

Causalean.Panel.AdoptionPath.lt_eq · Causalean/Panel/AdoptionPath.lean:57
isFinite_eq theorem — A path is eventually treated exactly when its adoption date is not infinite.

hypotheses

T :

ℕ

a :

WithTop (Fin T)

conclusion

isFinite a = (a ≠ ⊤)

Proof (Lean source)

@[simp] theorem isFinite_eq {T : ℕ} (a : WithTop (Fin T)) : isFinite a = (a ≠ ⊤) := rfl

Causalean.Panel.AdoptionPath.isFinite_eq · Causalean/Panel/AdoptionPath.lean:66
isInfinite_eq theorem — A path is never treated exactly when its adoption date is infinite.

hypotheses

T :

ℕ

a :

WithTop (Fin T)

conclusion

isInfinite a = (a = ⊤)

Proof (Lean source)

@[simp] theorem isInfinite_eq {T : ℕ} (a : WithTop (Fin T)) : isInfinite a = (a = ⊤) := rfl

Causalean.Panel.AdoptionPath.isInfinite_eq · Causalean/Panel/AdoptionPath.lean:74
isNeverTreated_eq theorem — The Sun-Abraham-compatible never-treated name is the infinite adoption-date predicate.

hypotheses

T :

ℕ

h :

WithTop (Fin T)

conclusion

isNeverTreated h = (h = ⊤)

Proof (Lean source)

@[simp] theorem isNeverTreated_eq {T : ℕ} (h : WithTop (Fin T)) : isNeverTreated h = (h = ⊤) := rfl

Causalean.Panel.AdoptionPath.isNeverTreated_eq · Causalean/Panel/AdoptionPath.lean:82
isEventuallyTreated_eq theorem — The Sun-Abraham-compatible eventually-treated name is the finite adoption-date predicate.

hypotheses

T :

ℕ

h :

WithTop (Fin T)

conclusion

isEventuallyTreated h = (h ≠ ⊤)

Proof (Lean source)

@[simp] theorem isEventuallyTreated_eq {T : ℕ} (h : WithTop (Fin T)) : isEventuallyTreated h = (h ≠ ⊤) := rfl

Causalean.Panel.AdoptionPath.isEventuallyTreated_eq · Causalean/Panel/AdoptionPath.lean:91
not_le_of_lt theorem — If t < A, then adoption has not occurred by t.

hypotheses

T :

ℕ
WithTop (Fin T)
Fin T

hlt :

lt a t

conclusion

¬ le a t

Proof (Lean source)

theorem not_le_of_lt {T : ℕ} {a : WithTop (Fin T)} {t : Fin T} (hlt : lt a t) : ¬ le a t := AdoptionDate.not_le_of_lt hlt

Causalean.Panel.AdoptionPath.not_le_of_lt · Causalean/Panel/AdoptionPath.lean:110
lt_of_isInfinite theorem — Never-treated paths are untreated in every finite period.

hypotheses

T :

ℕ
WithTop (Fin T)
Fin T

ha :

isInfinite a

conclusion

lt a t

Proof (Lean source)

theorem lt_of_isInfinite {T : ℕ} {a : WithTop (Fin T)} {t : Fin T} (ha : isInfinite a) : lt a t := AdoptionDate.lt_of_isInf ha

Causalean.Panel.AdoptionPath.lt_of_isInfinite · Causalean/Panel/AdoptionPath.lean:115

CellBridge 10 core · 6 supporting Provides measure-theoretic finite-cell bridge infrastructure for panel estimand characterizations. ★ integral_mul_twoAxisIndicatorSpan_eq_zero_of_axes

Provides measure-theoretic finite-cell bridge infrastructure for panel estimand characterizations. It defines cell indicators, indicator spans, cell masses, and finite-partition integral lemmas for observable cell maps.

abbrev finiteCellIndicator reviewed

Causalean.Panel.CellBridge

Finite-weighted-support cell indicator from Causalean.Panel.Weighted.IndicatorSpan.

Definition (Lean source)

abbrev finiteCellIndicator {R 𝒢 : Type*} [DecidableEq 𝒢] (G : R → 𝒢) (g : 𝒢) : R → ℝ := cellIndicator G g

Causalean.Panel.CellBridge.finiteCellIndicator · Causalean/Panel/CellBridge.lean:49

abbrev finiteIndicatorSpan reviewed

Causalean.Panel.CellBridge

Finite-weighted one-axis indicator span from Causalean.Panel.Weighted.IndicatorSpan.

Definition (Lean source)

abbrev finiteIndicatorSpan {R 𝒢 : Type*} [Fintype 𝒢] [DecidableEq 𝒢] (G : R → 𝒢) : Submodule ℝ (R → ℝ) := indicatorSpan G

Causalean.Panel.CellBridge.finiteIndicatorSpan · Causalean/Panel/CellBridge.lean:54

abbrev finiteTwoAxisIndicatorSpan reviewed

Causalean.Panel.CellBridge

Finite-weighted two-axis indicator span from Causalean.Panel.Weighted.IndicatorSpan.

Definition (Lean source)

abbrev finiteTwoAxisIndicatorSpan {R 𝒢 𝒯 : Type*} [Fintype 𝒢] [DecidableEq 𝒢] [Fintype 𝒯] [DecidableEq 𝒯] (G : R → 𝒢) (T : R → 𝒯) : Submodule ℝ (R → ℝ) := twoAxisIndicatorSpan G T

Causalean.Panel.CellBridge.finiteTwoAxisIndicatorSpan · Causalean/Panel/CellBridge.lean:60

def cellIndicator reviewed

Causalean.Panel.CellBridge

Real-valued singleton indicator for the cell {X = i}.

Definition (Lean source)

noncomputable def cellIndicator {Ω ι : Type*} [MeasurableSpace Ω] (X : Ω → ι) (i : ι) : Ω → ℝ := fun ω => indicator {ω' | X ω' = i} (fun _ => (1 : ℝ)) ω

Causalean.Panel.CellBridge.cellIndicator · Causalean/Panel/CellBridge.lean:70

def indicatorSpan reviewed

Causalean.Panel.CellBridge

One-axis finite indicator span generated by a measurable cell map G.

Definition (Lean source)

noncomputable def indicatorSpan {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [DecidableEq 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) [IsFiniteMeasure μ] (G : Ω → 𝒢) (G_meas : Measurable G) : LinearL2Class μ := by classical refine { mem := fun f => ∃ c : 𝒢 → ℝ, f =ᵐ[μ] (fun ω => ∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) , memLp := by intro f hf rcases hf with ⟨c, hfc⟩ have hsum : MemLp (fun ω => ∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) (2 : ENNReal) μ := by have hsum' : ∀ s : Finset 𝒢, MemLp (fun ω => s.sum (fun g => c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)) (2 : ENNReal) μ := by intro s refine Finset.induction_on s ?_ ?_ · simp · intro g s hg hs have hMeas : MeasurableSet {ω : Ω | G ω = g} := G_meas (measurableSet_singleton g) have hconst : MemLp (fun ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) (2 : ENNReal) μ := (MeasureTheory.memLp_const (μ := μ) (p := (2 : ENNReal)) (c := (1 : ℝ))).indicator hMeas have hterm : MemLp (fun ω => c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) (2 : ENNReal) μ := by simpa [mul_comm] using hconst.const_mul (c g) have hins : (fun ω => (insert g s).sum (fun g' => c g' * indicator {ω' | G ω' = g'} (fun _ => (1 : ℝ)) ω)) = (fun ω => c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (fun ω => s.sum (fun g' => c g' * indicator {ω' | G ω' = g'} (fun _ => (1 : ℝ)) ω)) := by funext ω simp [Finset.sum_insert hg, Pi.add_apply] rw [hins] exact hterm.add hs exact hsum' (Finset.univ : Finset 𝒢) exact (memLp_congr_ae hfc.symm).1 hsum , zero_mem := by refine ⟨fun _ => 0, ?_⟩ filter_upwards [] with ω simp , add_mem := by rintro f f' ⟨c, hfc⟩ ⟨c', hfc'⟩ refine ⟨fun g => c g + c' g, ?_⟩ filter_upwards [hfc, hfc'] with ω hf hf' change f ω + f' ω = ∑ g, (c g + c' g) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω rw [hf, hf'] calc (∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ g, c' g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) = ∑ g, (c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω + c' g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) := by simp [Finset.sum_add_distrib] _ = ∑ g, (c g + c' g) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω := by refine Finset.sum_congr rfl (fun g _ => ?_) ring , smul_mem := by intro a f ⟨c, hfc⟩ refine ⟨fun g => a * c g, ?_⟩ filter_upwards [hfc] with ω hf simp [hf, Finset.mul_sum, mul_assoc] }

Causalean.Panel.CellBridge.indicatorSpan · Causalean/Panel/CellBridge.lean:75 · uses LinearL2Class

def twoAxisIndicatorSpan reviewed

Causalean.Panel.CellBridge

Two-axis finite indicator span generated by measurable maps G and T.

Definition (Lean source)

noncomputable def twoAxisIndicatorSpan {Ω 𝒢 𝒯 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [DecidableEq 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] [Fintype 𝒯] [DecidableEq 𝒯] [MeasurableSpace 𝒯] [MeasurableSingletonClass 𝒯] (μ : Measure Ω) [IsFiniteMeasure μ] (G : Ω → 𝒢) (T : Ω → 𝒯) (G_meas : Measurable G) (T_meas : Measurable T) : LinearL2Class μ := by classical refine { mem := fun f => ∃ (cG : 𝒢 → ℝ) (cT : 𝒯 → ℝ), f =ᵐ[μ] (fun ω => (∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) , memLp := by intro f hf rcases hf with ⟨cG, cT, hfc⟩ have hsumG : MemLp (fun ω => ∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) (2 : ENNReal) μ := by exact (indicatorSpan μ G G_meas).memLp ⟨cG, Filter.EventuallyEq.rfl⟩ have hsumT : MemLp (fun ω => ∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) (2 : ENNReal) μ := by exact (indicatorSpan μ T T_meas).memLp ⟨cT, Filter.EventuallyEq.rfl⟩ have hsum : MemLp (fun ω => (∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) (2 : ENNReal) μ := hsumG.add hsumT exact (memLp_congr_ae hfc.symm).1 hsum , zero_mem := by refine ⟨fun _ => 0, fun _ => 0, ?_⟩ filter_upwards [] with ω simp , add_mem := by rintro f f' ⟨cG, cT, hfc⟩ ⟨cG', cT', hfc'⟩ refine ⟨fun g => cG g + cG' g, fun t => cT t + cT' t, ?_⟩ filter_upwards [hfc, hfc'] with ω hf hf' change f ω + f' ω = (∑ g, (cG g + cG' g) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, (cT t + cT' t) * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) rw [hf, hf'] calc ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) + ((∑ g, cG' g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT' t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) = ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ g, cG' g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)) + ((∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) + (∑ t, cT' t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) := by ring _ = (∑ g, (cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω + cG' g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)) + (∑ t, (cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω + cT' t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) := by simp [Finset.sum_add_distrib] _ = (∑ g, (cG g + cG' g) * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, (cT t + cT' t) * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) := by congr 1 · refine Finset.sum_congr rfl (fun g _ => ?_) ring · refine Finset.sum_congr rfl (fun t _ => ?_) ring , smul_mem := by intro a f ⟨cG, cT, hfc⟩ refine ⟨fun g => a * cG g, fun t => a * cT t, ?_⟩ filter_upwards [hfc] with ω hf simp [hf, Finset.mul_sum, mul_add, mul_assoc] }

Causalean.Panel.CellBridge.twoAxisIndicatorSpan · Causalean/Panel/CellBridge.lean:157 · uses LinearL2Class

def cellMass reviewed

Causalean.Panel.CellBridge

Cell mass (μ {G = g}).toReal.

Definition (Lean source)

def cellMass {Ω 𝒢 : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (G : Ω → 𝒢) (g : 𝒢) : ℝ := (μ {ω | G ω = g}).toReal

Causalean.Panel.CellBridge.cellMass · Causalean/Panel/CellBridge.lean:253

def jointCellMass reviewed

Causalean.Panel.CellBridge

Joint cell mass (μ {G = g ∧ T = t}).toReal.

Definition (Lean source)

def jointCellMass {Ω 𝒢 𝒯 : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (G : Ω → 𝒢) (T : Ω → 𝒯) (g : 𝒢) (t : 𝒯) : ℝ := (μ {ω | G ω = g ∧ T ω = t}).toReal

Causalean.Panel.CellBridge.jointCellMass · Causalean/Panel/CellBridge.lean:258

def cellMean reviewed

Causalean.Panel.CellBridge

Cell mean of a real-valued function on a finite cell. Zero-mass cells use Lean's totalized division convention.

Definition (Lean source)

noncomputable def cellMean {Ω 𝒢 : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (g : 𝒢) : ℝ := (∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ) / cellMass μ G g

Causalean.Panel.CellBridge.cellMean · Causalean/Panel/CellBridge.lean:263

theorem integral_mul_twoAxisIndicatorSpan_eq_zero_of_axes reviewed

Causalean.Panel.CellBridge

If a square-integrable residual V is orthogonal in expectation to the indicator of every level g of one axis G and orthogonal in expectation to the indicator of every level t of the other axis T, then it is orthogonal in expectation to every finite linear combination of those axis indicators, with coefficients cG and cT.

Formal statement

hypotheses

Ω 𝒢 𝒯 :

Type*

MeasurableSpace Ω

Fintype 𝒢

MeasurableSpace 𝒢

MeasurableSingletonClass 𝒢

Fintype 𝒯

MeasurableSpace 𝒯

MeasurableSingletonClass 𝒯

μ :

Measure Ω

IsFiniteMeasure μ

V :

Ω → ℝ

G :

Ω → 𝒢

T :

Ω → 𝒯

G_meas :

Measurable G

T_meas :

Measurable T

V_memLp :

MemLp V 2 μ

cG :

𝒢 → ℝ

cT :

𝒯 → ℝ

hG :

∀ g, ∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0

hT :

∀ t, ∫ ω, V ω * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0

conclusion

∫ ω, V ω * ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) ∂μ

= 0

Proof (Lean source)

theorem integral_mul_twoAxisIndicatorSpan_eq_zero_of_axes {Ω 𝒢 𝒯 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] [Fintype 𝒯] [MeasurableSpace 𝒯] [MeasurableSingletonClass 𝒯] (μ : Measure Ω) [IsFiniteMeasure μ] (V : Ω → ℝ) (G : Ω → 𝒢) (T : Ω → 𝒯) (G_meas : Measurable G) (T_meas : Measurable T) (V_memLp : MemLp V 2 μ) (cG : 𝒢 → ℝ) (cT : 𝒯 → ℝ) (hG : ∀ g, ∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0) (hT : ∀ t, ∫ ω, V ω * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω ∂μ = 0) : ∫ ω, V ω * ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) ∂μ = 0 := by classical have hGzero : ∫ ω, V ω * (∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ = 0 := integral_mul_indicatorSpan_eq_zero_of_cell μ V G G_meas V_memLp cG hG have hTzero : ∫ ω, V ω * (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) ∂μ = 0 := integral_mul_indicatorSpan_eq_zero_of_cell μ V T T_meas V_memLp cT hT have hGint : Integrable (fun ω => V ω * (∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)) μ := by let H := indicatorSpan μ G G_meas have hmem : H.mem (fun ω => ∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) := ⟨cG, Filter.EventuallyEq.rfl⟩ exact V_memLp.integrable_mul (H.memLp hmem) have hTint : Integrable (fun ω => V ω * (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) μ := by let H := indicatorSpan μ T T_meas have hmem : H.mem (fun ω => ∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) := ⟨cT, Filter.EventuallyEq.rfl⟩ exact V_memLp.integrable_mul (H.memLp hmem) calc ∫ ω, V ω * ((∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω)) ∂μ = ∫ ω, V ω * (∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) + V ω * (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω ring _ = ∫ ω, V ω * (∑ g, cG g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ + ∫ ω, V ω * (∑ t, cT t * indicator {ω' | T ω' = t} (fun _ => (1 : ℝ)) ω) ∂μ := by exact integral_add hGint hTint _ = 0 := by simp [hGzero, hTzero]

Causalean.Panel.CellBridge.integral_mul_twoAxisIndicatorSpan_eq_zero_of_axes · Causalean/Panel/CellBridge.lean:403

6 supporting declarations (lemmas, instances)

indicator_cell_memLp theorem — Cell indicators are in L² under a finite measure.

hypotheses

Ω 𝒢 :

Type*
MeasurableSpace Ω
MeasurableSpace 𝒢
MeasurableSingletonClass 𝒢

μ :

Measure Ω
IsFiniteMeasure μ

G :

Ω → 𝒢

G_meas :

Measurable G

g :

𝒢

conclusion

MemLp (fun ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) 2 μ

Proof (Lean source)

theorem indicator_cell_memLp {Ω 𝒢 : Type*} [MeasurableSpace Ω] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) [IsFiniteMeasure μ] (G : Ω → 𝒢) (G_meas : Measurable G) (g : 𝒢) : MemLp (fun ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) 2 μ := by let s : Set Ω := G ⁻¹' ({g} : Set 𝒢) have hMeas : MeasurableSet s := G_meas (measurableSet_singleton g) change MemLp (fun ω => indicator s (fun _ => (1 : ℝ)) ω) 2 μ exact (memLp_const (μ := μ) (1 : ℝ)).indicator hMeas

Causalean.Panel.CellBridge.indicator_cell_memLp · Causalean/Panel/CellBridge.lean:271
integral_cell_indicator_one_eq_cellMass theorem — Cell indicators integrate to their real cell mass.

hypotheses

Ω 𝒢 :

Type*
MeasurableSpace Ω
MeasurableSpace 𝒢
MeasurableSingletonClass 𝒢

μ :

Measure Ω

G :

Ω → 𝒢

G_meas :

Measurable G

g :

𝒢

conclusion

∫ ω, indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = cellMass μ G g

Proof (Lean source)

theorem integral_cell_indicator_one_eq_cellMass {Ω 𝒢 : Type*} [MeasurableSpace Ω] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) (G : Ω → 𝒢) (G_meas : Measurable G) (g : 𝒢) : ∫ ω, indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = cellMass μ G g := by let s : Set Ω := {ω | G ω = g} have hs_meas : MeasurableSet s := G_meas (measurableSet_singleton g) change (∫ ω, indicator s (1 : Ω → ℝ) ω ∂μ) = cellMass μ G g rw [MeasureTheory.integral_indicator_one hs_meas] simp [Measure.real, cellMass, s]

Causalean.Panel.CellBridge.integral_cell_indicator_one_eq_cellMass · Causalean/Panel/CellBridge.lean:282
cell_integral_div_mul_cellMass theorem — Dividing an indicator-weighted cell integral by a nonzero cell mass and multiplying back recovers the numerator; on zero-mass cells the numerator is zero because the indicator is a.e. zero.

hypotheses

Ω 𝒢 :

Type*
MeasurableSpace Ω

μ :

Measure Ω

F :

Ω → ℝ

G :

Ω → 𝒢

g :

𝒢

hμ :

μ {ω | G ω = g} ≠ ⊤

conclusion

((∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ) / cellMass μ G g) * cellMass μ G g
= ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ

Proof (Lean source)

theorem cell_integral_div_mul_cellMass {Ω 𝒢 : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (g : 𝒢) (hμ : μ {ω | G ω = g} ≠ ⊤) : ((∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ) / cellMass μ G g) * cellMass μ G g = ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by let s : Set Ω := {ω | G ω = g} let A : ℝ := ∫ ω, F ω * indicator s (fun _ => (1 : ℝ)) ω ∂μ have hs_top : μ s ≠ ⊤ := by simpa [s] using hμ by_cases hmass : cellMass μ G g = 0 · have hs_zero : μ s = 0 := by have hzero : (μ s).toReal = 0 := by simpa [cellMass, s] using hmass rcases (ENNReal.toReal_eq_zero_iff (μ s)).1 hzero with h0 | htop · exact h0 · exact elim (hs_top htop) have h_not_mem : ∀ᵐ ω ∂μ, ω ∉ s := by rw [MeasureTheory.ae_iff] simpa using hs_zero have h_ae : (fun ω => F ω * indicator s (fun _ => (1 : ℝ)) ω) =ᵐ[μ] 0 := by filter_upwards [h_not_mem] with ω hω simp [indicator, hω] have hA : A = 0 := by simpa [A] using (integral_eq_zero_of_ae h_ae) simp [cellMass, s, A, hA] · have hAdef : A = ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by simp [A, s] rw [hAdef.symm] field_simp [hmass]

Causalean.Panel.CellBridge.cell_integral_div_mul_cellMass · Causalean/Panel/CellBridge.lean:294
cellMean_mul_cellMass theorem — Cell mean multiplied by cell mass recovers the indicator-weighted raw integral.

hypotheses

Ω 𝒢 :

Type*
MeasurableSpace Ω

μ :

Measure Ω

F :

Ω → ℝ

G :

Ω → 𝒢

g :

𝒢

hμ :

μ {ω | G ω = g} ≠ ⊤

conclusion

cellMean μ F G g * cellMass μ G g
= ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ

Proof (Lean source)

theorem cellMean_mul_cellMass {Ω 𝒢 : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (g : 𝒢) (hμ : μ {ω | G ω = g} ≠ ⊤) : cellMean μ F G g * cellMass μ G g = ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by simpa [cellMean] using cell_integral_div_mul_cellMass μ F G g hμ

Causalean.Panel.CellBridge.cellMean_mul_cellMass · Causalean/Panel/CellBridge.lean:331
integral_mul_indicatorSpan_eq_zero_of_cell theorem — If a square-integrable residual is orthogonal to every cell indicator, it is orthogonal to every finite indicator-span member.

hypotheses

Ω 𝒢 :

Type*
MeasurableSpace Ω
Fintype 𝒢
MeasurableSpace 𝒢
MeasurableSingletonClass 𝒢

μ :

Measure Ω
IsFiniteMeasure μ

V :

Ω → ℝ

G :

Ω → 𝒢

G_meas :

Measurable G

V_memLp :

MemLp V 2 μ

c :

𝒢 → ℝ

hcell :

∀ g, ∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0

conclusion

∫ ω, V ω * (∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ = 0

Proof (Lean source)

theorem integral_mul_indicatorSpan_eq_zero_of_cell {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) [IsFiniteMeasure μ] (V : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (V_memLp : MemLp V 2 μ) (c : 𝒢 → ℝ) (hcell : ∀ g, ∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ = 0) : ∫ ω, V ω * (∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ = 0 := by classical let term : 𝒢 → Ω → ℝ := fun g ω => V ω * (c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) have hterm_int : ∀ g ∈ (Finset.univ : Finset 𝒢), Integrable (term g) μ := by intro g _ have hI : MemLp (fun ω => indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) 2 μ := indicator_cell_memLp μ G G_meas g have hcI : MemLp (fun ω => c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) 2 μ := by simpa [mul_comm] using hI.const_mul (c g) exact V_memLp.integrable_mul hcI have hpoint : (fun ω => V ω * (∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω)) = (fun ω => ∑ g, term g ω) := by funext ω simp [term, Finset.mul_sum] calc ∫ ω, V ω * (∑ g, c g * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ = ∫ ω, ∑ g, term g ω ∂μ := by rw [hpoint] _ = ∑ g, ∫ ω, term g ω ∂μ := by simpa using (MeasureTheory.integral_finset_sum (Finset.univ : Finset 𝒢) (f := term) hterm_int) _ = 0 := by refine Finset.sum_eq_zero (fun g _ => ?_) calc ∫ ω, term g ω ∂μ = ∫ ω, c g * (V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω simp [term] ring _ = c g * ∫ ω, V ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := integral_const_mul (c g) _ _ = 0 := by simp [hcell g]

Causalean.Panel.CellBridge.integral_mul_indicatorSpan_eq_zero_of_cell · Causalean/Panel/CellBridge.lean:342
integral_eq_sum_cell theorem — Integrate an integrable function by summing over a finite measurable partition generated by G.

hypotheses

Ω 𝒢 :

Type*
MeasurableSpace Ω
Fintype 𝒢
MeasurableSpace 𝒢
MeasurableSingletonClass 𝒢

μ :

Measure Ω

F :

Ω → ℝ

G :

Ω → 𝒢

G_meas :

Measurable G

F_int :

Integrable F μ

conclusion

∫ ω, F ω ∂μ = ∑ g, ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ

Proof (Lean source)

theorem integral_eq_sum_cell {Ω 𝒢 : Type*} [MeasurableSpace Ω] [Fintype 𝒢] [MeasurableSpace 𝒢] [MeasurableSingletonClass 𝒢] (μ : Measure Ω) (F : Ω → ℝ) (G : Ω → 𝒢) (G_meas : Measurable G) (F_int : Integrable F μ) : ∫ ω, F ω ∂μ = ∑ g, ∫ ω, F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω ∂μ := by classical let term : 𝒢 → Ω → ℝ := fun g ω => F ω * indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω have hterm_int : ∀ g ∈ (Finset.univ : Finset 𝒢), Integrable (term g) μ := by intro g _ have hG : MeasurableSet {ω : Ω | G ω = g} := G_meas (measurableSet_singleton g) have hEq : term g = fun ω => indicator {ω' | G ω' = g} F ω := by funext ω by_cases hω : G ω = g · simp [term, indicator, hω] · simp [term, indicator, hω] rw [hEq] exact F_int.indicator hG have hsum_ind : ∀ ω, (∑ g, indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) = 1 := by intro ω rw [Finset.sum_eq_single (G ω)] · simp · intro b _ hb have hne : ¬ G ω = b := fun h => hb h.symm simp [indicator, hne] · intro hnot exact elim (hnot (Finset.mem_univ _)) calc ∫ ω, F ω ∂μ = ∫ ω, F ω * (∑ g, indicator {ω' | G ω' = g} (fun _ => (1 : ℝ)) ω) ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω simp [hsum_ind ω] _ = ∫ ω, ∑ g, term g ω ∂μ := by refine integral_congr_ae ?_ filter_upwards [] with ω simp [term, Finset.mul_sum] _ = ∑ g, ∫ ω, term g ω ∂μ := by simpa using (MeasureTheory.integral_finset_sum (Finset.univ : Finset 𝒢) (f := term) hterm_int)

Causalean.Panel.CellBridge.integral_eq_sum_cell · Causalean/Panel/CellBridge.lean:479

UniformTwoWayPanel 12 core · 10 supporting This file provides finite-sum algebra for balanced unit-period panels under the uniform unit-period measure. ★ finite_residualized_coefficient_eq_of_normalEqs★ ddot_orthogonal_unit_time

Uniform Balanced Two-Way Panels

This file provides finite-sum algebra for balanced unit-period panels under the uniform unit-period measure. It defines BalancedPanel, uniform unit weights, unit means, time means, grand means, double demeaning ddot, the unnormalized inner product, the finite residualized coefficient, and the unit/time additive nuisance class. Its main results relate the uniform constructions to WeightedTwoWayPanel, prove the finite residualized-coefficient handoff, and show that double-demeaned arrays are orthogonal to unit-only, time-only, and unit/time additive functions.

structure BalancedPanel reviewed

Causalean.Panel.UniformTwoWayPanel

Balanced panel. The side conditions from the source definition that a panel counts as balanced: the unit index type has at least two elements and the time index type has at least two elements.

Definition (Lean source)

parameters

Unit Time :

Type*

Fintype Unit

Fintype Time

fields

unit_card_ge_two :

2 ≤ card Unit

time_card_ge_two :

2 ≤ card Time

Causalean.Panel.UniformTwoWayPanel.BalancedPanel · Causalean/Panel/UniformTwoWayPanel.lean:47

def uniformWeights reviewed

Causalean.Panel.UniformTwoWayPanel

Uniform unit weights as a probability vector, used to view this module as the uniform specialization of WeightedTwoWayPanel.

Definition (Lean source)

noncomputable def uniformWeights (hU : 0 < Fintype.card Unit) : WeightedTwoWayPanel.UnitWeights Unit := ⟨fun _ => (Fintype.card Unit : ℝ)⁻¹, (by intro _i have hU_real : (0 : ℝ) < Fintype.card Unit := by exact_mod_cast hU exact inv_pos.mpr hU_real), (by have hU_ne : (Fintype.card Unit : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hU) calc ∑ _i : Unit, (Fintype.card Unit : ℝ)⁻¹ = (Fintype.card Unit : ℝ) * (Fintype.card Unit : ℝ)⁻¹ := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] _ = 1 := mul_inv_cancel₀ hU_ne)⟩

Causalean.Panel.UniformTwoWayPanel.uniformWeights · Causalean/Panel/UniformTwoWayPanel.lean:57 · uses UnitWeights

def unitMean reviewed

Causalean.Panel.UniformTwoWayPanel

Unit mean \bar V_{i·} under the uniform period measure.

Definition (Lean source)

noncomputable def unitMean (V : Unit → Time → ℝ) (i : Unit) : ℝ := (Fintype.card Time : ℝ)⁻¹ * ∑ t, V i t

Causalean.Panel.UniformTwoWayPanel.unitMean · Causalean/Panel/UniformTwoWayPanel.lean:75

def timeMean reviewed

Causalean.Panel.UniformTwoWayPanel

Time mean \bar V_{·t} under the uniform unit measure.

Definition (Lean source)

noncomputable def timeMean (V : Unit → Time → ℝ) (t : Time) : ℝ := (Fintype.card Unit : ℝ)⁻¹ * ∑ i, V i t

Causalean.Panel.UniformTwoWayPanel.timeMean · Causalean/Panel/UniformTwoWayPanel.lean:79

def grandMean reviewed

Causalean.Panel.UniformTwoWayPanel

Grand mean \bar V under the uniform unit-period measure.

Definition (Lean source)

noncomputable def grandMean (V : Unit → Time → ℝ) : ℝ := ((Fintype.card Unit : ℝ) * (Fintype.card Time : ℝ))⁻¹ * ∑ i, ∑ t, V i t

Causalean.Panel.UniformTwoWayPanel.grandMean · Causalean/Panel/UniformTwoWayPanel.lean:83

def ddot reviewed

Causalean.Panel.UniformTwoWayPanel

Two-way residual / double-demeaned array.

Definition (Lean source)

noncomputable def ddot (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ℝ := V i t - unitMean V i - timeMean V t + grandMean V

Causalean.Panel.UniformTwoWayPanel.ddot · Causalean/Panel/UniformTwoWayPanel.lean:88

def inner reviewed

Causalean.Panel.UniformTwoWayPanel

Uniform finite-panel inner product, without the harmless normalizing constant.

Definition (Lean source)

noncomputable def inner (V W : Unit → Time → ℝ) : ℝ := ∑ i, ∑ t, V i t * W i t

Causalean.Panel.UniformTwoWayPanel.inner · Causalean/Panel/UniformTwoWayPanel.lean:92

def finiteResidualizedCoefficient reviewed

Causalean.Panel.UniformTwoWayPanel

Finite scalar residualized coefficient for a supplied residualized regressor Dtilde and residualized outcome Ytilde.

Definition (Lean source)

noncomputable def finiteResidualizedCoefficient (Dtilde Ytilde : Unit → Time → ℝ) : ℝ := inner Dtilde Ytilde / inner Dtilde Dtilde

Causalean.Panel.UniformTwoWayPanel.finiteResidualizedCoefficient · Causalean/Panel/UniformTwoWayPanel.lean:181

theorem finite_residualized_coefficient_eq_of_normalEqs reviewed

Causalean.Panel.UniformTwoWayPanel

Finite scalar Frisch–Waugh–Lovell handoff. Suppose the outcome and regressor decompose as Y = Yproj + Ytilde and D = Dproj + Dtilde, where Dproj and the fitted nuisance term Hβ both satisfy the nuisance predicate H, Dtilde is orthogonal to every array satisfying H, Dtilde is orthogonal to Yproj, and Dtilde has strictly positive self-inner-product (a nondegenerate residualized regressor). If the coefficient β and nuisance fit Hβ satisfy the normal equation against the raw regressor D and the normal equation against its nuisance component Dproj, then β equals the finite residualized coefficient inner Dtilde Ytilde / inner Dtilde Dtilde.

Formal statement

hypotheses

H :

(Unit → Time → ℝ) → Prop

Y D Yproj Ytilde Dproj Dtilde Hβ :

Unit → Time → ℝ

β :

ℝ

hY_decomp :

∀ i t, Y i t = Yproj i t + Ytilde i t

hD_decomp :

∀ i t, D i t = Dproj i t + Dtilde i t

hDproj_mem :

H Dproj

hHβ_mem :

H Hβ

hDtilde_orth_H :

∀ h : Unit → Time → ℝ

if

H h

then

inner Dtilde h = 0

hYproj_orth :

inner Dtilde Yproj = 0

hDtilde_pos :

0 < inner Dtilde Dtilde

h_normal_D :

inner D (fun i t => Y i t - D i t * β - Hβ i t) = 0

h_normal_Dproj :

inner Dproj (fun i t => Y i t - D i t * β - Hβ i t) = 0

conclusion

β = finiteResidualizedCoefficient Dtilde Ytilde

Proof (Lean source)

theorem finite_residualized_coefficient_eq_of_normalEqs (H : (Unit → Time → ℝ) → Prop) {Y D Yproj Ytilde Dproj Dtilde Hβ : Unit → Time → ℝ} {β : ℝ} (hY_decomp : ∀ i t, Y i t = Yproj i t + Ytilde i t) (hD_decomp : ∀ i t, D i t = Dproj i t + Dtilde i t) (hDproj_mem : H Dproj) (hHβ_mem : H Hβ) (hDtilde_orth_H : ∀ h : Unit → Time → ℝ, H h → inner Dtilde h = 0) (hYproj_orth : inner Dtilde Yproj = 0) (hDtilde_pos : 0 < inner Dtilde Dtilde) (h_normal_D : inner D (fun i t => Y i t - D i t * β - Hβ i t) = 0) (h_normal_Dproj : inner Dproj (fun i t => Y i t - D i t * β - Hβ i t) = 0) : β = finiteResidualizedCoefficient Dtilde Ytilde := by let e : Unit → Time → ℝ := fun i t => Y i t - D i t * β - Hβ i t have hDproj_e : inner Dproj e = 0 := h_normal_Dproj have hD_split : inner D e = inner Dproj e + inner Dtilde e := by unfold inner dsimp [e] calc ∑ i, ∑ t, D i t * (Y i t - D i t * β - Hβ i t) = ∑ i, ∑ t, (Dproj i t * (Y i t - D i t * β - Hβ i t) + Dtilde i t * (Y i t - D i t * β - Hβ i t)) := by apply Finset.sum_congr rfl intro i _hi apply Finset.sum_congr rfl intro t _ht rw [hD_decomp i t] ring _ = (∑ i, ∑ t, Dproj i t * (Y i t - D i t * β - Hβ i t)) + ∑ i, ∑ t, Dtilde i t * (Y i t - D i t * β - Hβ i t) := by simp only [Finset.sum_add_distrib] have hDtilde_e : inner Dtilde e = 0 := by linarith [h_normal_D, hDproj_e, hD_split] have hDproj_orth : inner Dtilde Dproj = 0 := hDtilde_orth_H Dproj hDproj_mem have hHβ_orth : inner Dtilde Hβ = 0 := hDtilde_orth_H Hβ hHβ_mem have hYproj_orth' : (∑ i, ∑ t, Dtilde i t * Yproj i t) = 0 := by simpa [inner] using hYproj_orth have hDproj_orth' : (∑ i, ∑ t, Dtilde i t * Dproj i t) = 0 := by simpa [inner] using hDproj_orth have hHβ_orth' : (∑ i, ∑ t, Dtilde i t * Hβ i t) = 0 := by simpa [inner] using hHβ_orth have hExpand : inner Dtilde e = inner Dtilde Ytilde - β * inner Dtilde Dtilde := by unfold inner dsimp [e] calc ∑ i, ∑ t, Dtilde i t * (Y i t - D i t * β - Hβ i t) = ∑ i, ∑ t, (Dtilde i t * Yproj i t + Dtilde i t * Ytilde i t - (Dtilde i t * Dproj i t) * β - (Dtilde i t * Dtilde i t) * β - Dtilde i t * Hβ i t) := by apply Finset.sum_congr rfl intro i _hi apply Finset.sum_congr rfl intro t _ht rw [hY_decomp i t, hD_decomp i t] ring _ = (∑ i, ∑ t, Dtilde i t * Yproj i t) + (∑ i, ∑ t, Dtilde i t * Ytilde i t) - (∑ i, ∑ t, Dtilde i t * Dproj i t) * β - (∑ i, ∑ t, Dtilde i t * Dtilde i t) * β - (∑ i, ∑ t, Dtilde i t * Hβ i t) := by simp only [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_mul] _ = (∑ i, ∑ t, Dtilde i t * Ytilde i t) - β * (∑ i, ∑ t, Dtilde i t * Dtilde i t) := by rw [hYproj_orth', hDproj_orth', hHβ_orth'] ring have hcoeff : β * inner Dtilde Dtilde = inner Dtilde Ytilde := by linarith [hDtilde_e, hExpand] have hden_ne : inner Dtilde Dtilde ≠ 0 := hDtilde_pos.ne' have hβ_eq : β = inner Dtilde Ytilde / inner Dtilde Dtilde := (eq_div_iff hden_ne).2 hcoeff simpa [finiteResidualizedCoefficient] using hβ_eq

Causalean.Panel.UniformTwoWayPanel.finite_residualized_coefficient_eq_of_normalEqs · Causalean/Panel/UniformTwoWayPanel.lean:187 · uses finiteResidualizedCoefficient , inner

abbrev IsUnitTimeAdditive reviewed

Causalean.Panel.UniformTwoWayPanel

Unit-time additive nuisance class h_it = a_i + b_t.

Definition (Lean source)

abbrev IsUnitTimeAdditive (h : Unit → Time → ℝ) : Prop := IsUnitTimeAdditive h

Causalean.Panel.UniformTwoWayPanel.IsUnitTimeAdditive · Causalean/Panel/UniformTwoWayPanel.lean:283

def unitTimeProjection reviewed

Causalean.Panel.UniformTwoWayPanel

The unit/time component removed by double demeaning.

Definition (Lean source)

noncomputable def unitTimeProjection (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ℝ := unitMean V i + timeMean V t - grandMean V

Causalean.Panel.UniformTwoWayPanel.unitTimeProjection · Causalean/Panel/UniformTwoWayPanel.lean:289

theorem ddot_orthogonal_unit_time reviewed

Causalean.Panel.UniformTwoWayPanel

Assume at least one unit and at least one period. Then for any array h of unit/time additive form h_it = a_i + b_t, the double-demeaned array ddot V is orthogonal to h under the unnormalized uniform panel inner product.

Formal statement

hypotheses

hU :

0 < card Unit

hT :

0 < card Time

V h :

Unit → Time → ℝ

hh :

IsUnitTimeAdditive h

conclusion

inner (ddot V) h = 0

Proof (Lean source)

theorem ddot_orthogonal_unit_time (hU : 0 < Fintype.card Unit) (hT : 0 < Fintype.card Time) (V h : Unit → Time → ℝ) (hh : IsUnitTimeAdditive h) : inner (ddot V) h = 0 := by classical let w := uniformWeights (Unit := Unit) hU calc inner (ddot V) h = (Fintype.card Unit : ℝ) * WeightedTwoWayPanel.inner w (ddot V) h := by simpa [w] using inner_eq_card_smul_weighted (Unit := Unit) (Time := Time) hU (ddot V) h _ = (Fintype.card Unit : ℝ) * WeightedTwoWayPanel.inner w (WeightedTwoWayPanel.ddot w V) h := by apply congrArg (fun F => (Fintype.card Unit : ℝ) * WeightedTwoWayPanel.inner w F h) funext i t rw [ddot_eq_weighted V i t] _ = 0 := by rw [WeightedTwoWayPanel.ddot_orthogonal_unit_time w V h hh, mul_zero]

Causalean.Panel.UniformTwoWayPanel.ddot_orthogonal_unit_time · Causalean/Panel/UniformTwoWayPanel.lean:370 · uses IsUnitTimeAdditive , ddot , inner

10 supporting declarations (lemmas, instances)

timeMean_eq_weighted theorem — In a finite balanced panel with uniformly weighted units, the usual time mean in any period equals the time mean computed under the uniform unit weights.

hypotheses

hU :

0 < card Unit

V :

Unit → Time → ℝ

t :

Time

conclusion

timeMean V t = WeightedTwoWayPanel.timeMean (uniformWeights hU) V t

Proof (Lean source)

theorem timeMean_eq_weighted (hU : 0 < card Unit) (V : Unit → Time → ℝ) (t : Time) : timeMean V t = WeightedTwoWayPanel.timeMean (uniformWeights hU) V t := by unfold timeMean WeightedTwoWayPanel.timeMean uniformWeights rw [← Finset.mul_sum]

Causalean.Panel.UniformTwoWayPanel.timeMean_eq_weighted · Causalean/Panel/UniformTwoWayPanel.lean:98
grandMean_eq_weighted theorem — In a finite balanced panel with uniform unit weights, the usual grand mean equals the grand mean computed under those weights.

hypotheses

hU :

0 < card Unit

V :

Unit → Time → ℝ

conclusion

grandMean V = WeightedTwoWayPanel.grandMean (uniformWeights hU) V

Proof (Lean source)

theorem grandMean_eq_weighted (hU : 0 < Fintype.card Unit) (V : Unit → Time → ℝ) : grandMean V = WeightedTwoWayPanel.grandMean (uniformWeights hU) V := by unfold grandMean WeightedTwoWayPanel.grandMean uniformWeights change (((Fintype.card Unit : ℝ) * (Fintype.card Time : ℝ))⁻¹ * ∑ i, ∑ t, V i t) = ∑ i, (Fintype.card Unit : ℝ)⁻¹ * ((Fintype.card Time : ℝ)⁻¹ * ∑ t, V i t) calc (((Fintype.card Unit : ℝ) * (Fintype.card Time : ℝ))⁻¹ * ∑ i, ∑ t, V i t) = (Fintype.card Unit : ℝ)⁻¹ * ((Fintype.card Time : ℝ)⁻¹ * ∑ i, ∑ t, V i t) := by rw [mul_inv] ring _ = ∑ i, (Fintype.card Unit : ℝ)⁻¹ * ((Fintype.card Time : ℝ)⁻¹ * ∑ t, V i t) := by rw [Finset.mul_sum, Finset.mul_sum]

Causalean.Panel.UniformTwoWayPanel.grandMean_eq_weighted · Causalean/Panel/UniformTwoWayPanel.lean:106
ddot_eq_weighted theorem — Uniform double-demeaning is weighted double-demeaning with uniform unit weights.

hypotheses

V :

Unit → Time → ℝ

i :

Unit

t :

Time

conclusion

ddot V i t
= WeightedTwoWayPanel.ddot (uniformWeights (Fintype.card_pos_iff.mpr ⟨i⟩)) V i t

Proof (Lean source)

theorem ddot_eq_weighted (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ddot V i t = WeightedTwoWayPanel.ddot (uniformWeights (Fintype.card_pos_iff.mpr ⟨i⟩)) V i t := by have hU : 0 < card Unit := Fintype.card_pos_iff.mpr ⟨i⟩ unfold ddot WeightedTwoWayPanel.ddot rw [timeMean_eq_weighted hU V t, grandMean_eq_weighted hU V] rfl

Causalean.Panel.UniformTwoWayPanel.ddot_eq_weighted · Causalean/Panel/UniformTwoWayPanel.lean:128
sum_eq_card_mul_uniform_weighted theorem — In a finite balanced panel, the unweighted sum across all unit-period cells equals the number of units times the corresponding sum under uniform unit weights.

hypotheses

hU :

0 < Fintype.card Unit

F :

Unit → Time → ℝ

conclusion

∑ i, ∑ t, F i t = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, (uniformWeights hU).p i * F i t

Proof (Lean source)

theorem sum_eq_card_mul_uniform_weighted (hU : 0 < Fintype.card Unit) (F : Unit → Time → ℝ) : ∑ i, ∑ t, F i t = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, (uniformWeights hU).p i * F i t := by have hU_ne : (Fintype.card Unit : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hU) unfold uniformWeights calc ∑ i, ∑ t, F i t = ((Fintype.card Unit : ℝ) * (Fintype.card Unit : ℝ)⁻¹) * ∑ i, ∑ t, F i t := by rw [mul_inv_cancel₀ hU_ne, one_mul] _ = (Fintype.card Unit : ℝ) * ((Fintype.card Unit : ℝ)⁻¹ * ∑ i, ∑ t, F i t) := by ring _ = (Fintype.card Unit : ℝ) * ∑ i, (Fintype.card Unit : ℝ)⁻¹ * ∑ t, F i t := by rw [Finset.mul_sum] _ = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, (Fintype.card Unit : ℝ)⁻¹ * F i t := by congr 1 apply Finset.sum_congr rfl intro i _hi rw [Finset.mul_sum]

Causalean.Panel.UniformTwoWayPanel.sum_eq_card_mul_uniform_weighted · Causalean/Panel/UniformTwoWayPanel.lean:139
inner_eq_card_smul_weighted theorem — The unnormalized uniform inner product is the unit count times the weighted inner product under uniform unit weights.

hypotheses

hU :

0 < Fintype.card Unit

V W :

Unit → Time → ℝ

conclusion

inner V W = (Fintype.card Unit : ℝ) * WeightedTwoWayPanel.inner (uniformWeights hU) V W

Proof (Lean source)

theorem inner_eq_card_smul_weighted (hU : 0 < Fintype.card Unit) (V W : Unit → Time → ℝ) : inner V W = (Fintype.card Unit : ℝ) * WeightedTwoWayPanel.inner (uniformWeights hU) V W := by simpa [inner, WeightedTwoWayPanel.inner] using sum_eq_card_mul_uniform_weighted (Unit := Unit) (Time := Time) hU (fun i t => V i t * W i t)

Causalean.Panel.UniformTwoWayPanel.inner_eq_card_smul_weighted · Causalean/Panel/UniformTwoWayPanel.lean:170
ddot_reconstruct theorem — Reconstruction identity V_it = ddot V_it + unitMean V_i + timeMean V_t - grandMean V.

hypotheses

V :

Unit → Time → ℝ

i :

Unit

t :

Time

conclusion

ddot V i t + unitMean V i + timeMean V t - grandMean V = V i t

Proof (Lean source)

theorem ddot_reconstruct (V : Unit → Time → ℝ) (i : Unit) (t : Time) : ddot V i t + unitMean V i + timeMean V t - grandMean V = V i t := by unfold ddot ring

Causalean.Panel.UniformTwoWayPanel.ddot_reconstruct · Causalean/Panel/UniformTwoWayPanel.lean:293
unitTimeProjection_additive theorem — The removed component is itself unit/time additive.

hypotheses

V :

Unit → Time → ℝ

conclusion

IsUnitTimeAdditive (unitTimeProjection V)

Proof (Lean source)

theorem unitTimeProjection_additive (V : Unit → Time → ℝ) : IsUnitTimeAdditive (unitTimeProjection V) := by refine ⟨unitMean V, fun t => timeMean V t - grandMean V, ?_⟩ intro i t unfold unitTimeProjection ring

Causalean.Panel.UniformTwoWayPanel.unitTimeProjection_additive · Causalean/Panel/UniformTwoWayPanel.lean:300
sub_ddot_eq_unitTimeProjection theorem — Pointwise residual decomposition V - ddot V into the unit/time projection.

hypotheses

V :

Unit → Time → ℝ

i :

Unit

t :

Time

conclusion

V i t - ddot V i t = unitTimeProjection V i t

Proof (Lean source)

theorem sub_ddot_eq_unitTimeProjection (V : Unit → Time → ℝ) (i : Unit) (t : Time) : V i t - ddot V i t = unitTimeProjection V i t := by unfold ddot unitTimeProjection ring

Causalean.Panel.UniformTwoWayPanel.sub_ddot_eq_unitTimeProjection · Causalean/Panel/UniformTwoWayPanel.lean:308
ddot_orthogonal_unit theorem — Double-demeaned arrays are orthogonal to arbitrary unit-only functions.

hypotheses

hU :

0 < card Unit

hT :

0 < card Time

V :

Unit → Time → ℝ

a :

Unit → ℝ

conclusion

∑ i, ∑ t, ddot V i t * a i = 0

Proof (Lean source)

theorem ddot_orthogonal_unit (hU : 0 < Fintype.card Unit) (hT : 0 < Fintype.card Time) (V : Unit → Time → ℝ) (a : Unit → ℝ) : ∑ i, ∑ t, ddot V i t * a i = 0 := by classical let w := uniformWeights (Unit := Unit) hU have hweighted : ∑ i, ∑ t, w.p i * (WeightedTwoWayPanel.ddot w V i t * a i) = 0 := WeightedTwoWayPanel.ddot_orthogonal_unit w V a calc ∑ i, ∑ t, ddot V i t * a i = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, w.p i * (ddot V i t * a i) := by simpa [w] using sum_eq_card_mul_uniform_weighted (Unit := Unit) (Time := Time) hU (fun i t => ddot V i t * a i) _ = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, w.p i * (WeightedTwoWayPanel.ddot w V i t * a i) := by congr 1 apply Finset.sum_congr rfl intro i _hi apply Finset.sum_congr rfl intro t _ht rw [ddot_eq_weighted V i t] _ = 0 := by rw [hweighted, mul_zero]

Causalean.Panel.UniformTwoWayPanel.ddot_orthogonal_unit · Causalean/Panel/UniformTwoWayPanel.lean:315
ddot_orthogonal_time theorem — Double-demeaned arrays are orthogonal to arbitrary time-only functions.

hypotheses

hU :

0 < card Unit

V :

Unit → Time → ℝ

b :

Time → ℝ

conclusion

∑ i, ∑ t, ddot V i t * b t = 0

Proof (Lean source)

theorem ddot_orthogonal_time (hU : 0 < Fintype.card Unit) (V : Unit → Time → ℝ) (b : Time → ℝ) : ∑ i, ∑ t, ddot V i t * b t = 0 := by classical let w := uniformWeights (Unit := Unit) hU have hweighted : ∑ i, ∑ t, w.p i * (WeightedTwoWayPanel.ddot w V i t * b t) = 0 := WeightedTwoWayPanel.ddot_orthogonal_time w V b calc ∑ i, ∑ t, ddot V i t * b t = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, w.p i * (ddot V i t * b t) := by simpa [w] using sum_eq_card_mul_uniform_weighted (Unit := Unit) (Time := Time) hU (fun i t => ddot V i t * b t) _ = (Fintype.card Unit : ℝ) * ∑ i, ∑ t, w.p i * (WeightedTwoWayPanel.ddot w V i t * b t) := by congr 1 apply Finset.sum_congr rfl intro i _hi apply Finset.sum_congr rfl intro t _ht rw [ddot_eq_weighted V i t] _ = 0 := by rw [hweighted, mul_zero]

Causalean.Panel.UniformTwoWayPanel.ddot_orthogonal_time · Causalean/Panel/UniformTwoWayPanel.lean:343

FWLInstanceL2 1 core · 4 supporting This file instantiates the abstract Frisch-Waugh-Lovell development on square-integrable real functions under a probability measure. ★ fwlCoef_eq_of_original_minimizer

L2 Frisch-Waugh-Lovell Instance

This file instantiates the abstract Frisch-Waugh-Lovell development on square-integrable real functions under a probability measure. It supplies orthogonal projections for finite-dimensional nuisance subspaces, identifies the Lp inner product with the corresponding population integral, and exposes the residualized normal equations, least-squares optimality, and uniqueness statements for the L²(μ) specialization.

theorem fwlCoef_eq_of_original_minimizer reviewed

Causalean.Panel.FWLInstanceL2

FWL uniqueness on L²(μ). Fix square-integrable regressors X and outcome Y, and a finite-dimensional nuisance subspace H of L²(μ), and assume the residualized regressor Gram matrix is invertible. If the nuisance term h lies in H and the pair (β, h) minimizes the original least-squares objective jointly over all coefficient vectors and nuisance terms in H, then β equals the Frisch–Waugh–Lovell coefficient computed by residualizing against H. Specialization of Causalean.Mathlib.FWL.fwlCoef_eq_of_original_minimizer.

Formal statement

hypotheses

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

Lp ℝ 2 μ

hh :

h ∈ H

hmin :

∀ (γ : Fin K → ℝ) {g : Lp ℝ 2 μ}

if

g ∈ H

then

originalObjective X Y β h

≤ originalObjective X Y γ g

conclusion

β = fwlCoef H X Y

Proof (Lean source)

theorem fwlCoef_eq_of_original_minimizer (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : Lp ℝ 2 μ} (hh : h ∈ H) (hmin : ∀ (γ : Fin K → ℝ) {g : Lp ℝ 2 μ}, g ∈ H → originalObjective X Y β h ≤ originalObjective X Y γ g) : β = fwlCoef H X Y := fwlCoef_eq_of_original_minimizer H X Y hQ β hh hmin

Causalean.Panel.FWLInstanceL2.fwlCoef_eq_of_original_minimizer · Causalean/Panel/FWLInstanceL2.lean:107 · uses fwlCoef , gramResid , originalObjective

4 supporting declarations (lemmas, instances)

hasOrthogonalProjection_of_finiteDimensional instance — A finite-dimensional subspace of Lp ℝ 2 μ admits an orthogonal projection: it is complete (finite-dimensional over the complete field ℝ), so Mathlib's completeness instance applies.

instance hasOrthogonalProjection_of_finiteDimensional (H : Submodule ℝ (Lp ℝ 2 μ)) [FiniteDimensional ℝ H] : H.HasOrthogonalProjection := inferInstance

Causalean.Panel.FWLInstanceL2.hasOrthogonalProjection_of_finiteDimensional · Causalean/Panel/FWLInstanceL2.lean:59
inner_eq_integral theorem — L² inner product = integral pairing. For two square-integrable real random variables, the Hilbert-space inner product equals the integral of their product, independent of the chosen representatives. This is the bridge between abstract FWL inner products and the population second moments used in estimand papers.

hypotheses

f g :

Lp ℝ 2 μ

conclusion

inner ℝ f g = ∫ a, f a * g a ∂μ

Proof (Lean source)

theorem inner_eq_integral (f g : Lp ℝ 2 μ) : inner ℝ f g = ∫ a, f a * g a ∂μ := by rw [L2.inner_def] refine integral_congr_ae (Filter.Eventually.of_forall (fun a => ?_)) change inner ℝ (f a) (g a) = f a * g a exact mul_comm _ _

Causalean.Panel.FWLInstanceL2.inner_eq_integral · Causalean/Panel/FWLInstanceL2.lean:67
gramResid_mulVec_fwlCoef theorem — Residualized normal equations on L²(μ). The FWL coefficient solves gramResid H X *ᵥ fwlCoef H X Y = residInnerVec H X Y whenever the residualized Gram matrix is invertible. Specialization of Causalean.Mathlib.FWL.gramResid_mulVec_fwlCoef.

hypotheses

hQ :

IsUnit (gramResid H X).det

conclusion

(gramResid H X).mulVec (fwlCoef H X Y)
= residInnerVec H X Y

Proof (Lean source)

theorem gramResid_mulVec_fwlCoef (hQ : IsUnit (gramResid H X).det) : (gramResid H X).mulVec (fwlCoef H X Y) = residInnerVec H X Y := gramResid_mulVec_fwlCoef H X Y hQ

Causalean.Panel.FWLInstanceL2.gramResid_mulVec_fwlCoef · Causalean/Panel/FWLInstanceL2.lean:84
fwlCoef_original_minimizes theorem — FWL least-squares optimality on L²(μ). The FWL coefficient (paired with the nuisance projection of its raw residual) minimizes the original least-squares objective over coefficients and nuisance terms in H. Specialization of Causalean.Mathlib.FWL.fwlCoef_original_minimizes.

hypotheses

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

Lp ℝ 2 μ

hh :

h ∈ H

conclusion

originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)))
≤ originalObjective X Y β h

Proof (Lean source)

theorem fwlCoef_original_minimizes (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : Lp ℝ 2 μ} (hh : h ∈ H) : originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))) ≤ originalObjective X Y β h := fwlCoef_original_minimizes H X Y hQ β hh

Causalean.Panel.FWLInstanceL2.fwlCoef_original_minimizes · Causalean/Panel/FWLInstanceL2.lean:94

InnerProduct 1 core · 15 supporting This file provides the panel-facing import point for weighted inner products on observed cell arrays. ★ ip_self_eq_zero_iff

Panel Inner Products

This file provides the panel-facing import point for weighted inner products on observed cell arrays. It restates the generic weighted-support inner-product operations and algebraic lemmas under the panel cell namespace, including the scalar aliases Cells.ip, Cells.ip_eq_weighted, the matrix-valued aliases Cells.ipMat, Cells.ipMat_eq_weighted, and the symmetry, additivity, homogeneity, nonnegativity, vanishing, and transpose lemmas used by panel projection proofs.

lemma ip_self_eq_zero_iff reviewed

Causalean.Panel.Cells

For a panel cell structure and a panel array A, the self inner product c.ip A A is zero exactly when A vanishes on every observed cell of c.

Formal statement

hypotheses

c :

Cells I T

A :

(I × T) → ℝ

conclusion

c.ip A A = 0 ↔ ∀ r ∈ c.observed, A r = 0

Proof (Lean source)

lemma ip_self_eq_zero_iff (c : Cells I T) (A : (I × T) → ℝ) : c.ip A A = 0 ↔ ∀ r ∈ c.observed, A r = 0 := ip_self_eq_zero_iff c A

Causalean.Panel.Cells.ip_self_eq_zero_iff · Causalean/Panel/InnerProduct.lean:126 · uses Cells , ip

15 supporting declarations (lemmas, instances)

ip_eq_weighted lemma — Cells.ip is definitionally equal to WeightedSupport.ip.

hypotheses

c :

Cells I T

A B :

(I × T) → ℝ

conclusion

ip c A B = ip c A B

Proof (Lean source)

lemma ip_eq_weighted (c : Cells I T) (A B : (I × T) → ℝ) : ip c A B = ip c A B := rfl

Causalean.Panel.Cells.ip_eq_weighted · Causalean/Panel/InnerProduct.lean:67
ipMat_eq_weighted lemma — Cells.ipMat is definitionally equal to WeightedSupport.ipMat.

hypotheses

c :

Cells I T

A B :

Fin K → (I × T) → ℝ

conclusion

ipMat c A B = ipMat c A B

Proof (Lean source)

lemma ipMat_eq_weighted (c : Cells I T) (A B : Fin K → (I × T) → ℝ) : ipMat c A B = ipMat c A B := rfl

Causalean.Panel.Cells.ipMat_eq_weighted · Causalean/Panel/InnerProduct.lean:80
ip_def lemma — The panel weighted inner product unfolds to the weighted sum over observed unit-period cells.

hypotheses

c :

Cells I T

A B :

(I × T) → ℝ

conclusion

c.ip A B = ∑ r ∈ c.observed, c.weight r * A r * B r

Proof (Lean source)

@[simp] lemma ip_def (c : Cells I T) (A B : (I × T) → ℝ) : c.ip A B = ∑ r ∈ c.observed, c.weight r * A r * B r := rfl

Causalean.Panel.Cells.ip_def · Causalean/Panel/InnerProduct.lean:91
ip_symm lemma — The panel weighted inner product is symmetric in its two arrays.

hypotheses

c :

Cells I T

A B :

(I × T) → ℝ

conclusion

c.ip A B = c.ip B A

Proof (Lean source)

lemma ip_symm (c : Cells I T) (A B : (I × T) → ℝ) : c.ip A B = c.ip B A := ip_symm c A B

Causalean.Panel.Cells.ip_symm · Causalean/Panel/InnerProduct.lean:96
ip_add_left lemma — The panel weighted inner product is additive in its left array.

hypotheses

c :

Cells I T

A A' B :

(I × T) → ℝ

conclusion

c.ip (A + A') B = c.ip A B + c.ip A' B

Proof (Lean source)

lemma ip_add_left (c : Cells I T) (A A' B : (I × T) → ℝ) : c.ip (A + A') B = c.ip A B + c.ip A' B := ip_add_left c A A' B

Causalean.Panel.Cells.ip_add_left · Causalean/Panel/InnerProduct.lean:101
ip_add_right lemma — The panel weighted inner product is additive in its right array.

hypotheses

c :

Cells I T

A B B' :

(I × T) → ℝ

conclusion

c.ip A (B + B') = c.ip A B + c.ip A B'

Proof (Lean source)

lemma ip_add_right (c : Cells I T) (A B B' : (I × T) → ℝ) : c.ip A (B + B') = c.ip A B + c.ip A B' := ip_add_right c A B B'

Causalean.Panel.Cells.ip_add_right · Causalean/Panel/InnerProduct.lean:106
ip_smul_left lemma — The panel weighted inner product is homogeneous in its left array.

hypotheses

c :

Cells I T

s :

ℝ

A B :

(I × T) → ℝ

conclusion

c.ip (s • A) B = s * c.ip A B

Proof (Lean source)

lemma ip_smul_left (c : Cells I T) (s : ℝ) (A B : (I × T) → ℝ) : c.ip (s • A) B = s * c.ip A B := ip_smul_left c s A B

Causalean.Panel.Cells.ip_smul_left · Causalean/Panel/InnerProduct.lean:111
ip_smul_right lemma — The panel weighted inner product is homogeneous in its right array.

hypotheses

c :

Cells I T

s :

ℝ

A B :

(I × T) → ℝ

conclusion

c.ip A (s • B) = s * c.ip A B

Proof (Lean source)

lemma ip_smul_right (c : Cells I T) (s : ℝ) (A B : (I × T) → ℝ) : c.ip A (s • B) = s * c.ip A B := ip_smul_right c s A B

Causalean.Panel.Cells.ip_smul_right · Causalean/Panel/InnerProduct.lean:116
ip_self_nonneg lemma — The self inner product of any panel array is nonnegative.

hypotheses

c :

Cells I T

A :

(I × T) → ℝ

conclusion

0 ≤ c.ip A A

Proof (Lean source)

lemma ip_self_nonneg (c : Cells I T) (A : (I × T) → ℝ) : 0 ≤ c.ip A A := ip_self_nonneg c A

Causalean.Panel.Cells.ip_self_nonneg · Causalean/Panel/InnerProduct.lean:121
ipMat_apply lemma — The matrix-valued panel inner product has entries equal to scalar inner products of the corresponding array columns.

hypotheses

c :

Cells I T

A B :

Fin K → (I × T) → ℝ

j k :

Fin K

conclusion

c.ipMat A B j k = c.ip (A j) (B k)

Proof (Lean source)

@[simp] lemma ipMat_apply (c : Cells I T) (A B : Fin K → (I × T) → ℝ) (j k : Fin K) : c.ipMat A B j k = c.ip (A j) (B k) := rfl

Causalean.Panel.Cells.ipMat_apply · Causalean/Panel/InnerProduct.lean:132
ipMat_transpose lemma — Swapping the two tuples of arrays transposes the matrix-valued panel inner product.

hypotheses

c :

Cells I T

A B :

Fin K → (I × T) → ℝ

conclusion

(c.ipMat A B).transpose = c.ipMat B A

Proof (Lean source)

lemma ipMat_transpose (c : Cells I T) (A B : Fin K → (I × T) → ℝ) : (c.ipMat A B).transpose = c.ipMat B A := ipMat_transpose c A B

Causalean.Panel.Cells.ipMat_transpose · Causalean/Panel/InnerProduct.lean:138
ipMat_add_left lemma — The matrix-valued panel inner product is additive in its left tuple of arrays.

hypotheses

c :

Cells I T

A A' B :

Fin K → (I × T) → ℝ

conclusion

c.ipMat (A + A') B = c.ipMat A B + c.ipMat A' B

Proof (Lean source)

lemma ipMat_add_left (c : Cells I T) (A A' B : Fin K → (I × T) → ℝ) : c.ipMat (A + A') B = c.ipMat A B + c.ipMat A' B := ipMat_add_left c A A' B

Causalean.Panel.Cells.ipMat_add_left · Causalean/Panel/InnerProduct.lean:144
ipMat_add_right lemma — The matrix-valued panel inner product is additive in its right tuple of arrays.

hypotheses

c :

Cells I T

A B B' :

Fin K → (I × T) → ℝ

conclusion

c.ipMat A (B + B') = c.ipMat A B + c.ipMat A B'

Proof (Lean source)

lemma ipMat_add_right (c : Cells I T) (A B B' : Fin K → (I × T) → ℝ) : c.ipMat A (B + B') = c.ipMat A B + c.ipMat A B' := ipMat_add_right c A B B'

Causalean.Panel.Cells.ipMat_add_right · Causalean/Panel/InnerProduct.lean:150
ipMat_smul_left lemma — The matrix-valued panel inner product is homogeneous in its left tuple of arrays.

hypotheses

c :

Cells I T

s :

ℝ

A B :

Fin K → (I × T) → ℝ

conclusion

c.ipMat (s • A) B = s • c.ipMat A B

Proof (Lean source)

lemma ipMat_smul_left (c : Cells I T) (s : ℝ) (A B : Fin K → (I × T) → ℝ) : c.ipMat (s • A) B = s • c.ipMat A B := ipMat_smul_left c s A B

Causalean.Panel.Cells.ipMat_smul_left · Causalean/Panel/InnerProduct.lean:156
ipMat_smul_right lemma — The matrix-valued panel inner product is homogeneous in its right tuple of arrays.

hypotheses

c :

Cells I T

s :

ℝ

A B :

Fin K → (I × T) → ℝ

conclusion

c.ipMat A (s • B) = s • c.ipMat A B

Proof (Lean source)

lemma ipMat_smul_right (c : Cells I T) (s : ℝ) (A B : Fin K → (I × T) → ℝ) : c.ipMat A (s • B) = s • c.ipMat A B := ipMat_smul_right c s A B

Causalean.Panel.Cells.ipMat_smul_right · Causalean/Panel/InnerProduct.lean:162

Subspace 1 core · 14 supporting This file exposes panel-level names for weighted orthogonal projection, residualization, and cell-array spaces. ★ residualize_in_orthogonal

Panel Subspace Aliases

This file exposes panel-level names for weighted orthogonal projection, residualization, and cell-array spaces. It keeps the panel regression API connected to the generic weighted subspace construction used throughout the library while preserving convenient Cells.* names for projection, residual-maker, residualized-regressor, orthogonality, and idempotence facts.

lemma residualize_in_orthogonal reviewed

Causalean.Panel.Cells

For an array h lying in the nuisance subspace H, the array X residualized against H is orthogonal to h under the panel weighted inner product c.ip.

Formal statement

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

h :

V I T

hH :

h ∈ H

conclusion

c.ip (c.tildeX H X) h = 0

Proof (Lean source)

lemma residualize_in_orthogonal (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) {h : V I T} (hH : h ∈ H) : c.ip (c.tildeX H X) h = 0 := residualize_in_orthogonal c H X hH

Causalean.Panel.Cells.residualize_in_orthogonal · Causalean/Panel/Subspace.lean:122 · uses Cells , V, ip, tildeX

14 supporting declarations (lemmas, instances)

proj_eq_weighted lemma — The panel projection alias is definitionally equal to the generic weighted support projection.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

conclusion

proj c H = proj c H

Proof (Lean source)

lemma proj_eq_weighted (c : Cells I T) (H : Submodule ℝ (V I T)) : proj c H = proj c H := rfl

Causalean.Panel.Cells.proj_eq_weighted · Causalean/Panel/Subspace.lean:52
residualize_eq_weighted lemma — The panel residual-maker alias is definitionally equal to the generic weighted support residual maker.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

conclusion

residualize c H = residualize c H

Proof (Lean source)

lemma residualize_eq_weighted (c : Cells I T) (H : Submodule ℝ (V I T)) : residualize c H = residualize c H := rfl

Causalean.Panel.Cells.residualize_eq_weighted · Causalean/Panel/Subspace.lean:63
tildeX_eq_weighted lemma — The panel residualized-array alias is definitionally equal to the generic weighted support residualized array.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

conclusion

tildeX c H X = tildeX c H X

Proof (Lean source)

lemma tildeX_eq_weighted (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) : tildeX c H X = tildeX c H X := rfl

Causalean.Panel.Cells.tildeX_eq_weighted · Causalean/Panel/Subspace.lean:75
tildeXVec_eq_weighted lemma — The panel column-wise residualization alias is definitionally equal to the generic weighted support column-wise residualization.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

Fin K → V I T

conclusion

tildeXVec c H X = tildeXVec c H X

Proof (Lean source)

lemma tildeXVec_eq_weighted (c : Cells I T) (H : Submodule ℝ (V I T)) (X : Fin K → V I T) : tildeXVec c H X = tildeXVec c H X := rfl

Causalean.Panel.Cells.tildeXVec_eq_weighted · Causalean/Panel/Subspace.lean:90
tildeX_eq lemma — Residualizing a panel array subtracts its nuisance-space projection.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

conclusion

c.tildeX H X = X - c.proj H X

Proof (Lean source)

@[simp] lemma tildeX_eq (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) : c.tildeX H X = X - c.proj H X := tildeX_eq c H X

Causalean.Panel.Cells.tildeX_eq · Causalean/Panel/Subspace.lean:104
residualize_apply lemma — Applying the panel residual maker subtracts the nuisance-space projection.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

conclusion

c.residualize H X = X - c.proj H X

Proof (Lean source)

@[simp] lemma residualize_apply (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) : c.residualize H X = X - c.proj H X := residualize_apply c H X

Causalean.Panel.Cells.residualize_apply · Causalean/Panel/Subspace.lean:110
tildeXVec_apply lemma — Column-wise residualization residualizes each regressor column separately.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

Fin K → V I T

k :

Fin K

conclusion

c.tildeXVec H X k = c.tildeX H (X k)

Proof (Lean source)

@[simp] lemma tildeXVec_apply (c : Cells I T) (H : Submodule ℝ (V I T)) (X : Fin K → V I T) (k : Fin K) : c.tildeXVec H X k = c.tildeX H (X k) := tildeXVec_apply c H X k

Causalean.Panel.Cells.tildeXVec_apply · Causalean/Panel/Subspace.lean:116
residualize_self_of_mem lemma — A nuisance-space array residualizes to zero on observed cells.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

hX :

X ∈ H

r :

I × T

hr :

r ∈ c.observed

conclusion

c.tildeX H X r = 0

Proof (Lean source)

lemma residualize_self_of_mem (c : Cells I T) (H : Submodule ℝ (V I T)) {X : V I T} (hX : X ∈ H) (r : I × T) (hr : r ∈ c.observed) : c.tildeX H X r = 0 := residualize_self_of_mem c H hX r hr

Causalean.Panel.Cells.residualize_self_of_mem · Causalean/Panel/Subspace.lean:129
residualize_idem_apply lemma — Applying the panel residual maker twice agrees with applying it once on observed cells.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

r :

I × T

hr :

r ∈ c.observed

conclusion

c.residualize H (c.residualize H X) r = c.residualize H X r

Proof (Lean source)

lemma residualize_idem_apply (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) (r : I × T) (hr : r ∈ c.observed) : c.residualize H (c.residualize H X) r = c.residualize H X r := residualize_idem_apply c H X r hr

Causalean.Panel.Cells.residualize_idem_apply · Causalean/Panel/Subspace.lean:136
proj_mem lemma — The chosen panel projection of an array lies in the nuisance subspace.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

conclusion

c.proj H X ∈ H

Proof (Lean source)

lemma proj_mem (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) : c.proj H X ∈ H := proj_mem c H X

Causalean.Panel.Cells.proj_mem · Causalean/Panel/Subspace.lean:144
proj_orthogonal lemma — The projection residual is orthogonal to every nuisance-space array under the panel weighted inner product.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

h :

V I T

hH :

h ∈ H

conclusion

c.ip (X - c.proj H X) h = 0

Proof (Lean source)

lemma proj_orthogonal (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) {h : V I T} (hH : h ∈ H) : c.ip (X - c.proj H X) h = 0 := proj_orthogonal c H X hH

Causalean.Panel.Cells.proj_orthogonal · Causalean/Panel/Subspace.lean:149
proj_apply_of_mem lemma — Projecting a nuisance-space array returns the same values on observed cells.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

Y :

V I T

hY :

Y ∈ H

r :

I × T

hr :

r ∈ c.observed

conclusion

c.proj H Y r = Y r

Proof (Lean source)

lemma proj_apply_of_mem (c : Cells I T) (H : Submodule ℝ (V I T)) {Y : V I T} (hY : Y ∈ H) (r : I × T) (hr : r ∈ c.observed) : c.proj H Y r = Y r := proj_apply_of_mem c H hY r hr

Causalean.Panel.Cells.proj_apply_of_mem · Causalean/Panel/Subspace.lean:156
proj_apply_eq_of_mem_orthogonal lemma — Any nuisance-space candidate with the projection orthogonality condition matches the chosen projection on observed cells.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

Y :

V I T

hY :

Y ∈ H

horth :

∀ h ∈ H, c.ip (X - Y) h = 0

r :

I × T

hr :

r ∈ c.observed

conclusion

c.proj H X r = Y r

Proof (Lean source)

lemma proj_apply_eq_of_mem_orthogonal (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) {Y : V I T} (hY : Y ∈ H) (horth : ∀ h ∈ H, c.ip (X - Y) h = 0) (r : I × T) (hr : r ∈ c.observed) : c.proj H X r = Y r := proj_apply_eq_of_mem_orthogonal c H X hY horth r hr

Causalean.Panel.Cells.proj_apply_eq_of_mem_orthogonal · Causalean/Panel/Subspace.lean:163
proj_idem_apply lemma — Applying the chosen panel projection twice agrees with applying it once on observed cells.

hypotheses

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

r :

I × T

hr :

r ∈ c.observed

conclusion

c.proj H (c.proj H X) r = c.proj H X r

Proof (Lean source)

lemma proj_idem_apply (c : Cells I T) (H : Submodule ℝ (V I T)) (X : V I T) (r : I × T) (hr : r ∈ c.observed) : c.proj H (c.proj H X) r = c.proj H X r := proj_idem_apply c H X r hr

Causalean.Panel.Cells.proj_idem_apply · Causalean/Panel/Subspace.lean:173

Observed Panel Cells

Weighted Finite Two-Way Panel Helpers

Bridge to the generic WeightedSupport FWL tower

Adoption Path Helpers

Uniform Balanced Two-Way Panels

L2 Frisch-Waugh-Lovell Instance

Panel Inner Products

Panel Subspace Aliases

Bridge to the generic `WeightedSupport` FWL tower