Panel.PO · Causalean Library

CellPO 8 core · 0 supporting This file provides the potential-outcomes foundation for a finite panel: weighted observed unit-period cells, a random treatment path, cell-specific exposures and baseline exposures, potential outcomes, and factual outco ★ DSigmaAlg_le

Cell-level panel potential outcomes

This file provides the potential-outcomes foundation for a finite panel: weighted observed unit-period cells, a random treatment path, cell-specific exposures and baseline exposures, potential outcomes, and factual outcomes. It also defines realized exposure and outcome, the σ-algebra generated by the treatment path, and the conditional baseline and exposure-response functions used by the panel-regression layer.

structure PanelPOSystem reviewed

Causalean.Panel

A panel potential-outcomes system pairs finite unit and time index sets with a finite collection of observed unit-period cells carrying positive normalized weights, a treatment-path-valued random variable D that is measurable in every unit-period coordinate, a cell-specific exposure mapping e together with a baseline exposure e0, a family of potential outcomes Y at each cell and exposure that is measurable and integrable, and a family of factual observed outcomes Yobs stored independently of the potential-outcome schedule that is likewise measurable and integrable.

Definition (Lean source)

fields

Unit index type.

I :

Type*

Time index type.

T :

Type*

fintypeI :

Fintype I

fintypeT :

Fintype T

decI :

DecidableEq I

decT :

DecidableEq T

Observed unit-period cells with positive normalized weights.

cells :

Cells I T

Action type for treatment assignments.

A :

Type*

Observed-cell-indexed exposure set `E_r`.

E :

(r : I × T) → r ∈ cells.observed → Type*

Each observed-cell exposure set carries a measurable structure.

measE :

∀ r hr, MeasurableSpace (E r hr)

Exposure mapping `e_r : (I → T → A) → E_r` for observed cells.

e :

∀ r hr

if

TreatmentPath I T A

then

E r hr

Baseline exposure `e_r^0 ∈ E_r` for observed cells.

e0 :

∀ r hr, E r hr

Sample space.

Ω :

Type*

MeasurableSpace Ω

measA :

MeasurableSpace A

Probability measure.

μ :

Measure Ω

IsProbabilityMeasure μ

Treatment path random variable `D : Ω → I → T → A`.

D :

Ω → TreatmentPath I T A

`D` is measurable as a map into the function space. Encoded cellwise: each `(D ·) i t : Ω → A` is measurable.

D_meas :

∀ i t, Measurable (fun ω => D ω i t)

Cell-level potential outcome family `Y r e : Ω → ℝ` on observed cells.

Y :

(r : I × T) → (hr : r ∈ cells.observed) → E r hr → Ω → ℝ

Each potential outcome is measurable.

Y_meas :

∀ r hr e, Measurable (Y r hr e)

Each potential outcome is integrable.

Y_integrable :

∀ r hr e, Integrable (Y r hr e) μ

Factual observed outcome family on observed cells.

Yobs :

(r : I × T) → r ∈ cells.observed → Ω → ℝ

Each factual observed outcome is measurable.

Yobs_meas :

∀ r hr, Measurable (Yobs r hr)

Each factual observed outcome is integrable.

Yobs_integrable :

∀ r hr, Integrable (Yobs r hr) μ

Causalean.Panel.PanelPOSystem · Causalean/Panel/PO/CellPO.lean:46

def observedExposure reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system, an observed unit-period cell, and a sample point, the realized exposure is the cell's exposure mapping applied to the treatment path realized at that sample point.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

r :

P.I × P.T

hr :

r ∈ P.cells.observed

ω :

P.Ω

def

observedExposure P r hr ω :

P.E r hr

given by

P.e r hr (P.D ω)

Causalean.Panel.PanelPOSystem.observedExposure · Causalean/Panel/PO/CellPO.lean:115 · uses PanelPOSystem

def observedY reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system, an observed unit-period cell, and a sample point, the factual observed outcome is the outcome stored for that cell and sample point.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

r :

P.I × P.T

hr :

r ∈ P.cells.observed

ω :

P.Ω

def

observedY P r hr ω :

ℝ

given by

P.Yobs r hr ω

Causalean.Panel.PanelPOSystem.observedY · Causalean/Panel/PO/CellPO.lean:122 · uses PanelPOSystem

def DSigmaAlg reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system, the treatment-path σ-algebra is the smallest σ-algebra on the sample space that makes the treatment assigned to every unit in every period measurable.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

def

DSigmaAlg P :

MeasurableSpace P.Ω

given by

⨆ (i : P.I) (t : P.T), comap (fun ω => P.D ω i t) inferInstance

Causalean.Panel.PanelPOSystem.DSigmaAlg · Causalean/Panel/PO/CellPO.lean:131 · uses PanelPOSystem

lemma DSigmaAlg_le reviewed

Causalean.Panel.PanelPOSystem

The σ-algebra generated by the treatment path D, σ(D), is a sub-σ-algebra of the ambient σ-algebra on the outcome space Ω.

Formal statement

hypotheses

P :

PanelPOSystem

shared

conclusion

P.DSigmaAlg ≤ (inferInstance : MeasurableSpace P.Ω)

Proof (Lean source)

lemma DSigmaAlg_le : P.DSigmaAlg ≤ (inferInstance : MeasurableSpace P.Ω) := by rw [DSigmaAlg] exact iSup_le (fun i => iSup_le (fun t => measurable_iff_comap_le.mp (P.D_meas i t)))

Causalean.Panel.PanelPOSystem.DSigmaAlg_le · Causalean/Panel/PO/CellPO.lean:140 · uses PanelPOSystem , DSigmaAlg

def m0 reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system and an observed unit-period cell, the baseline conditional mean, evaluated at each sample point, is the conditional expectation of that cell's potential outcome under its baseline exposure given the treatment-path σ-algebra.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

r :

P.I × P.T

hr :

r ∈ P.cells.observed

def

m0 P r hr :

P.Ω → ℝ

given by

condExp P.DSigmaAlg P.μ (P.Y r hr (P.e0 r hr))

Causalean.Panel.PanelPOSystem.m0 · Causalean/Panel/PO/CellPO.lean:147 · uses PanelPOSystem

def tau reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system, an observed unit-period cell, and an exposure available at that cell, the cell-level exposure response, evaluated at each sample point, is the conditional expectation given the treatment-path σ-algebra of the potential outcome under that exposure minus the potential outcome under the cell's baseline exposure.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

r :

P.I × P.T

hr :

r ∈ P.cells.observed

e :

P.E r hr

def

tau P r hr e :

P.Ω → ℝ

given by

condExp P.DSigmaAlg P.μ (fun ω => P.Y r hr e ω - P.Y r hr (P.e0 r hr) ω)

Causalean.Panel.PanelPOSystem.tau · Causalean/Panel/PO/CellPO.lean:154 · uses PanelPOSystem

def realizedTau reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system, an observed unit-period cell, and a sample point, the realized exposure response is that cell's exposure response at the exposure induced by the treatment path realized at the sample point.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

r :

P.I × P.T

hr :

r ∈ P.cells.observed

ω :

P.Ω

def

realizedTau P r hr ω :

ℝ

given by

P.tau r hr (P.observedExposure r hr ω) ω

Causalean.Panel.PanelPOSystem.realizedTau · Causalean/Panel/PO/CellPO.lean:164 · uses PanelPOSystem

Consistency 3 core · 0 supporting This file states the panel consistency property for a PanelPOSystem. ★ panelConsistency_holds

Panel Consistency

This file states the panel consistency property for a PanelPOSystem. The predicate PanelPOSystem.observedY_eq_potentialOutcome is the pointwise observed-cell equality, while PanelConsistency requires it for every observed cell and sample point. The lemma panelConsistency_holds exposes the equality directly from the assumption.

def observedY_eq_potentialOutcome reviewed

Causalean.Panel.PanelPOSystem

For a panel potential-outcomes system, an observed unit-period cell, and a sample point, pointwise consistency is the assertion that the factual observed outcome equals the potential outcome at that cell under the exposure realized at that sample point.

Definition (Lean source)

parameters

P :

PanelPOSystem

shared

r :

P.I × P.T

hr :

r ∈ P.cells.observed

ω :

P.Ω

def

observedY_eq_potentialOutcome P r hr ω :

Prop

given by

P.observedY r hr ω = P.Y r hr (P.observedExposure r hr ω) ω

Causalean.Panel.PanelPOSystem.observedY_eq_potentialOutcome · Causalean/Panel/PO/Consistency.lean:34 · uses PanelPOSystem

def PanelConsistency reviewed

Causalean.Panel

For a panel potential-outcomes system, the panel consistency condition requires that, for every observed unit-period cell and every sample point, the factual observed outcome equals the potential outcome at that cell under the exposure realized at that sample point.

Definition (Lean source)

parameters

P :

PanelPOSystem

r :

P.I × P.T

hr :

r ∈ P.cells.observed

ω :

P.Ω

def

PanelConsistency P :

Prop

given by

P.observedY_eq_potentialOutcome r hr ω

Causalean.Panel.PanelConsistency · Causalean/Panel/PO/Consistency.lean:44 · uses PanelPOSystem

lemma panelConsistency_holds reviewed

Causalean.Panel

If panel consistency holds for the panel potential-outcome system P, then the factual observed outcome equals the potential outcome evaluated at the realized exposure, for every observed unit-period cell and every sample point.

Formal statement

hypotheses

P :

PanelPOSystem

hP :

PanelConsistency P

r :

P.I × P.T

hr :

r ∈ P.cells.observed

ω :

P.Ω

conclusion

P.observedY r hr ω = P.Y r hr (P.observedExposure r hr ω) ω

Proof (Lean source)

lemma panelConsistency_holds (P : PanelPOSystem) (hP : PanelConsistency P) : ∀ (r : P.I × P.T) (hr : r ∈ P.cells.observed) (ω : P.Ω), P.observedY r hr ω = P.Y r hr (P.observedExposure r hr ω) ω := hP

Causalean.Panel.panelConsistency_holds · Causalean/Panel/PO/Consistency.lean:51 · uses PanelConsistency , PanelPOSystem , observedExposure , observedY

Exposure 2 core · 0 supporting This file defines Exposure, a cell-specific map from a realized TreatmentPath to a cell-dependent exposure type, and BaselineExposure, a distinguished baseline exposure for each cell.

Exposure Mappings

This file defines Exposure, a cell-specific map from a realized TreatmentPath to a cell-dependent exposure type, and BaselineExposure, a distinguished baseline exposure for each cell. These objects are the potential-outcome interface between treatment histories and cell-level responses.

def Exposure reviewed

Causalean.Panel

For a set of units, a set of periods, a treatment-value set, and a cell-specific exposure set, an exposure mapping assigns to every unit-period cell and every realized treatment path an exposure in that cell's exposure set.

Definition (Lean source)

parameters

I T A :

Type*

E :

I × T → Type*

def

Exposure I T A E :

Type _

given by

(r : I × T) → TreatmentPath I T A → E r

Causalean.Panel.Exposure · Causalean/Panel/PO/Exposure.lean:34

def BaselineExposure reviewed

Causalean.Panel

For a set of units, a set of periods, and a cell-specific exposure set, a baseline exposure assigns a distinguished exposure to every unit-period cell.

Definition (Lean source)

parameters

I T :

Type*

E :

I × T → Type*

def

BaselineExposure E :

Type _

given by

(r : I × T) → E r

Causalean.Panel.BaselineExposure · Causalean/Panel/PO/Exposure.lean:40

PopulationCells 5 core · 10 supporting This file provides the shared finite-cell population substrate on which the panel estimand-characterization population bridges are built: a finite measurable partition of a probability space into positive-mass cells, tog ★ mean_consistency

Population cell partition

This file provides the shared finite-cell population substrate on which the panel estimand-characterization population bridges are built: a finite measurable partition of a probability space into positive-mass cells, together with cell masses, cell-conditional means, and their basic identities.

structure CellPartition reviewed

Causalean.Panel.PO

A finite measurable partition of a probability space (Ω, μ) into positive-mass cells indexed by a finite type ι: an assignment of a cell to each index such that every cell is measurable, distinct cells are pairwise disjoint, the cells cover the whole space, and every cell has strictly positive probability mass.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

μ :

Measure Ω

ι :

Type*

Fintype ι

fields

The cell assigned to index `i` (e.g. `{ω | G ω = i}`).

cell :

ι → Set Ω

Each cell is measurable.

cell_meas :

∀ i, MeasurableSet (cell i)

Distinct cells are disjoint.

cell_disj :

Pairwise (onFun Disjoint cell)

The cells cover the whole space.

cell_cov :

(⋃ i, cell i) = univ

Every cell has positive real mass.

cell_pos :

∀ i, 0 < (μ (cell i)).toReal

Causalean.Panel.PO.CellPartition · Causalean/Panel/PO/PopulationCells.lean:51

def cellPartitionOfClassifier reviewed

Causalean.Panel.PO

For a measurable sample space, a finite index set, a measure, a classifier assigning each sample point an index, measurable classifier level sets, and strictly positive real mass for every level set, the classifier-induced cell partition assigns each index its classifier level set.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

ι :

Type*

Fintype ι

μ :

Measure Ω

g :

Ω → ι

hmeas :

∀ i, MeasurableSet (g ⁻¹' {i})

hpos :

∀ i, 0 < (μ (g ⁻¹' {i})).toReal

def

cellPartitionOfClassifier μ g hmeas hpos :

CellPartition μ ι

given by

clause 1

cell i := g ⁻¹' {i}

clause 2

cell_meas := hmeas

clause 3

cell_disj := fun _a _b hab => Disjoint.preimage g (Set.disjoint_singleton.mpr hab)

clause 4

cell_cov := by ext ω; simp

clause 5

cell_pos := hpos

Causalean.Panel.PO.cellPartitionOfClassifier · Causalean/Panel/PO/PopulationCells.lean:68 · uses CellPartition

def mass reviewed

Causalean.Panel.PO.CellPartition

For a measurable sample space, a measure, a finite index set, a cell partition, and one of its indices, the cell mass is the real-valued measure of that index's cell.

Definition (Lean source)

parameters

Ω :

Type u_1

Measure Ω

shared

ι :

Type u_2

shared

P :

CellPartition μ ι

i :

ι

def

mass P i :

ℝ

given by

(μ (P.cell i)).toReal

Causalean.Panel.PO.CellPartition.mass · Causalean/Panel/PO/PopulationCells.lean:96 · uses CellPartition

def mean reviewed

Causalean.Panel.PO.CellPartition

For a measurable sample space, a measure, a finite index set, a cell partition, a real-valued variable on the sample space, and one of the partition's indices, the cell-conditional mean is that variable's integral over the indexed cell divided by the cell's real-valued mass.

Definition (Lean source)

parameters

Ω :

Type u_1

Measure Ω

shared

ι :

Type u_2

shared

P :

CellPartition μ ι

f :

Ω → ℝ

i :

ι

def

mean P f i :

ℝ

given by

normalizedRestrictedIntegral μ (P.cell i) f

Causalean.Panel.PO.CellPartition.mean · Causalean/Panel/PO/PopulationCells.lean:101 · uses CellPartition

theorem mean_consistency reviewed

Causalean.Panel.PO.CellPartition

Cell-mean consistency descent. On a cell where the treatment value d is binary, d ∈ {0,1}, and pointwise potential-outcome consistency Y = Y0 + d·(Y1 − Y0) holds throughout the cell, the cell-conditional means satisfy the same identity: E[Y ∣ cell] = E[Y0 ∣ cell] + d·(E[Y1 ∣ cell] − E[Y0 ∣ cell]).

Formal statement

hypotheses

Ω :

Type u_1

Measure Ω

shared

ι :

Type u_2

shared

P :

CellPartition μ ι

i :

ι

Y Y0 Y1 :

Ω → ℝ

d :

ℝ

hd :

d = 0 ∨ d = 1

hcons :

∀ ω ∈ P.cell i, Y ω = Y0 ω + d * (Y1 ω - Y0 ω)

conclusion

P.mean Y i = P.mean Y0 i + d * (P.mean Y1 i - P.mean Y0 i)

Proof (Lean source)

theorem mean_consistency (P : CellPartition μ ι) (i : ι) (Y Y0 Y1 : Ω → ℝ) {d : ℝ} (hd : d = 0 ∨ d = 1) (hcons : ∀ ω ∈ P.cell i, Y ω = Y0 ω + d * (Y1 ω - Y0 ω)) : P.mean Y i = P.mean Y0 i + d * (P.mean Y1 i - P.mean Y0 i) := by rcases hd with h0 | h1 · subst h0 have hY : P.mean Y i = P.mean Y0 i := P.mean_congr_on i (fun ω hω => by rw [hcons ω hω]; ring) rw [hY]; ring · subst h1 have hY : P.mean Y i = P.mean Y1 i := P.mean_congr_on i (fun ω hω => by rw [hcons ω hω]; ring) rw [hY]; ring

Causalean.Panel.PO.CellPartition.mean_consistency · Causalean/Panel/PO/PopulationCells.lean:168 · uses CellPartition , mean

10 supporting declarations (lemmas, instances)

cellPartitionOfClassifier_cell theorem

hypotheses

Ω :

Type u_1
shared

ι :

Type*
Fintype ι

μ :

Measure Ω

g :

Ω → ι

hmeas :

∀ i, MeasurableSet (g ⁻¹' {i})

hpos :

∀ i, 0 < (μ (g ⁻¹' {i})).toReal

i :

ι

conclusion

(cellPartitionOfClassifier μ g hmeas hpos).cell i = g ⁻¹' {i}

Proof (Lean source)

@[simp] theorem cellPartitionOfClassifier_cell {ι : Type*} [Fintype ι] (μ : Measure Ω) (g : Ω → ι) (hmeas : ∀ i, MeasurableSet (g ⁻¹' {i})) (hpos : ∀ i, 0 < (μ (g ⁻¹' {i})).toReal) (i : ι) : (cellPartitionOfClassifier μ g hmeas hpos).cell i = g ⁻¹' {i} := rfl

Causalean.Panel.PO.CellPartition.cellPartitionOfClassifier_cell · Causalean/Panel/PO/PopulationCells.lean:90
mass_pos theorem — Every cell has strictly positive mass.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

i :

ι

conclusion

0 < P.mass i

Proof (Lean source)

theorem mass_pos (P : CellPartition μ ι) (i : ι) : 0 < P.mass i := P.cell_pos i

Causalean.Panel.PO.CellPartition.mass_pos · Causalean/Panel/PO/PopulationCells.lean:108
mass_ne_zero theorem — Every cell has nonzero mass.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

i :

ι

conclusion

P.mass i ≠ 0

Proof (Lean source)

theorem mass_ne_zero (P : CellPartition μ ι) (i : ι) : P.mass i ≠ 0 := (P.mass_pos i).ne'

Causalean.Panel.PO.CellPartition.mass_ne_zero · Causalean/Panel/PO/PopulationCells.lean:111
mass_sum_one theorem — Masses sum to one. The cell probabilities of a partition of a probability space add to 1.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

IsProbabilityMeasure μ

conclusion

∑ i, P.mass i = 1

Proof (Lean source)

theorem mass_sum_one (P : CellPartition μ ι) [IsProbabilityMeasure μ] : ∑ i, P.mass i = 1 := by have hsum : ∑ i, μ (P.cell i) = 1 := by have h := measure_iUnion (μ := μ) P.cell_disj P.cell_meas rw [P.cell_cov, measure_univ, tsum_fintype] at h exact h.symm calc ∑ i, P.mass i = (∑ i, μ (P.cell i)).toReal := (ENNReal.toReal_sum (fun i _ => measure_ne_top μ (P.cell i))).symm _ = (1 : ENNReal).toReal := by rw [hsum] _ = 1 := ENNReal.toReal_one

Causalean.Panel.PO.CellPartition.mass_sum_one · Causalean/Panel/PO/PopulationCells.lean:115
integral_eq_sum_mass_mul_mean theorem — Finite-partition total law. The integral of f is the mass-weighted sum of its cell means: ∫ f = ∑ i, π_i · E[f ∣ cell i].

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

IsFiniteMeasure μ

f :

Ω → ℝ

hf :

Integrable f μ

conclusion

∫ ω, f ω ∂μ = ∑ i, P.mass i * P.mean f i

Proof (Lean source)

theorem integral_eq_sum_mass_mul_mean (P : CellPartition μ ι) [IsFiniteMeasure μ] (f : Ω → ℝ) (hf : Integrable f μ) : ∫ ω, f ω ∂μ = ∑ i, P.mass i * P.mean f i := integral_eq_sum_measure_mul_eventCondExp μ P.cell P.cell_meas P.cell_disj P.cell_cov f hf

Causalean.Panel.PO.CellPartition.integral_eq_sum_mass_mul_mean · Causalean/Panel/PO/PopulationCells.lean:129
mean_congr_on theorem — Cell means agree when the integrands agree pointwise on the cell. This is the workhorse "consistency descent" step: on a cell where an observed quantity equals a potential-outcome slice, their cell means coincide.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

f g :

Ω → ℝ

i :

ι

h :

∀ ω ∈ P.cell i, f ω = g ω

conclusion

P.mean f i = P.mean g i

Proof (Lean source)

theorem mean_congr_on (P : CellPartition μ ι) {f g : Ω → ℝ} (i : ι) (h : ∀ ω ∈ P.cell i, f ω = g ω) : P.mean f i = P.mean g i := eventCondExp_congr_on μ (P.cell_meas i) h

Causalean.Panel.PO.CellPartition.mean_congr_on · Causalean/Panel/PO/PopulationCells.lean:137
mean_congr_ae theorem — Cell means agree for a.e.-equal integrands.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

f g :

Ω → ℝ

i :

ι

h :

f =ᵐ[μ] g

conclusion

P.mean f i = P.mean g i

Proof (Lean source)

theorem mean_congr_ae (P : CellPartition μ ι) {f g : Ω → ℝ} (i : ι) (h : f =ᵐ[μ] g) : P.mean f i = P.mean g i := eventCondExp_congr_ae μ (P.cell i) (ae_restrict_of_ae h)

Causalean.Panel.PO.CellPartition.mean_congr_ae · Causalean/Panel/PO/PopulationCells.lean:145
mean_sub theorem — Cell means are additive over subtraction of integrable integrands.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

f g :

Ω → ℝ

i :

ι

hf :

IntegrableOn f (P.cell i) μ

hg :

IntegrableOn g (P.cell i) μ

conclusion

P.mean (f - g) i = P.mean f i - P.mean g i

Proof (Lean source)

theorem mean_sub (P : CellPartition μ ι) {f g : Ω → ℝ} (i : ι) (hf : IntegrableOn f (P.cell i) μ) (hg : IntegrableOn g (P.cell i) μ) : P.mean (f - g) i = P.mean f i - P.mean g i := eventCondExp_sub μ (P.cell i) hf hg

Causalean.Panel.PO.CellPartition.mean_sub · Causalean/Panel/PO/PopulationCells.lean:151
mean_add theorem — Cell means are additive over sums of integrable integrands.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

f g :

Ω → ℝ

i :

ι

hf :

IntegrableOn f (P.cell i) μ

hg :

IntegrableOn g (P.cell i) μ

conclusion

P.mean (f + g) i = P.mean f i + P.mean g i

Proof (Lean source)

theorem mean_add (P : CellPartition μ ι) {f g : Ω → ℝ} (i : ι) (hf : IntegrableOn f (P.cell i) μ) (hg : IntegrableOn g (P.cell i) μ) : P.mean (f + g) i = P.mean f i + P.mean g i := eventCondExp_add μ (P.cell i) hf hg

Causalean.Panel.PO.CellPartition.mean_add · Causalean/Panel/PO/PopulationCells.lean:157
mean_smul theorem — Cell means are homogeneous under real scalar multiplication.

hypotheses

Ω :

Type u_1
Measure Ω
shared

ι :

Type u_2
shared

P :

CellPartition μ ι

c :

ℝ

f :

Ω → ℝ

i :

ι

conclusion

P.mean (fun ω => c * f ω) i = c * P.mean f i

Proof (Lean source)

theorem mean_smul (P : CellPartition μ ι) (c : ℝ) (f : Ω → ℝ) (i : ι) : P.mean (fun ω => c * f ω) i = c * P.mean f i := eventCondExp_smul μ (P.cell i) c f

Causalean.Panel.PO.CellPartition.mean_smul · Causalean/Panel/PO/PopulationCells.lean:163

TreatmentPath 5 core · 2 supporting This file defines TreatmentPath, the assignment of an action to each unit-time pair, and the finite-memory history constructors used by the panel potential-outcomes layer. ★ History_zero

Treatment Paths and Finite-Memory Histories

This file defines TreatmentPath, the assignment of an action to each unit-time pair, and the finite-memory history constructors used by the panel potential-outcomes layer. History uses an explicit boundary treatment for lags before the observed panel starts, HistoryDefault uses the typeclass default boundary value, and BinaryHistory specializes to binary treatment with zero as the boundary value.

def TreatmentPath reviewed

Causalean.Panel

Given a set of units, a set of time periods, and a set of treatment actions, a treatment path assigns one treatment action to every unit-period pair.

Definition (Lean source)

parameters

I T A :

Type*

def

TreatmentPath I T A :

Type _

given by

I → T → A

Causalean.Panel.TreatmentPath · Causalean/Panel/PO/TreatmentPath.lean:25

def History reviewed

Causalean.Panel.TreatmentPath

Finite-memory history of length p+1 ending at time t, with the boundary convention "out-of-range = baseline" for an explicit baseline treatment value a0 : A. Lag k : Fin (p+1) returns D i ⟨t - k, _⟩ when k ≤ t.val, and a0 otherwise. Periods are indexed 0, …, T₀ - 1. In the binary case (A := Fin 2, baseline 0) this is H_{it}^{(p)} = (D_{it}, D_{i,t-1}, …, D_{i,t-p}) with the convention that treatment before the first period is 0; in one-based notation s = t.val + 1, this is D_{is} = 0 for s ∉ {1, …, T₀}.

Definition (Lean source)

parameters

I :

Type u_1

shared

A :

Type u_2

shared

T₀ :

ℕ

shared

a0 :

A

p :

ℕ

D :

TreatmentPath I (Fin T₀) A

i :

I

t :

Fin T₀

def

History a0 p D i t :

Fin (p + 1) → A

given by

fun k

=> if h : k.val ≤ t.val then D i ⟨t.val

- k.val, by have : t.val

- k.val ≤ t.val := sub_le _ _ exact lt_of_le_of_lt this t.isLt⟩ else a0

Causalean.Panel.TreatmentPath.History · Causalean/Panel/PO/TreatmentPath.lean:34 · uses TreatmentPath

def HistoryDefault reviewed

Causalean.Panel.TreatmentPath

Compatibility wrapper for code that deliberately wants the typeclass-provided default value as the finite-history boundary treatment.

Definition (Lean source)

parameters

I :

Type u_1

shared

A :

Type u_2

shared

T₀ :

ℕ

shared

Inhabited A

p :

ℕ

D :

TreatmentPath I (Fin T₀) A

i :

I

t :

Fin T₀

def

HistoryDefault p D i t :

Fin (p + 1) → A

given by

History (default : A) p D i t

Causalean.Panel.TreatmentPath.HistoryDefault · Causalean/Panel/PO/TreatmentPath.lean:52 · uses TreatmentPath

def BinaryHistory reviewed

Causalean.Panel.TreatmentPath

Binary finite-memory history with the conventional zero baseline.

Definition (Lean source)

parameters

I :

Type u_1

shared

T₀ :

ℕ

shared

p :

ℕ

D :

TreatmentPath I (Fin T₀) (Fin 2)

i :

I

t :

Fin T₀

def

BinaryHistory p D i t :

Fin (p + 1) → Fin 2

given by

History 0 p D i t

Causalean.Panel.TreatmentPath.BinaryHistory · Causalean/Panel/PO/TreatmentPath.lean:59 · uses TreatmentPath

lemma History_zero reviewed

Causalean.Panel.TreatmentPath

Lag 0 of the finite-memory treatment history equals the unit's contemporaneous treatment value.

Formal statement

hypotheses

I :

Type u_1

shared

A :

Type u_2

shared

T₀ :

ℕ

shared

a0 :

A

p :

ℕ

D :

TreatmentPath I (Fin T₀) A

i :

I

t :

Fin T₀

conclusion

History a0 p D i t 0 = D i t

Proof (Lean source)

@[simp] lemma History_zero (a0 : A) (p : ℕ) (D : TreatmentPath I (Fin T₀) A) (i : I) (t : Fin T₀) : History a0 p D i t 0 = D i t := by unfold History simp

Causalean.Panel.TreatmentPath.History_zero · Causalean/Panel/PO/TreatmentPath.lean:65 · uses TreatmentPath , History

2 supporting declarations (lemmas, instances)

HistoryDefault_zero lemma — Lag 0 of the default-boundary history is the contemporaneous treatment.

hypotheses

I :

Type u_1
shared

A :

Type u_2
shared

T₀ :

ℕ
shared

Inhabited A

p :

ℕ

D :

TreatmentPath I (Fin T₀) A

i :

I

t :

Fin T₀

conclusion

HistoryDefault p D i t 0 = D i t

Proof (Lean source)

@[simp] lemma HistoryDefault_zero [Inhabited A] (p : ℕ) (D : TreatmentPath I (Fin T₀) A) (i : I) (t : Fin T₀) : HistoryDefault p D i t 0 = D i t := by simp [HistoryDefault]

Causalean.Panel.TreatmentPath.HistoryDefault_zero · Causalean/Panel/PO/TreatmentPath.lean:73
BinaryHistory_zero lemma — Lag 0 of the binary zero-baseline history is the contemporaneous treatment.

hypotheses

I :

Type u_1
shared

T₀ :

ℕ
shared

p :

ℕ

D :

TreatmentPath I (Fin T₀) (Fin 2)

i :

I

t :

Fin T₀

conclusion

BinaryHistory p D i t 0 = D i t

Proof (Lean source)

@[simp] lemma BinaryHistory_zero (p : ℕ) (D : TreatmentPath I (Fin T₀) (Fin 2)) (i : I) (t : Fin T₀) : BinaryHistory p D i t 0 = D i t := by simp [BinaryHistory]

Causalean.Panel.TreatmentPath.BinaryHistory_zero · Causalean/Panel/PO/TreatmentPath.lean:79