Panel

Cells 3 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

For finite sets of units and periods with decidable equality, the observed cells of a panel are a finite collection of unit-period pairs equipped with strictly positive weights that sum to one over that collection.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

Fintype I

Fintype T

DecidableEq I

DecidableEq T

def

Cells I T :

Type _

given by

WeightedSupport (I × T)

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

def balanced reviewed

Causalean.Panel.Cells

The balanced panel: every cell is observed and every cell carries weight 1 / (|I| · |T|).

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

def

balanced :

Cells I T

given by

clause 1

observed := Finset.univ

clause 2

observed_nonempty := Finset.univ_nonempty

clause 3

weight _ := (1 : ℝ) / (Fintype.card I * Fintype.card T)

clause 4

weight_pos := by intro r _ have hI : (0 : ℝ) < Fintype.card I := by exact_mod_cast Fintype.card_pos have hT : (0 : ℝ) < Fintype.card T := by exact_mod_cast Fintype.card_pos positivity

clause 5

weight_zero_off := by intro r hr exact (hr (Finset.mem_univ r)).elim

clause 6

weight_sum_one := by have hI : (Fintype.card I : ℝ)

≠ 0 := by have : 0 < Fintype.card I := Fintype.card_pos exact_mod_cast this.ne' have hT : (Fintype.card T : ℝ) ≠ 0 := by have : 0 < Fintype.card T := Fintype.card_pos exact_mod_cast this.ne' rw [Finset.sum_const] have hcard : (Finset.univ : Finset (I × T)).card = Fintype.card I * Fintype.card T := by rw [Finset.card_univ, Fintype.card_prod] rw [hcard, nsmul_eq_mul] push_cast field_simp

Causalean.Panel.Cells.balanced · Causalean/Panel/Cells.lean:80 · uses Cells

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

I :

Type u_1

shared

T :

Type u_2

shared

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.

hypotheses

I :

Type u_1
shared

T :

Type u_2
shared

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

InnerProduct 3 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.

def ip reviewed

Causalean.Panel.Cells

Bare-name alias for c.ip. Defined with the explicit finset-sum body (same as WeightedSupport.ip) so that unfold ip exposes the sum form expected by the pre-refactor proof scripts. Definitionally equal (by rfl) to Causalean.Panel.Weighted.WeightedSupport.ip.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

c :

Cells I T

A B :

(I × T) → ℝ

def

ip c A B :

ℝ

given by

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

Causalean.Panel.Cells.ip · Causalean/Panel/InnerProduct.lean:60 · uses Cells

def ipMat reviewed

Causalean.Panel.Cells

Bare-name alias for the matrix-valued panel inner product. Its (j, k) entry is the scalar weighted inner product of the jth array in A with the kth array in B.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

K :

ℕ

shared

c :

Cells I T

A B :

Fin K → (I × T) → ℝ

def

ipMat c A B :

Matrix (Fin K) (Fin K) ℝ

given by

fun j k => c.ip (A j) (B k)

Causalean.Panel.Cells.ipMat · Causalean/Panel/InnerProduct.lean:73 · uses Cells

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

I :

Type u_1

shared

T :

Type u_2

shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

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:53

def unitMean reviewed

Causalean.Panel.WeightedTwoWayPanel

For a set of units, a finite set of periods, a panel array indexed by units and periods, and a unit, the unit mean is the arithmetic average of that unit's values over all periods.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V :

Unit → Time → ℝ

i :

Unit

def

unitMean V i :

ℝ

given by

(Fintype.card Time : ℝ)⁻¹ * ∑ t, V i t

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

def timeMean reviewed

Causalean.Panel.WeightedTwoWayPanel

For a finite set of units, a set of periods, unit weights that are strictly positive and sum to one, a panel array indexed by units and periods, and a period, the weighted time mean is the weighted average across units of the array at that period.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

w :

UnitWeights Unit

V :

Unit → Time → ℝ

t :

Time

def

timeMean w V t :

ℝ

given by

∑ i, w.p i * V i t

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

def grandMean reviewed

Causalean.Panel.WeightedTwoWayPanel

For a finite set of units, a finite set of periods, unit weights that are strictly positive and sum to one, and a panel array indexed by units and periods, the weighted grand mean is the weighted average across units of their arithmetic means over periods.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

w :

UnitWeights Unit

V :

Unit → Time → ℝ

def

grandMean w V :

ℝ

given by

∑ i, w.p i * unitMean V i

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

def ddot reviewed

Causalean.Panel.WeightedTwoWayPanel

For a finite set of units, a finite set of periods, unit weights that are strictly positive and sum to one, a panel array indexed by units and periods, a unit, and a period, the double-demeaned value is that array value minus its unit mean and weighted time mean plus its weighted grand mean.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

w :

UnitWeights Unit

V :

Unit → Time → ℝ

i :

Unit

t :

Time

def

ddot w V i t :

ℝ

given by

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

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

def inner reviewed

Causalean.Panel.WeightedTwoWayPanel

For a finite set of units, a finite set of periods, unit weights that are strictly positive and sum to one, and two panel arrays, the weighted panel inner product is the sum over every unit and period of the unit weight times the product of the arrays; no uniform-period normalizing factor is included.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

w :

UnitWeights Unit

V W :

Unit → Time → ℝ

def

inner w V W :

ℝ

given by

∑ i, ∑ t, w.p i * (V i t * W i t)

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

abbrev IsUnitTimeAdditive reviewed

Causalean.Panel.WeightedTwoWayPanel

For a set of units, a set of periods, and a panel array indexed by units and periods, the unit-time additive property holds exactly when there exist a real-valued unit-specific function and a real-valued time-specific function whose sum equals the array at every unit-period pair.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

h :

Unit → Time → ℝ

def

IsUnitTimeAdditive h :

Prop

given by

IsUnitTimeAdditive h

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

def unitTimeProjection reviewed

Causalean.Panel.WeightedTwoWayPanel

For a finite set of units, a finite set of periods, unit weights that are strictly positive and sum to one, a panel array indexed by units and periods, a unit, and a period, the unit-time component removed by double demeaning is the unit mean plus the weighted time mean minus the weighted grand mean.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

w :

UnitWeights Unit

V :

Unit → Time → ℝ

i :

Unit

t :

Time

def

unitTimeProjection w V i t :

ℝ

given by

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

Causalean.Panel.WeightedTwoWayPanel.unitTimeProjection · Causalean/Panel/WeightedTwoWayPanel.lean:99 · 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

Unit :

Type u_1

shared

Time :

Type u_2

shared

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 only [sum_algebra_simps] _ = 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:241 · uses IsUnitTimeAdditive , UnitWeights , ddot , inner

def cellSupport reviewed

Causalean.Panel.WeightedTwoWayPanel

For finite, nonempty, distinguishable sets of units and periods and unit weights that are strictly positive and sum to one, the cell-indexed weighted support for the panel treats every unit-period pair as observed and assigns pair $(i,t)$ the weight given by unit $i$ 's weight divided by the number of periods.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

w :

UnitWeights Unit

def

cellSupport w :

WeightedSupport (Unit × Time)

given by

clause 1

observed := univ

clause 2

observed_nonempty := Finset.univ_nonempty

clause 3

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

clause 4

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

clause 5

weight_zero_off := by intro r hr; exact (hr (Finset.mem_univ r)).elim

clause 6

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 simp only [sum_algebra_simps] field_simp simp_rw [hrow] exact w.sum_one

Causalean.Panel.WeightedTwoWayPanel.cellSupport · Causalean/Panel/WeightedTwoWayPanel.lean:281 · 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

Unit :

Type u_1

shared

Time :

Type u_2

shared

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:355 · 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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:106
unitTimeProjection_additive theorem — The removed component is itself unit/time additive.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:112
sub_ddot_eq_unitTimeProjection theorem — Pointwise residual decomposition V - ddot V into the unit/time projection.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:120
ddot_orthogonal_unit theorem — Double-demeaned arrays are orthogonal (in the p-weighted inner product) to arbitrary unit-only functions.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:184
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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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 [sum_algebra_simps] _ = 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 simp only [sum_algebra_simps] _ = 0 := by simp [hcol]

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

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:311
cellSupport_observed lemma — Every unit-period cell is observed in the cell-support bridge.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:316
mem_twoAxisAdditiveSpan_iff lemma — Membership in the two-axis additive span is exactly the panel's IsUnitTimeAdditive predicate after uncurrying.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
Unit × Time → ℝ
shared

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:322
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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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] simp only [sum_algebra_simps] refine Finset.sum_congr rfl fun i _ => Finset.sum_congr rfl fun t _ => ?_ field_simp

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

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

For a panel with a finite horizon of $T$ periods and a finite adoption period $g$ , the finite adoption path is the path whose adoption date is $g$ , rather than the never-treated date.

Definition (Lean source)

parameters

T :

ℕ

g :

Fin T

def

finite g :

WithTop (Fin T)

given by

(g : WithTop (Fin T))

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

def le reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon, an adoption path $a$ , and a period $t$ in that horizon, the treated-by- $t$ predicate holds exactly when the adoption date is no later than $t$ .

Definition (Lean source)

parameters

T :

ℕ

a :

WithTop (Fin T)

t :

Fin T

def

le a t :

Prop

given by

a ≤ (t : WithTop (Fin T))

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

def lt reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon, an adoption path $a$ , and a period $t$ in that horizon, the untreated-at- $t$ predicate holds exactly when $t$ is strictly before the adoption date.

Definition (Lean source)

parameters

T :

ℕ

a :

WithTop (Fin T)

t :

Fin T

def

lt a t :

Prop

given by

(t : WithTop (Fin T)) < a

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

def isFinite reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon and an adoption path $a$ , the finite-path predicate holds exactly when its adoption date is not the never-treated date.

Definition (Lean source)

parameters

T :

ℕ

a :

WithTop (Fin T)

def

isFinite a :

Prop

given by

a ≠ ⊤

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

def isInfinite reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon and an adoption path $a$ , the infinite-path predicate holds exactly when its adoption date is the never-treated date.

Definition (Lean source)

parameters

T :

ℕ

a :

WithTop (Fin T)

def

isInfinite a :

Prop

given by

a = ⊤

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

def isNeverTreated reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon and an adoption path $h$ , the never-treated predicate holds exactly when $h$ has the never-treated adoption date.

Definition (Lean source)

parameters

T :

ℕ

h :

WithTop (Fin T)

def

isNeverTreated h :

Prop

given by

isInfinite h

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

def isEventuallyTreated reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon and an adoption path $h$ , the eventually-treated predicate holds exactly when $h$ has a finite adoption date.

Definition (Lean source)

parameters

T :

ℕ

h :

WithTop (Fin T)

def

isEventuallyTreated h :

Prop

given by

isFinite h

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

def absorbingTreatment reviewed

Causalean.Panel.AdoptionPath

For a finite-period horizon, an adoption path $h$ , and a period $t$ in that horizon, the absorbing treatment indicator equals one exactly when $h$ has adopted by $t$ , and equals zero otherwise.

Definition (Lean source)

parameters

T :

ℕ

h :

WithTop (Fin T)

t :

Fin T

def

absorbingTreatment h t :

ℝ

given by

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:103 · 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:111
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:116

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

For a collection of records, a set of cell labels with decidable equality, a cell map $G$ , and a cell label $g$ , the finite-cell indicator is the real-valued function that equals one for records assigned label $g$ and zero for all other records.

Definition (Lean source)

parameters

R 𝒢 :

Type*

DecidableEq 𝒢

G :

R → 𝒢

g :

𝒢

def

finiteCellIndicator G g :

R → ℝ

given by

cellIndicator G g

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

abbrev finiteIndicatorSpan reviewed

Causalean.Panel.CellBridge

For a collection of records, a cell map $G$ , and a finite set of cell labels with decidable equality, the finite one-axis indicator span is the real vector space generated by the indicators of the cells of $G$ .

Definition (Lean source)

parameters

R 𝒢 :

Type*

Fintype 𝒢

DecidableEq 𝒢

G :

R → 𝒢

def

finiteIndicatorSpan G :

Submodule ℝ (R → ℝ)

given by

indicatorSpan G

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

abbrev finiteTwoAxisIndicatorSpan reviewed

Causalean.Panel.CellBridge

For a collection of records, cell maps $G$ and $T$ , and their finite label sets with decidable equality, the finite two-axis indicator span is the real vector space generated jointly by the indicators of the cells of $G$ and of $T$ .

Definition (Lean source)

parameters

R 𝒢 𝒯 :

Type*

Fintype 𝒢

DecidableEq 𝒢

Fintype 𝒯

DecidableEq 𝒯

G :

R → 𝒢

T :

R → 𝒯

def

finiteTwoAxisIndicatorSpan G T :

Submodule ℝ (R → ℝ)

given by

twoAxisIndicatorSpan G T

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

def cellIndicator reviewed

Causalean.Panel.CellBridge

For a sample space equipped with a σ-algebra, a set of cell labels, a cell-assignment map $X$ , and a cell label $i$ , the cell indicator is the real-valued function equal to one exactly on the event that $X$ equals $i$ , and zero elsewhere.

Definition (Lean source)

parameters

Ω ι :

Type*

MeasurableSpace Ω

X :

Ω → ι

i :

ι

def

cellIndicator X i :

Ω → ℝ

given by

fun ω => indicator {ω' | X ω' = i} (fun _ => (1 : ℝ)) ω

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

def indicatorSpan reviewed

Causalean.Panel.CellBridge

For a measurable sample space, a finite cell-label set with decidable equality and measurable singleton events, a finite measure $μ$ , a measurable cell-assignment map $G$ , the one-axis indicator span is the class of square-integrable real functions that agree almost everywhere with a finite linear combination of the indicators of the cells of $G$ .

Definition (Lean source)

parameters

Ω 𝒢 :

Type*

MeasurableSpace Ω

Fintype 𝒢

DecidableEq 𝒢

MeasurableSpace 𝒢

MeasurableSingletonClass 𝒢

μ :

Measure Ω

IsFiniteMeasure μ

G :

Ω → 𝒢

G_meas :

Measurable G

def

indicatorSpan μ G G_meas :

LinearL2Class μ

given by

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:77 · uses LinearL2Class

def twoAxisIndicatorSpan reviewed

Causalean.Panel.CellBridge

For a measurable sample space, finite cell-label sets with decidable equality and measurable singleton events, a finite measure $μ$ , and measurable cell-assignment maps $G$ and $T$ , the two-axis indicator span is the class of square-integrable real functions that agree almost everywhere with the sum of a finite linear combination of $G$ -cell indicators and a finite linear combination of $T$ -cell indicators.

Definition (Lean source)

parameters

Ω 𝒢 𝒯 :

Type*

MeasurableSpace Ω

Fintype 𝒢

DecidableEq 𝒢

MeasurableSpace 𝒢

MeasurableSingletonClass 𝒢

Fintype 𝒯

DecidableEq 𝒯

MeasurableSpace 𝒯

MeasurableSingletonClass 𝒯

μ :

Measure Ω

IsFiniteMeasure μ

G :

Ω → 𝒢

T :

Ω → 𝒯

G_meas :

Measurable G

T_meas :

Measurable T

def

twoAxisIndicatorSpan μ G T G_meas T_meas :

LinearL2Class μ

given by

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:159 · uses LinearL2Class

def cellMass reviewed

Causalean.Panel.CellBridge

For a sample space equipped with a σ-algebra, a set of cell labels, a measure $μ$ , a cell-assignment map $G$ , and a cell label $g$ , the cell mass is the real-valued mass that $μ$ assigns to the event that $G$ equals $g$ .

Definition (Lean source)

parameters

Ω 𝒢 :

Type*

MeasurableSpace Ω

μ :

Measure Ω

G :

Ω → 𝒢

g :

𝒢

def

cellMass μ G g :

ℝ

given by

(μ {ω | G ω = g}).toReal

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

def jointCellMass reviewed

Causalean.Panel.CellBridge

For a sample space equipped with a σ-algebra, sets of labels for two cell maps, a measure $μ$ , cell-assignment maps $G$ and $T$ , and labels $g$ and $t$ , the joint cell mass is the real-valued mass that $μ$ assigns to the event that $G=g$ and $T=t$ .

Definition (Lean source)

parameters

Ω 𝒢 𝒯 :

Type*

MeasurableSpace Ω

μ :

Measure Ω

G :

Ω → 𝒢

T :

Ω → 𝒯

g :

𝒢

t :

𝒯

def

jointCellMass μ G T g t :

ℝ

given by

(μ {ω | G ω = g ∧ T ω = t}).toReal

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

def cellMean reviewed

Causalean.Panel.CellBridge

For a sample space equipped with a σ-algebra, a set of cell labels, a measure $μ$ , a real-valued function $F$ , a cell-assignment map $G$ , and a cell label $g$ , the cell mean is the integral of $F$ over the event $G=g$ , divided by that event's real-valued mass.

Definition (Lean source)

parameters

Ω 𝒢 :

Type*

MeasurableSpace Ω

μ :

Measure Ω

F :

Ω → ℝ

G :

Ω → 𝒢

g :

𝒢

def

cellMean μ F G g :

ℝ

given by

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

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

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:406

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:274
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:285
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:297
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:334
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:345
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:482

Subspace 6 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.

abbrev V reviewed

Causalean.Panel.Cells

Cell-array space: scalar-valued arrays on I × T.

Definition (Lean source)

parameters

I T :

Type*

def

V I T :

Type _

given by

(I × T) → ℝ

Causalean.Panel.Cells.V · Causalean/Panel/Subspace.lean:31

def proj reviewed

Causalean.Panel.Cells

Bare-name alias for c.proj. Definitionally equal to Causalean.Panel.Weighted.WeightedSupport.proj.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

c :

Cells I T

H :

Submodule ℝ (V I T)

def

proj c H :

V I T →ₗ[ℝ] V I T

given by

proj c H

Causalean.Panel.Cells.proj · Causalean/Panel/Subspace.lean:46 · uses Cells , V

def residualize reviewed

Causalean.Panel.Cells

Bare-name alias for c.residualize. Definitionally equal to Causalean.Panel.Weighted.WeightedSupport.residualize.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

c :

Cells I T

H :

Submodule ℝ (V I T)

def

residualize c H :

V I T →ₗ[ℝ] V I T

given by

LinearMap.id - c.proj H

Causalean.Panel.Cells.residualize · Causalean/Panel/Subspace.lean:57 · uses Cells , V

def tildeX reviewed

Causalean.Panel.Cells

Bare-name alias for c.tildeX. Same body as Causalean.Panel.Weighted.WeightedSupport.tildeX (defined as residualize H X) so that unfold tildeX exposes the residualized form.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

V I T

def

tildeX c H X :

V I T

given by

c.residualize H X

Causalean.Panel.Cells.tildeX · Causalean/Panel/Subspace.lean:68 · uses Cells , V

def tildeXVec reviewed

Causalean.Panel.Cells

Bare-name alias for c.tildeXVec. Same body as Causalean.Panel.Weighted.WeightedSupport.tildeXVec so that unfold tildeXVec exposes the column-by-column form.

Definition (Lean source)

parameters

I :

Type u_1

shared

T :

Type u_2

shared

K :

ℕ

shared

c :

Cells I T

H :

Submodule ℝ (V I T)

X :

Fin K → V I T

def

tildeXVec c H X :

Fin K → V I T

given by

fun k => c.tildeX H (X k)

Causalean.Panel.Cells.tildeXVec · Causalean/Panel/Subspace.lean:83 · uses Cells , V

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

I :

Type u_1

shared

T :

Type u_2

shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

K :

ℕ
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

I :

Type u_1
shared

T :

Type u_2
shared

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

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

For a finite set of units whose cardinality is strictly positive, the uniform unit-weight vector assigns every unit the reciprocal of the number of units.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

hU :

0 < Fintype.card Unit

def

uniformWeights hU :

WeightedTwoWayPanel.UnitWeights Unit

given by

⟨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

For a finite set of units, a finite set of periods, a real-valued unit-period array, and a unit, the unit mean is the arithmetic average of that unit's array values over all periods.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V :

Unit → Time → ℝ

i :

Unit

def

unitMean V i :

ℝ

given by

(Fintype.card Time : ℝ)⁻¹ * ∑ t, V i t

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

def timeMean reviewed

Causalean.Panel.UniformTwoWayPanel

For a finite set of units, a finite set of periods, a real-valued unit-period array, and a period, the time mean is the arithmetic average of that period's array values over all units.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V :

Unit → Time → ℝ

t :

Time

def

timeMean V t :

ℝ

given by

(Fintype.card Unit : ℝ)⁻¹ * ∑ i, V i t

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

def grandMean reviewed

Causalean.Panel.UniformTwoWayPanel

For a finite set of units, a finite set of periods, and a real-valued unit-period array, the grand mean is the arithmetic average of its values over all unit-period pairs.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V :

Unit → Time → ℝ

def

grandMean V :

ℝ

given by

((Fintype.card Unit : ℝ) * (Fintype.card Time : ℝ))⁻¹ * ∑ i, ∑ t, V i t

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

def ddot reviewed

Causalean.Panel.UniformTwoWayPanel

For a finite set of units, a finite set of periods, a real-valued unit-period array, a unit, and a period, the double-demeaned value equals the array value minus its unit mean and period mean plus its grand mean.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V :

Unit → Time → ℝ

i :

Unit

t :

Time

def

ddot V i t :

ℝ

given by

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

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

def inner reviewed

Causalean.Panel.UniformTwoWayPanel

For a finite set of units, a finite set of periods, and two real-valued unit-period arrays, the unnormalized uniform inner product is the sum, over all unit-period pairs, of the product of their values.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V W :

Unit → Time → ℝ

def

inner V W :

ℝ

given by

∑ i, ∑ t, V i t * W i t

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

def finiteResidualizedCoefficient reviewed

Causalean.Panel.UniformTwoWayPanel

For a finite set of units, a finite set of periods, and a residualized regressor and residualized outcome array, the finite residualized coefficient is their unnormalized inner product divided by the regressor's unnormalized self-inner-product.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

Dtilde Ytilde :

Unit → Time → ℝ

def

finiteResidualizedCoefficient Dtilde Ytilde :

ℝ

given by

inner Dtilde Ytilde / inner Dtilde Dtilde

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

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

Unit :

Type u_1

shared

Time :

Type u_2

shared

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:200 · uses finiteResidualizedCoefficient , inner

abbrev IsUnitTimeAdditive reviewed

Causalean.Panel.UniformTwoWayPanel

For a set of units, a set of periods, and a real-valued unit-period array, the unit-time additive condition holds precisely when there exist a real-valued unit function and a real-valued period function whose sum equals the array at every unit-period pair.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

h :

Unit → Time → ℝ

def

IsUnitTimeAdditive h :

Prop

given by

IsUnitTimeAdditive h

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

def unitTimeProjection reviewed

Causalean.Panel.UniformTwoWayPanel

For a finite set of units, a finite set of periods, a real-valued unit-period array, a unit, and a period, the unit-time projection is that unit's mean plus that period's mean minus the grand mean.

Definition (Lean source)

parameters

Unit :

Type u_1

shared

Time :

Type u_2

shared

V :

Unit → Time → ℝ

i :

Unit

t :

Time

def

unitTimeProjection V i t :

ℝ

given by

unitMean V i + timeMean V t - grandMean V

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

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

Unit :

Type u_1

shared

Time :

Type u_2

shared

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:388 · 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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:109
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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:117
ddot_eq_weighted theorem — Uniform double-demeaning is weighted double-demeaning with uniform unit weights.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:139
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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:150
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

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:181
ddot_reconstruct theorem — Reconstruction identity V_it = ddot V_it + unitMean V_i + timeMean V_t - grandMean V.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:311
unitTimeProjection_additive theorem — The removed component is itself unit/time additive.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:318
sub_ddot_eq_unitTimeProjection theorem — Pointwise residual decomposition V - ddot V into the unit/time projection.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:326
ddot_orthogonal_unit theorem — Double-demeaned arrays are orthogonal to arbitrary unit-only functions.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:333
ddot_orthogonal_time theorem — Double-demeaned arrays are orthogonal to arbitrary time-only functions.

hypotheses

Unit :

Type u_1
shared

Time :

Type u_2
shared

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:361

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

α :

Type u_1

Measure α

shared

K :

ℕ

shared

H :

Submodule ℝ ↥(Lp ℝ 2 μ)

shared

X :

Fin K → ↥(Lp ℝ 2 μ)

shared

Y :

↥(Lp ℝ 2 μ)

shared

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 — For a measurable sample space, a measure on that sample space, and a finite-dimensional real linear subspace of the square-integrable real functions under that measure, an orthogonal projection onto that subspace exists.

parameters

α :

Type u_1
Measure α
shared

H :

Submodule ℝ (Lp ℝ 2 μ)
FiniteDimensional ℝ H

instance

hasOrthogonalProjection_of_finiteDimensional H :
H.HasOrthogonalProjection

given by

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

α :

Type u_1
Measure α
shared

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

α :

Type u_1
Measure α
shared

K :

ℕ
shared

H :

Submodule ℝ ↥(Lp ℝ 2 μ)
shared

X :

Fin K → ↥(Lp ℝ 2 μ)
shared

Y :

↥(Lp ℝ 2 μ)
shared

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

α :

Type u_1
Measure α
shared

K :

ℕ
shared

H :

Submodule ℝ ↥(Lp ℝ 2 μ)
shared

X :

Fin K → ↥(Lp ℝ 2 μ)
shared

Y :

↥(Lp ℝ 2 μ)
shared

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

Observed Panel Cells

Panel Inner Products

Weighted Finite Two-Way Panel Helpers

Bridge to the generic WeightedSupport FWL tower

Adoption Path Helpers

Panel Subspace Aliases

Uniform Balanced Two-Way Panels

L2 Frisch-Waugh-Lovell Instance

Bridge to the generic `WeightedSupport` FWL tower