Formalization: Forbidden Comparisons in Fixed-Effect Poisson Difference-in-Differences
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
Basic 62 declarations This file defines the deterministic triangular-array and collapsed cohort-time objects used by the paper.
PPML forbidden comparisons: finite collapsed worlds
This file defines the deterministic triangular-array and collapsed cohort-time
objects used by the paper. Calendar time is zero-indexed in Lean, so Lean
period 0 represents paper period 1. Adoption dates use the shared
WithTop (Fin T) convention, with ⊤ denoting never treated.
def Cohort
A cohort is an adoption date within the panel, with an additional never-treated cohort.
def Cell
A cell is a cohort-period pair in the panel.
def SupportedCell
Cohort-time cells restricted to the finite support C.
Definition (Lean source)
def PosReal
Strictly positive real numbers, used for primitive masses.
Definition (Lean source)
abbrev PosReal := {x : ℝ // 0 < x}
def OpenUnit
Limiting shares, whose carrier records the open-unit-interval restriction.
def CohortDummy
The index set of cohort dummies: the supported adoption cohorts other than the never-treated one. The never-treated cohort is the omitted category, absorbed by the intercept, so one cohort effect is carried by each remaining supported cohort.
Definition (Lean source)
def TimeDummy
The index set of time dummies: every calendar period other than the base period. Lean period zero is the paper's first period and is the omitted category, so one time effect is carried by each remaining period.
def CollapsedNuisanceIndex
Intercept, non-never-treated cohort effects, and non-base-period time effects.
Definition (Lean source)
abbrev CollapsedNuisanceIndex (T : ℕ) (C : Finset (Cohort T)) :=
Unit ⊕ (CohortDummy T C ⊕ TimeDummy T)
def CollapsedParameter
The treatment coordinate is stored last, as the second factor.
Definition (Lean source)
def UnitDummy
The index set of unit dummies: every unit other than the first, which is the omitted category absorbed by the intercept.
def PeriodIndex
Calendar indices use all Lean indices 0,...,T-1, representing paper periods 1,...,T.
Definition (Lean source)
abbrev PeriodIndex (T : ℕ) := Fin T
def UnitIndex
Unit indices use all Lean indices 0,...,N-1, representing paper units 1,...,N.
def UnitNuisanceIndex
Intercept, non-base unit effects, and non-base-period time effects: the coordinates of the nuisance block of a unit-and-time fixed-effect specification.
Definition (Lean source)
def UnitParameter
A full unit-and-time fixed-effect coefficient vector: the nuisance coordinates together with the single treatment coefficient, which is stored last as the second factor.
Definition (Lean source)
abbrev UnitParameter (N T : ℕ) := (UnitNuisanceIndex N T → ℝ) × ℝ
def ValidPanelHorizon
The paper only considers horizons in {4,5,...}.
Definition (Lean source)
def ValidPanelHorizon : Prop := 4 ≤ T
def ValidCohortSupport
Supported finite cohorts are paper dates 2,...,T, and never-treated is supported.
def treatmentIndicator
Whether adoption cohort g is treated in calendar period t.
Definition (Lean source)
def cohortCount
The finite-array cohort count induced by deterministic cohort labels.
Definition (Lean source)
def cohortCount {N : ℕ} (G : Fin N → Cohort T) (g : Cohort T) : ℕ :=
(Finset.univ.filter fun i => G i = g).card
def cohortIndexSet
The cohort index set induced by deterministic labels.
def limitingCellMass
The limiting cohort-time mass pi_g / T.
Definition (Lean source)
def finiteCellMass
The finite-array cohort-time mass n_gN / (N*T).
Definition (Lean source)
noncomputable def finiteCellMass {N : ℕ} (G : Fin N → Cohort T) (g : Cohort T) : ℝ :=
(cohortCount T G g : ℝ) / (N * T)
def withinCohortBaseline
The within-cohort average of the positive unit baseline masses.
Definition (Lean source)
noncomputable def withinCohortBaseline {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (g : Cohort T) : ℝ :=
(cohortCount T G g : ℝ)⁻¹ * ∑ i ∈ cohortIndexSet T G g, (b i : ℝ)
theorem withinCohortBaseline_pos
On its declared positive-count domain, the within-cohort baseline is strictly positive.
Formal statement
hypotheses
conclusion
0 < withinCohortBaseline T G b g
Proof (Lean source)
lemma withinCohortBaseline_pos {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (g : Cohort T) (hCount : 0 < cohortCount T G g) :
0 < withinCohortBaseline T G b g := by
unfold withinCohortBaseline
apply mul_pos (inv_pos.mpr (Nat.cast_pos.mpr hCount))
apply Finset.sum_pos'
· intro i _
exact (b i).property.le
· rw [cohortCount] at hCount
obtain ⟨i, hi⟩ := Finset.card_pos.mp hCount
exact ⟨i, by simpa [cohortIndexSet] using hi, (b i).property⟩
def finiteUntreatedMean
The finite-array untreated cohort mean.
Definition (Lean source)
noncomputable def finiteUntreatedMean {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (g : Cohort T) (t : Fin T) : ℝ :=
withinCohortBaseline T G b g * exp (gamma t)
theorem finiteUntreatedMean_pos
A supported positive-count cohort has a strictly positive finite untreated mean.
Formal statement
hypotheses
conclusion
0 < finiteUntreatedMean T G b gamma g t
Proof (Lean source)
lemma finiteUntreatedMean_pos {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (g : Cohort T) (t : Fin T)
(hCount : 0 < cohortCount T G g) :
0 < finiteUntreatedMean T G b gamma g t := by
exact mul_pos (withinCohortBaseline_pos T G b g hCount) (Real.exp_pos _)
def untreatedMean
The limiting untreated cohort mean.
def finiteObservedCohortMean
The finite-array observed cohort mean.
Definition (Lean source)
noncomputable def finiteObservedCohortMean {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (t : Fin T) : ℝ :=
finiteUntreatedMean T G b gamma g t *
exp (treatmentIndicator T g t * delta (g, t))
theorem finiteObservedCohortMean_pos
A supported positive-count cohort has a strictly positive finite observed mean.
Formal statement
hypotheses
conclusion
0 < finiteObservedCohortMean T G b gamma delta g t
Proof (Lean source)
lemma finiteObservedCohortMean_pos {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (t : Fin T) (hCount : 0 < cohortCount T G g) :
0 < finiteObservedCohortMean T G b gamma delta g t := by
exact mul_pos (finiteUntreatedMean_pos T G b gamma g t hCount) (Real.exp_pos _)
def observedCohortMean
The limiting observed cohort mean.
Definition (Lean source)
noncomputable def observedCohortMean (barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta : Cell T → ℝ) (g : Cohort T) (t : Fin T) : ℝ :=
untreatedMean T barB gamma g t * exp (treatmentIndicator T g t * delta (g, t))
def collapsedNuisanceRegressor
The fixed-effect nuisance part of the collapsed regressor.
Definition (Lean source)
noncomputable def collapsedNuisanceRegressor (g : Cohort T) (t : Fin T) :
CollapsedNuisanceIndex T C → ℝ
| inl _ => 1
| inr (inl c) => if g = c.1.1 then 1 else 0
| inr (inr u) => if t = u.1 then 1 else 0
def collapsedRegressor
The collapsed regressor, with treatment as its final coordinate.
Definition (Lean source)
noncomputable def collapsedRegressor (g : Cohort T) (t : Fin T) :
CollapsedParameter T C :=
(collapsedNuisanceRegressor T C g t, treatmentIndicator T g t)
def collapsedIndex
Dot product for collapsed parameters.
Definition (Lean source)
def collapsedIndex (r theta : CollapsedParameter T C) : ℝ :=
(∑ j, r.1 j * theta.1 j) + r.2 * theta.2
def limitingCriterion
The limiting collapsed Poisson pseudo-criterion.
Definition (Lean source)
noncomputable def limitingCriterion (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(theta : CollapsedParameter T C) : ℝ :=
∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(observedCohortMean T barB gamma delta g t *
collapsedIndex T C (collapsedRegressor T C g t) theta -
exp (collapsedIndex T C (collapsedRegressor T C g t) theta))
def finiteCollapsedCriterion
The finite-array collapsed Poisson pseudo-criterion.
Definition (Lean source)
noncomputable def finiteCollapsedCriterion {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(theta : CollapsedParameter T C) : ℝ :=
∑ g ∈ C, ∑ t : Fin T,
finiteCellMass T G g *
(finiteObservedCohortMean T G b gamma delta g t *
collapsedIndex T C (collapsedRegressor T C g t) theta -
exp (collapsedIndex T C (collapsedRegressor T C g t) theta))
The selected maximizer theta_star(delta) of the limiting collapsed criterion.
Definition (Lean source)
noncomputable def collapsedPopulationProjection (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
CollapsedParameter T C :=
maximizerOrZero (limitingCriterion T C pi barB gamma delta)
def betaStar
The treatment coordinate of the limiting pseudo-true parameter.
def fittedMean
The fitted limiting cohort-time mean.
Definition (Lean source)
noncomputable def fittedMean (pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) (g : Cohort T) (t : Fin T) : ℝ :=
exp (collapsedIndex T C (collapsedRegressor T C g t)
(collapsedPopulationProjection T C pi barB gamma delta))
def SamplingLaw
An abstract sampling law on an outcome sample space, represented by the expectation functional it induces on real-valued functions of that space. Nothing beyond expectations of the outcome array is ever used, so the law is carried by this functional rather than by a probability measure.
Definition (Lean source)
abbrev SamplingLaw (Omega : Type*) := (Omega → ℝ) → ℝ
def expectationUnder
The expectation operator carried by the abstract sampling law.
Definition (Lean source)
def expectationUnder {Omega : Type*} (P : SamplingLaw Omega) : (Omega → ℝ) → ℝ := P
def unitTreatment
The unit treatment indicator induced by its cohort label.
Definition (Lean source)
noncomputable def unitTreatment (G : Fin N → Cohort T) (i : Fin N) (t : Fin T) : ℝ :=
treatmentIndicator T (G i) t
def unitNuisanceRegressor
Unit-and-time fixed-effect nuisance regressor.
Definition (Lean source)
noncomputable def unitNuisanceRegressor (i : Fin N) (t : Fin T) :
UnitNuisanceIndex N T → ℝ
| inl _ => 1
| inr (inl j) => if i = j.1 then 1 else 0
| inr (inr u) => if t = u.1 then 1 else 0
def unitRegressor
The unit-and-time regressor with treatment last.
Definition (Lean source)
noncomputable def unitRegressor (G : Fin N → Cohort T) (i : Fin N) (t : Fin T) :
UnitParameter N T :=
(unitNuisanceRegressor T N i t, unitTreatment T N G i t)
def unitIndex
Dot product for finite-array unit parameters.
Definition (Lean source)
def unitIndex (v theta : UnitParameter N T) : ℝ :=
(∑ j, v.1 j * theta.1 j) + v.2 * theta.2
def unitObservedMean
The deterministic unit-time mean implied by the exponential model.
def unitCriterion
The unit-and-time-FE population Poisson criterion.
Definition (Lean source)
noncomputable def unitCriterion (G : Fin N → Cohort T) (b : Fin N → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) (theta : UnitParameter N T) : ℝ :=
((N * T : ℕ) : ℝ)⁻¹ * ∑ i : Fin N, ∑ t : Fin T,
(unitObservedMean T N G b gamma delta i t *
unitIndex T N (unitRegressor T N G i t) theta -
exp (unitIndex T N (unitRegressor T N G i t) theta))
The last coordinate of the selected unit-FE population maximizer.
Definition (Lean source)
noncomputable def betaNStar (G : Fin N → Cohort T) (b : Fin N → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) : ℝ :=
(maximizerOrZero (unitCriterion T N G b gamma delta)).2
def extendedExp
Option ℝ realizes finite unit effects together with none = -∞.
def ExtendedCandidate
A candidate for the unit fixed-effect Poisson fit in which unit effects may take the value minus infinity: one extended unit effect per unit (the absent value standing for minus infinity), together with finite time effects and a finite treatment coefficient. Admitting minus infinity is what makes the maximum attained for units whose entire outcome path is zero.
Definition (Lean source)
def sampleCriterion
Extended unit-FE sample objective with finite time and treatment coordinates.
Definition (Lean source)
noncomputable def sampleCriterion (G : Fin N → Cohort T) (Y : Fin N → Fin T → ℝ)
(p : ExtendedCandidate N T) : ℝ :=
∑ i : Fin N, ∑ t : Fin T,
let etaFinite := p.2.1 t + p.2.2 * unitTreatment T N G i t
match p.1 i with
| none => 0
| some unitEffect =>
Y i t * (unitEffect + etaFinite) - exp unitEffect * exp etaFinite
def ExtendedCandidateAdmissible
A -∞ unit effect is admissible only for a unit whose whole outcome path is zero.
Definition (Lean source)
def ExtendedCandidateAdmissible (Y : Fin N → Fin T → ℝ) (p : ExtendedCandidate N T) : Prop :=
(∀ t : Fin T, t.val = 0 → p.2.1 t = 0) ∧
∀ i : Fin N, p.1 i = none → ∀ t : Fin T, Y i t = 0
def IsExtendedSampleMaximizer
Normalized maximizers of the extended sample objective.
Definition (Lean source)
def IsExtendedSampleMaximizer (G : Fin N → Cohort T) (Y : Fin N → Fin T → ℝ)
(p : ExtendedCandidate N T) : Prop :=
ExtendedCandidateAdmissible T N Y p ∧
∀ q : ExtendedCandidate N T,
ExtendedCandidateAdmissible T N Y q →
sampleCriterion T N G Y q ≤ sampleCriterion T N G Y p
def finiteCoordinateNormSq
Squared norm of the finite time-effect and treatment coordinates.
Definition (Lean source)
def finiteCoordinateNormSq (p : ExtendedCandidate N T) : ℝ :=
(∑ t, (p.2.1 t) ^ 2) + p.2.2 ^ 2
The total extended-MLE coefficient, with the stipulated minimum-norm selection and zero fallback.
Definition (Lean source)
noncomputable def hatBetaN (G : Fin N → Cohort T) (Y : Fin N → Fin T → ℝ) : ℝ :=
by
classical
exact if h : ∃ p : ExtendedCandidate N T,
IsExtendedSampleMaximizer T N G Y p ∧
∀ q, IsExtendedSampleMaximizer T N G Y q →
finiteCoordinateNormSq T N p ≤ finiteCoordinateNormSq T N q
then (choose h).2.2 else 0
Untreated potential-outcome means factor into a positive unit baseline and a common calendar-time exponential component; the treatment-zero outcome equals that untreated outcome.
Definition (Lean source)
def UnitUntreatedExponentialMean (Omega : ℕ → Type*)
(P : ∀ N, SamplingLaw (Omega N))
(Y : ∀ N, Fin N → Fin T → Fin 2 → Omega N → ℝ)
(b : ∀ N, Fin N → PosReal) (gamma : Fin T → ℝ) : Prop :=
(∀ N i t, expectationUnder (P N) (Y N i t 0) = (b N i : ℝ) * exp (gamma t)) ∧
∀ t : Fin T, t.val = 0 → gamma t = 0
Within each supported cohort, the average unit baseline converges to a strictly positive cohort-specific limiting baseline.
In every treated unit-period, the mean treated outcome equals the mean untreated outcome multiplied by that cell's exponential treatment effect.
Definition (Lean source)
def ProportionalEffects (Omega : ℕ → Type*) (P : ∀ N, SamplingLaw (Omega N))
(Y : ∀ N, Fin N → Fin T → Fin 2 → Omega N → ℝ)
(G : ∀ N, Fin N → Cohort T) (delta : Cell T → ℝ) : Prop :=
∀ N i t, unitTreatment T N (G N) i t = 1 →
expectationUnder (P N) (Y N i t 1) =
expectationUnder (P N) (Y N i t 0) * exp (delta (G N i, t))
The collapsed fixed-effects and treatment design has full rank under the limiting cell masses.
Definition (Lean source)
def CollapsedDesignRank (pi : Cohort T → OpenUnit) : Prop :=
∀ a : CollapsedParameter T C, a ≠ 0 →
0 < ∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g * (collapsedIndex T C (collapsedRegressor T C g t) a) ^ 2
The support contains adoption cohorts 1, 2, and 3, as well as the never-treated cohort.
Every treated cohort-period has a strictly positive log treatment effect.
Definition (Lean source)
def StrictPositiveEffects (delta : Cell T → ℝ) : Prop :=
∀ g ∈ C, ∀ t : Fin T, treatmentIndicator T g t = 1 → 0 < delta (g, t)
Collapse 2 declarations Exact unit-FE collapse and convergence to the limiting collapsed projection.
Exact unit-FE collapse and convergence to the limiting collapsed projection.
def finiteCollapsedProjection
The selected maximizer of the finite collapsed criterion.
Definition (Lean source)
noncomputable def finiteCollapsedProjection (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal) (gamma : Fin T → ℝ)
(delta : Cell T → ℝ) : CollapsedParameter T C :=
maximizerOrZero (finiteCollapsedCriterion T C G b gamma delta)
The unit-FE and collapsed criteria have the same beta, and these betas converge.
Formal statement
hypotheses
T :
ℕ
hHorizon :
@realizes T(standing 4 ≤ T premise)
hSupport :
@realizes C(paper cohort-support premise)
Omega :
ℕ → Type*
P :
∀ N, SamplingLaw (Omega N)
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hGSupport :
∀ N i, G N i ∈ C
@realizes G_i(every deterministic label lies in C)
hShare :
CohortShareLimit T C G pi
hMean :
UnitUntreatedExponentialMean T Omega P Y b gamma
hBaseline :
WithinCohortBaselineLimit T C G b barB
hEffects :
ProportionalEffects T Omega P Y G delta
hRank :
CollapsedDesignRank T C pi
conclusion
(∀ N, C.card ≤ N → IsUniqueGlobalMax (unitCriterion T N (G N) (b N) gamma delta) (maximizerOrZero (unitCriterion T N (G N) (b N) gamma delta)) ∧ IsUniqueGlobalMax (finiteCollapsedCriterion T C (G N) (b N) gamma delta) (finiteCollapsedProjection T C (G N) (b N) gamma delta) ∧ betaNStar T N (G N) (b N) gamma delta = (finiteCollapsedProjection T C (G N) (b N) gamma delta).2) ∧
Tendsto (fun N => betaNStar T N (G N) (b N) gamma delta) atTop (nhds (betaStar T C pi barB gamma delta)) ∧
C.card
≤ N → (∀ g ∈ C, withinCohortBaseline T (G N) b' g = withinCohortBaseline T (G N) (b N) g) → betaNStar T N (G N) b' gamma delta = betaNStar T N (G N) (b N) gamma delta
Proof (Lean source)
lemma unit_fe_collapse (T : ℕ) (C : Finset (Cohort T))
(hHorizon : ValidPanelHorizon T) -- @realizes T(standing 4 ≤ T premise)
(hSupport : ValidCohortSupport T C) -- @realizes C(paper cohort-support premise)
(Omega : ℕ → Type*) (P : ∀ N, SamplingLaw (Omega N))
(Y : ∀ N, Fin N → Fin T → Fin 2 → Omega N → ℝ)
(G : ∀ N, Fin N → Cohort T) (b : ∀ N, Fin N → PosReal)
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(hGSupport : ∀ N i, G N i ∈ C) -- @realizes G_i(every deterministic label lies in C)
(hShare : CohortShareLimit T C G pi)
(hMean : UnitUntreatedExponentialMean T Omega P Y b gamma)
(hBaseline : WithinCohortBaselineLimit T C G b barB)
(hEffects : ProportionalEffects T Omega P Y G delta)
(hRank : CollapsedDesignRank T C pi) :
(∀ N, C.card ≤ N →
IsUniqueGlobalMax (unitCriterion T N (G N) (b N) gamma delta)
(maximizerOrZero (unitCriterion T N (G N) (b N) gamma delta)) ∧
IsUniqueGlobalMax (finiteCollapsedCriterion T C (G N) (b N) gamma delta)
(finiteCollapsedProjection T C (G N) (b N) gamma delta) ∧
betaNStar T N (G N) (b N) gamma delta =
(finiteCollapsedProjection T C (G N) (b N) gamma delta).2) ∧
Tendsto (fun N => betaNStar T N (G N) (b N) gamma delta) atTop
(nhds (betaStar T C pi barB gamma delta)) ∧
∀ N (b' : Fin N → PosReal), C.card ≤ N →
(∀ g ∈ C, withinCohortBaseline T (G N) b' g =
withinCohortBaseline T (G N) (b N) g) →
betaNStar T N (G N) b' gamma delta = betaNStar T N (G N) (b N) gamma delta := by
classical
have hT : 0 < T := lt_of_lt_of_le (by norm_num) hHorizon
have hC : C.Nonempty := ⟨⊤, hSupport.1⟩
have hfinite : ∀ N, C.card ≤ N →
IsUniqueGlobalMax (unitCriterion T N (G N) (b N) gamma delta)
(maximizerOrZero (unitCriterion T N (G N) (b N) gamma delta)) ∧
IsUniqueGlobalMax (finiteCollapsedCriterion T C (G N) (b N) gamma delta)
(finiteCollapsedProjection T C (G N) (b N) gamma delta) ∧
betaNStar T N (G N) (b N) gamma delta =
(finiteCollapsedProjection T C (G N) (b N) gamma delta).2 := by
intro N hcard
have harray := hShare.1 N hcard
simpa [finiteCollapsedProjection, betaNStar] using
finite_unit_and_collapsed_unique_beta T C (G N) (b N) gamma delta pi
harray.1 hT hC hSupport.1 (hGSupport N) harray.2 hRank
refine ⟨hfinite, ?_, ?_⟩
· have hcollapsed := selectedFiniteCollapsed_tendsto T C G b pi barB gamma delta
hHorizon hSupport hShare hBaseline hRank
have hcollapsedBeta : Tendsto
(fun N => (finiteCollapsedProjection T C (G N) (b N) gamma delta).2)
atTop (nhds (betaStar T C pi barB gamma delta)) := by
exact (continuous_snd.tendsto
(collapsedPopulationProjection T C pi barB gamma delta)).comp hcollapsed
apply hcollapsedBeta.congr'
filter_upwards [Filter.eventually_ge_atTop C.card] with N hcard
exact (hfinite N hcard).2.2.symm
· intro N b' hcard hmeans
have harray := hShare.1 N hcard
have hcrit : finiteCollapsedCriterion T C (G N) b' gamma delta =
finiteCollapsedCriterion T C (G N) (b N) gamma delta := by
funext theta
unfold finiteCollapsedCriterion
apply Finset.sum_congr rfl
intro g hg
apply Finset.sum_congr rfl
intro t ht
rw [show finiteObservedCohortMean T (G N) b' gamma delta g t =
finiteObservedCohortMean T (G N) (b N) gamma delta g t by
simp only [finiteObservedCohortMean, finiteUntreatedMean, hmeans g hg]]
have hselected :
maximizerOrZero (finiteCollapsedCriterion T C (G N) b' gamma delta) =
maximizerOrZero (finiteCollapsedCriterion T C (G N) (b N) gamma delta) :=
congrArg maximizerOrZero hcrit
have hb' := finite_unit_and_collapsed_unique_beta T C (G N) b' gamma delta pi
harray.1 hT hC hSupport.1 (hGSupport N) harray.2 hRank
have hb := finite_unit_and_collapsed_unique_beta T C (G N) (b N) gamma delta pi
harray.1 hT hC hSupport.1 (hGSupport N) harray.2 hRank
unfold betaNStar
calc
(maximizerOrZero (unitCriterion T N (G N) b' gamma delta)).2 =
(maximizerOrZero (finiteCollapsedCriterion T C (G N) b' gamma delta)).2 :=
hb'.2.2
_ = (maximizerOrZero
(finiteCollapsedCriterion T C (G N) (b N) gamma delta)).2 := by rw [hselected]
_ = (maximizerOrZero (unitCriterion T N (G N) (b N) gamma delta)).2 :=
hb.2.2.symm
ForbiddenSign 3 declarations Sharp effect-derivative and forbidden-cell sign characterization.
Sharp effect-derivative and forbidden-cell sign characterization.
def fwlEnergy
The positive residual-energy denominator in the PPML derivative formula.
Definition (Lean source)
noncomputable def fwlEnergy (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) : ℝ :=
∑ z : SupportedCell T C,
limitingCellMass T pi z.1.1 * fittedMean T C pi barB gamma delta z.1.1 z.2 *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2
theorem fwlEnergy_pos_of_collapsedDesignRank
Full collapsed rank forces the residualized treatment regressor to have strictly positive fitted-mean-weighted energy.
Formal statement
Proof (Lean source)
lemma fwlEnergy_pos_of_collapsedDesignRank (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(hRank : CollapsedDesignRank T C pi) :
0 < fwlEnergy T C hT hC pi barB gamma delta := by
classical
let W := weightedFWLResidual T C hT hC pi barB gamma delta
let rho := rhoStar T C hT hC pi barB gamma delta
let a : CollapsedParameter T C := (fun j => -rho j, 1)
have ha : a ≠ 0 := by
intro ha0
have := congrArg snd ha0
norm_num [a] at this
have hnonneg : 0 ≤ fwlEnergy T C hT hC pi barB gamma delta := by
unfold fwlEnergy
exact sum_nonneg fun z _ =>
mul_nonneg
(mul_nonneg (le_of_lt (div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)))
(le_of_lt (Real.exp_pos _)))
(sq_nonneg _)
by_contra hnpos
have henergy : fwlEnergy T C hT hC pi barB gamma delta = 0 :=
le_antisymm (le_of_not_gt hnpos) hnonneg
have hW (z : SupportedCell T C) : W z = 0 := by
have hterm :
limitingCellMass T pi z.1.1 *
fittedMean T C pi barB gamma delta z.1.1 z.2 * (W z) ^ 2 ≤
fwlEnergy T C hT hC pi barB gamma delta := by
unfold fwlEnergy
change _ * (W z) ^ 2 ≤ ∑ y, _ * (W y) ^ 2
let f : SupportedCell T C → ℝ := fun y =>
limitingCellMass T pi y.1.1 *
fittedMean T C pi barB gamma delta y.1.1 y.2 * (W y) ^ 2
have hs := Finset.single_le_sum (s := univ) (f := f)
(fun y _ => mul_nonneg
(mul_nonneg (le_of_lt (div_pos (pi y.1.1).property.1 (by exact_mod_cast hT)))
(le_of_lt (Real.exp_pos _)))
(sq_nonneg _)) (Finset.mem_univ z)
simpa [f] using hs
rw [henergy] at hterm
have hweight : 0 < limitingCellMass T pi z.1.1 *
fittedMean T C pi barB gamma delta z.1.1 z.2 :=
mul_pos (div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)) (Real.exp_pos _)
have hsquare : (W z) ^ 2 = 0 := by
apply le_antisymm
· by_contra hs
have hp := mul_pos hweight (lt_of_not_ge hs)
exact (not_lt_of_ge hterm) hp
· exact sq_nonneg _
exact sq_eq_zero_iff.mp hsquare
have hindex (z : SupportedCell T C) :
collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) a = W z := by
rw [show W z = weightedFWLResidual T C hT hC pi barB gamma delta z by rfl]
rw [weightedFWLResidual_eq_rhoStar T C hT hC pi barB gamma delta
z.1.1 z.1.2 z.2]
simp only [collapsedIndex, collapsedRegressor, a, rho, mul_one]
simp_rw [mul_neg]
rw [Finset.sum_neg_distrib]
ring
have hrank := hRank a ha
have hzero :
(∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) a) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
rw [hindex (⟨g, hg⟩, t), hW (⟨g, hg⟩, t)]
simp
rw [hzero] at hrank
exact (lt_irrefl 0) hrank
A treated effect moves beta with exactly the sign of its pseudo-true weighted FWL residual.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
k :
Cohort T
hk :
k ∈ C
s :
Fin T
hks :
treatmentIndicator T k s = 1
hRank :
CollapsedDesignRank T C pi
conclusion
let W := weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) let denominator := fwlEnergy T C hT hC pi barB gamma delta let derivative := limitingCellMass T pi k * untreatedMean T barB gamma k s * exp (delta (k, s)) * W / denominator HasDerivAt (fun x => betaStar T C pi barB gamma (update delta (k, s) x)) derivative (delta (k, s)) ∧
0 < denominator ∧
(derivative < 0 ↔ W < 0) ∧
(derivative = 0 ↔ W = 0) ∧
(0 < derivative ↔ 0 < W)
Proof (Lean source)
theorem sharp_ppml_forbidden_sign (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(k : Cohort T) (hk : k ∈ C) (s : Fin T) (hks : treatmentIndicator T k s = 1)
(hRank : CollapsedDesignRank T C pi) :
let W := weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s)
let denominator := fwlEnergy T C hT hC pi barB gamma delta
let derivative := limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) * W / denominator
HasDerivAt
(fun x => betaStar T C pi barB gamma (update delta (k, s) x))
derivative (delta (k, s)) ∧
0 < denominator ∧
(derivative < 0 ↔ W < 0) ∧
(derivative = 0 ↔ W = 0) ∧
(0 < derivative ↔ 0 < W) := by
dsimp only
have hdenominator := fwlEnergy_pos_of_collapsedDesignRank
T C hT hC pi barB gamma delta hRank
have hmass : 0 < limitingCellMass T pi k :=
div_pos (pi k).property.1 (by exact_mod_cast hT)
have hbaseline : 0 < untreatedMean T barB gamma k s := by
exact mul_pos (barB k).property (Real.exp_pos _)
have hprefactor : 0 < limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) / fwlEnergy T C hT hC pi barB gamma delta :=
div_pos (mul_pos (mul_pos hmass hbaseline) (Real.exp_pos _)) hdenominator
refine ⟨?_, hdenominator, ?_, ?_, ?_⟩
· have henergy : 0 < ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2 := by
simpa [fwlEnergy, meanFWLWeight] using hdenominator
simpa [fwlEnergy, meanFWLWeight] using
betaStar_update_hasDerivAt T C hT hC pi barB gamma delta k hk s hks hRank henergy
· rw [show limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) /
fwlEnergy T C hT hC pi barB gamma delta =
(limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) / fwlEnergy T C hT hC pi barB gamma delta) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) by ring]
constructor
· intro hneg
by_contra hW
exact (not_lt_of_ge (mul_nonneg hprefactor.le (le_of_not_gt hW))) hneg
· exact mul_neg_of_pos_of_neg hprefactor
· rw [show limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) /
fwlEnergy T C hT hC pi barB gamma delta =
(limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) / fwlEnergy T C hT hC pi barB gamma delta) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) by ring]
exact mul_eq_zero_iff_left (ne_of_gt hprefactor)
· rw [show limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) /
fwlEnergy T C hT hC pi barB gamma delta =
(limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) / fwlEnergy T C hT hC pi barB gamma delta) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) by ring]
exact (mul_pos_iff_of_pos_left hprefactor)
FourCohort 32 declarations The explicit four-cohort sign-reversal fixture and its local diagnostic.
The explicit four-cohort sign-reversal fixture and its local diagnostic.
def fourResidualNumerator
The numerator matrix of the no-effect two-way residual table.
Definition (Lean source)
def fourResidualNumerator (g : Cohort 4) (t : Fin 4) : ℝ :=
if g = ((⟨1, by decide⟩ : Fin 4) : Cohort 4) then
if t.val = 0 then -3 else if t.val = 1 then 3 else if t.val = 2 then 1 else -1
else if g = ((⟨2, by decide⟩ : Fin 4) : Cohort 4) then
if t.val = 0 then -1 else if t.val = 1 then -3 else if t.val = 2 then 3 else 1
else if g = ((⟨3, by decide⟩ : Fin 4) : Cohort 4) then
if t.val = 0 then 1 else if t.val = 1 then -1 else if t.val = 2 then -3 else 3
else
if t.val = 0 then 3 else if t.val = 1 then 1 else if t.val = 2 then -1 else -3
def fourResidualTable
The exact no-effect residual table displayed in the paper.
Definition (Lean source)
def zeroEffects4
The homogeneous no-effect vector used only for the derivative diagnostic.
Definition (Lean source)
def zeroEffects4 (_z : Cell 4) : ℝ := 0
def fourHorizonPositive
The counterexample's four-period horizon is positive. It is supplied as the positivity side condition wherever the fixture instantiates a result stated for a general panel horizon.
Definition (Lean source)
def fourHorizonPositive : 0 < 4 := by decide
def fourSupportNonempty
The counterexample's cohort support is nonempty: it contains the never-treated cohort.
Definition (Lean source)
def fourSupportNonempty : fourCohortSupport.Nonempty :=
⟨⊤, by simp [fourCohortSupport]⟩
def fourLateCohort
The cohort that carries the exceptional effect in the counterexample: the units adopting at Lean date one, which is the paper's adoption date two.
def fourLatePeriod
The period in which the counterexample's exceptional effect occurs: Lean period three, which is the paper's period four and the last period of the panel.
Definition (Lean source)
def fourLatePeriod : Fin 4 := ⟨3, by decide⟩
def fourLateSupportedCell
The supported cohort-time cell at which the counterexample places its exceptionally large treatment effect: the paper's adoption cohort two, observed in the paper's period four.
Definition (Lean source)
noncomputable def fourLateSupportedCell : SupportedCell 4 fourCohortSupport :=
(⟨fourLateCohort, by simp [fourLateCohort, fourCohortSupport]⟩, fourLatePeriod)
theorem fourCohortCollapsedDesignRank
The counterexample's collapsed design has full rank: no nonzero coefficient direction produces a zero linear index at every supported cohort-time cell, so the cell-mass-weighted sum of squared indices is strictly positive away from the origin.
Formal statement
conclusion
Proof (Lean source)
lemma fourCohortCollapsedDesignRank :
CollapsedDesignRank 4 fourCohortSupport fourCohortShare := by
intro a ha
have hnonneg (g : Cohort 4) (t : Fin 4) :
0 ≤ limitingCellMass 4 fourCohortShare g *
(collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport g t) a) ^ 2 :=
mul_nonneg (by
simp only [limitingCellMass, fourCohortShare]
positivity) (sq_nonneg _)
by_contra hpos
have hsum :
(∑ g ∈ fourCohortSupport, ∑ t : Fin 4,
limitingCellMass 4 fourCohortShare g *
(collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport g t) a) ^ 2) = 0 := by
apply le_antisymm (le_of_not_gt hpos)
exact sum_nonneg fun g _ => sum_nonneg fun t _ => hnonneg g t
have hindex (g : Cohort 4) (hg : g ∈ fourCohortSupport) (t : Fin 4) :
collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport g t) a = 0 := by
have hgzero := (Finset.sum_eq_zero_iff_of_nonneg
(fun g hg => sum_nonneg fun t _ => hnonneg g t)).mp hsum g hg
have htzero := (Finset.sum_eq_zero_iff_of_nonneg
(fun t _ => hnonneg g t)).mp hgzero t (Finset.mem_univ t)
have hmass : limitingCellMass 4 fourCohortShare g ≠ 0 := by
norm_num [limitingCellMass, fourCohortShare]
exact sq_eq_zero_iff.mp ((mul_eq_zero.mp htzero).resolve_left hmass)
have hzero : a = 0 := by
rcases a with ⟨u, beta⟩
have htop (n : Fin 4) := hindex (⊤ : Cohort 4)
(by simp [fourCohortSupport]) n
have hc1 (n : Fin 4) := hindex fourLateCohort
(by simp [fourLateCohort, fourCohortSupport]) n
have hc2 (n : Fin 4) := hindex
((⟨2, by decide⟩ : Fin 4) : Cohort 4)
(by simp [fourCohortSupport]) n
have hc3 (n : Fin 4) := hindex
((⟨3, by decide⟩ : Fin 4) : Cohort 4)
(by simp [fourCohortSupport]) n
have hcohortTop : (∑ x : CohortDummy 4 fourCohortSupport,
if (⊤ : Cohort 4) = x.1.1 then u (inr (inl x)) else 0) = 0 := by
apply Fintype.sum_eq_zero
intro x
rw [if_neg]
exact x.2 ∘ Eq.symm
have htimeZero : (∑ x : TimeDummy 4,
if (⟨0, by decide⟩ : Fin 4) = x.1 then u (inr (inr x)) else 0) = 0 := by
apply Fintype.sum_eq_zero
intro x
rw [if_neg]
intro h
exact x.2 (by simpa [← h])
have hcohort (x : CohortDummy 4 fourCohortSupport) :
(∑ y : CohortDummy 4 fourCohortSupport,
if x.1.1 = y.1.1 then u (inr (inl y)) else 0) =
u (inr (inl x)) := by
rw [Fintype.sum_eq_single x]
· simp
· intro y hy
rw [if_neg]
intro h
exact hy (Subtype.ext (Subtype.ext h.symm))
have htime (x : TimeDummy 4) :
(∑ y : TimeDummy 4,
if x.1 = y.1 then u (inr (inr y)) else 0) =
u (inr (inr x)) := by
rw [Fintype.sum_eq_single x]
· simp
· intro y hy
rw [if_neg]
intro h
exact hy (Subtype.ext h.symm)
have hintercept : u (inl ()) = 0 := by
have hx := htop (⟨0, by decide⟩ : Fin 4)
simp only [collapsedIndex, collapsedRegressor, collapsedNuisanceRegressor,
Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton, one_mul] at hx
simp only [ite_mul, one_mul, zero_mul] at hx
rw [hcohortTop, htimeZero] at hx
norm_num [treatmentIndicator,
absorbingTreatment_eq] at hx
exact hx
have hcohortZero (x : CohortDummy 4 fourCohortSupport) :
u (inr (inl x)) = 0 := by
have hxmem := x.1.2
simp only [fourCohortSupport, Finset.mem_insert, mem_singleton] at hxmem
rcases hxmem with h | h | h | h
· have heq : x.1.1 = fourLateCohort := by simpa [fourLateCohort] using h
have hx := hindex x.1.1 x.1.2 (⟨0, by decide⟩ : Fin 4)
simp only [collapsedIndex, collapsedRegressor, collapsedNuisanceRegressor,
Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton, one_mul] at hx
simp only [ite_mul, one_mul, zero_mul] at hx
rw [hcohort x, htimeZero, hintercept] at hx
have huntreated : treatmentIndicator 4 x.1.1 (⟨0, by decide⟩ : Fin 4) = 0 := by
rw [heq]
rw [treatmentIndicator, absorbingTreatment_eq,
if_neg (by
apply not_le.mpr
change ((⟨0, by decide⟩ : Fin 4) : WithTop (Fin 4)) <
((⟨1, by decide⟩ : Fin 4) : WithTop (Fin 4))
exact WithTop.coe_lt_coe.mpr (by decide))]
rw [huntreated] at hx
norm_num at hx ⊢
exact hx
· have hx := hindex x.1.1 x.1.2 (⟨0, by decide⟩ : Fin 4)
simp only [collapsedIndex, collapsedRegressor, collapsedNuisanceRegressor,
Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton, one_mul] at hx
simp only [ite_mul, one_mul, zero_mul] at hx
rw [hcohort x, htimeZero, hintercept] at hx
norm_num [h, treatmentIndicator,
absorbingTreatment_eq] at hx
exact hx
· have hx := hindex x.1.1 x.1.2 (⟨0, by decide⟩ : Fin 4)
simp only [collapsedIndex, collapsedRegressor, collapsedNuisanceRegressor,
Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton, one_mul] at hx
simp only [ite_mul, one_mul, zero_mul] at hx
rw [hcohort x, htimeZero, hintercept] at hx
norm_num [h, treatmentIndicator,
absorbingTreatment_eq] at hx
exact hx
· exact (x.2 h).elim
have htimeZero' (x : TimeDummy 4) : u (inr (inr x)) = 0 := by
have hx := htop x.1
simp only [collapsedIndex, collapsedRegressor, collapsedNuisanceRegressor,
Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton, one_mul] at hx
simp only [ite_mul, one_mul, zero_mul] at hx
rw [hcohortTop, htime x, hintercept] at hx
simp [treatmentIndicator,
absorbingTreatment_eq] at hx
exact hx
have hu : u = 0 := by
funext j
rcases j with (_ | j)
· exact hintercept
· rcases j with (j | j)
· exact hcohortZero j
· exact htimeZero' j
have hbeta : beta = 0 := by
have hx := hc1 (⟨1, by decide⟩ : Fin 4)
simp [collapsedIndex, collapsedRegressor, hu] at hx
norm_num [fourLateCohort, treatmentIndicator,
absorbingTreatment_eq] at hx
exact hx
ext j
· exact congrFun hu j
· exact hbeta
exact ha hzero
theorem fourFittedMean_zeroEffects
With zero treatment effects, the fitted mean equals one in every supported four-cohort cell.
Formal statement
hypotheses
conclusion
Proof (Lean source)
lemma fourFittedMean_zeroEffects (g : Cohort 4) (hg : g ∈ fourCohortSupport)
(t : Fin 4) :
fittedMean 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma zeroEffects4 g t = 1 := by
let Omega : ℕ → Type := fun _ => Unit
let P : ∀ N, SamplingLaw (Omega N) := fun _ f => f ()
let Y : ∀ N, Fin N → Fin 4 → Fin 2 → Omega N → ℝ := fun _ _ _ _ _ => 1
let b : ∀ N, Fin N → PosReal := fun _ _ => ⟨1, zero_lt_one⟩
have hMean : UnitUntreatedExponentialMean 4 Omega P Y b fourCohortGamma := by
constructor
· intro N i s
simp [P, Y, b, fourCohortGamma, expectationUnder]
· intro s hs
rfl
have hhom : ∀ k ∈ fourCohortSupport, ∀ s : Fin 4,
treatmentIndicator 4 k s = 1 → zeroEffects4 (k, s) = 0 := by
simp [zeroEffects4]
have hfit := (homogeneous_effect_reduction 4 fourCohortSupport Omega P Y b
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4 0
hMean fourCohortCollapsedDesignRank hhom).2 g hg t
simpa [untreatedMean, fourCohortLimitBaseline, fourCohortGamma] using hfit
theorem fourResidualTable_row_sum
Each cohort's entries in the explicit four-cohort residual table sum to zero over time.
Formal statement
Proof (Lean source)
lemma fourResidualTable_row_sum (g : Cohort 4) (hg : g ∈ fourCohortSupport) :
(∑ t : Fin 4, fourResidualTable g t) = 0 := by
simp only [fourCohortSupport, Finset.mem_insert, mem_singleton] at hg
rcases hg with rfl | rfl | rfl | rfl <;>
norm_num [fourResidualTable, fourResidualNumerator, Fin.sum_univ_succ]
theorem fourResidualTable_column_sum
The explicit four-cohort residual table sums to zero across cohorts in every period.
Formal statement
Proof (Lean source)
lemma fourResidualTable_column_sum (t : Fin 4) :
(∑ g ∈ fourCohortSupport, fourResidualTable g t) = 0 := by
fin_cases t <;>
norm_num [fourCohortSupport, fourResidualTable, fourResidualNumerator]
theorem additive_supported_mem_collapsedNuisanceSubspace
Any supported-cell function that is additive in an intercept, cohort component, and time component belongs to the collapsed fixed-effects nuisance space.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
alpha :
ℝ
cohortPart :
Cohort T → ℝ
timePart :
Fin T → ℝ
hcohortTop :
cohortPart ⊤ = 0
htimeZero :
timePart ⟨0, hT⟩ = 0
conclusion
(fun z : SupportedCell T C => alpha + cohortPart z.1.1 + timePart z.2) ∈ collapsedNuisanceSubspace T C
Proof (Lean source)
lemma additive_supported_mem_collapsedNuisanceSubspace
(T : ℕ) (hT : 0 < T) (C : Finset (Cohort T))
(alpha : ℝ) (cohortPart : Cohort T → ℝ) (timePart : Fin T → ℝ)
(hcohortTop : cohortPart ⊤ = 0)
(htimeZero : timePart ⟨0, hT⟩ = 0) :
(fun z : SupportedCell T C => alpha + cohortPart z.1.1 + timePart z.2) ∈
collapsedNuisanceSubspace T C := by
classical
let rho : CollapsedNuisanceIndex T C → ℝ
| inl _ => alpha
| inr (inl g) => cohortPart g.1.1
| inr (inr t) => timePart t.1
apply (Submodule.mem_span_range_iff_exists_fun ℝ).mpr
refine ⟨rho, ?_⟩
funext z
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul,
collapsedNuisanceSubspace, collapsedNuisanceRegressor,
Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton, one_mul]
have hcohort : (∑ g : CohortDummy T C,
if z.1.1 = g.1.1 then cohortPart g.1.1 else 0) = cohortPart z.1.1 := by
by_cases htop : z.1.1 = ⊤
· rw [htop, hcohortTop]
apply Fintype.sum_eq_zero
intro g
simp only [ite_eq_right_iff]
intro heq
exact (g.2 heq.symm).elim
· let g : CohortDummy T C := ⟨z.1, htop⟩
rw [Fintype.sum_eq_single g]
· simp [g]
· intro y hy
rw [if_neg]
intro heq
exact hy (Subtype.ext (Subtype.ext heq.symm))
have htime : (∑ t : TimeDummy T,
if z.2 = t.1 then timePart t.1 else 0) = timePart z.2 := by
by_cases hz : z.2 = ⟨0, hT⟩
· rw [hz, htimeZero]
apply Fintype.sum_eq_zero
intro t
simp only [ite_eq_right_iff]
intro heq
exact (t.2 (by simpa [← heq])).elim
· have hzval : z.2.val ≠ 0 := by
intro hv
apply hz
apply Fin.ext
simpa using hv
let t : TimeDummy T := ⟨z.2, hzval⟩
rw [Fintype.sum_eq_single t]
· simp [t]
· intro y hy
rw [if_neg]
intro heq
exact hy (Subtype.ext heq.symm)
simp only [rho, one_mul, mul_ite, mul_one, mul_zero]
rw [hcohort, htime]
ring
theorem fourResidualProjection_mem
In the four-cohort design, treatment minus the displayed residual table is a fixed-effects nuisance component.
Formal statement
conclusion
(fun z : SupportedCell 4 fourCohortSupport => treatmentIndicator 4 z.1.1 z.2 - fourResidualTable z.1.1 z.2) ∈ collapsedNuisanceSubspace 4 fourCohortSupport
Proof (Lean source)
lemma fourResidualProjection_mem :
(fun z : SupportedCell 4 fourCohortSupport =>
treatmentIndicator 4 z.1.1 z.2 - fourResidualTable z.1.1 z.2) ∈
collapsedNuisanceSubspace 4 fourCohortSupport := by
let cohortPart : Cohort 4 → ℝ := fun g =>
if g = fourLateCohort then 3 / 4
else if g = ((⟨2, by decide⟩ : Fin 4) : Cohort 4) then 1 / 2
else if g = ((⟨3, by decide⟩ : Fin 4) : Cohort 4) then 1 / 4
else 0
let timePart : Fin 4 → ℝ := fun t => t.val / 4
have hadd := additive_supported_mem_collapsedNuisanceSubspace 4 fourHorizonPositive
fourCohortSupport (-(3 : ℝ) / 8) cohortPart timePart (by simp [cohortPart, fourLateCohort])
(by simp [timePart])
convert hadd using 1
funext z
rcases z with ⟨⟨g, hg⟩, t⟩
simp only [fourCohortSupport, Finset.mem_insert, mem_singleton] at hg
rcases hg with h | h | h | h
· subst g
have h10 : ¬((((⟨1, by decide⟩ : Fin 4) : Cohort 4)) ≤
(((⟨0, by decide⟩ : Fin 4) : Cohort 4))) := by
simp only [WithTop.coe_le_coe, Fin.mk_le_mk]
omega
fin_cases t <;> simp [cohortPart, timePart, fourLateCohort, h10,
fourResidualTable, fourResidualNumerator, treatmentIndicator,
absorbingTreatment_eq] <;> norm_num <;> decide
· subst g
fin_cases t <;> simp [cohortPart, timePart, fourLateCohort,
fourResidualTable, fourResidualNumerator, treatmentIndicator,
absorbingTreatment_eq] <;> norm_num
· subst g
fin_cases t <;> simp [cohortPart, timePart, fourLateCohort,
fourResidualTable, fourResidualNumerator, treatmentIndicator,
absorbingTreatment_eq] <;> norm_num
· subst g
fin_cases t <;> simp [cohortPart, timePart, fourLateCohort,
fourResidualTable, fourResidualNumerator, treatmentIndicator,
absorbingTreatment_eq] <;> norm_num
theorem fourMeanWeightedSupport_weight
Under zero treatment effects, every supported cell receives equal mean-projection weight, namely one sixteenth.
Formal statement
hypotheses
conclusion
Proof (Lean source)
lemma fourMeanWeightedSupport_weight (z : SupportedCell 4 fourCohortSupport) :
(meanWeightedSupport 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4).weight z =
(1 : ℝ) / 16 := by
unfold meanWeightedSupport normalizedPositiveSupport
simp only [Finset.mem_univ, ↓reduceIte]
simp only [meanFWLWeight]
have hfit (y : SupportedCell 4 fourCohortSupport) :
fittedMean 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma zeroEffects4 y.1.1 y.2 = 1 :=
fourFittedMean_zeroEffects y.1.1 y.1.2 y.2
simp_rw [hfit]
norm_num [meanFWLWeight, limitingCellMass, fourCohortShare,
Fintype.sum_prod_type, fourCohortSupport]
theorem fourResidualTable_nuisance_normal
The explicit residual table has zero unweighted inner product with every nuisance regressor.
Formal statement
hypotheses
conclusion
(∑ z : SupportedCell 4 fourCohortSupport, fourResidualTable z.1.1 z.2 * collapsedNuisanceRegressor 4 fourCohortSupport z.1.1 z.2 j)
= 0
Proof (Lean source)
lemma fourResidualTable_nuisance_normal
(j : CollapsedNuisanceIndex 4 fourCohortSupport) :
(∑ z : SupportedCell 4 fourCohortSupport,
fourResidualTable z.1.1 z.2 *
collapsedNuisanceRegressor 4 fourCohortSupport z.1.1 z.2 j) = 0 := by
rw [Fintype.sum_prod_type]
rcases j with (_ | j)
· simp only [collapsedNuisanceRegressor, mul_one]
apply Fintype.sum_eq_zero
intro g
exact fourResidualTable_row_sum g.1 g.2
· rcases j with (j | j)
· apply Fintype.sum_eq_zero
intro g
simp only [collapsedNuisanceRegressor]
by_cases hgj : g.1 = j.1.1
· simp only [hgj, ↓reduceIte, mul_one]
exact fourResidualTable_row_sum j.1.1 j.1.2
· simp [hgj]
· rw [Finset.sum_comm]
apply Fintype.sum_eq_zero
intro t
by_cases htj : t = j.1
· subst t
simp only [collapsedNuisanceRegressor, ↓reduceIte, mul_one]
exact (Finset.sum_attach _ _).trans (fourResidualTable_column_sum j.1)
· simp [collapsedNuisanceRegressor, htj]
theorem fourResidualTable_orthogonal
The explicit residual table is orthogonal, under the mean weights, to the entire fixed-effects nuisance space.
Formal statement
conclusion
let c := meanWeightedSupport 4 fourCohortSupport fourHorizonPositive fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4 let H := collapsedNuisanceSubspace 4 fourCohortSupport let R : SupportedCell 4 fourCohortSupport → ℝ := fun z
=> fourResidualTable z.1.1 z.2 ∀ h ∈ H, c.ip R h = 0
Proof (Lean source)
lemma fourResidualTable_orthogonal :
let c := meanWeightedSupport 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline
fourCohortGamma zeroEffects4
let H := collapsedNuisanceSubspace 4 fourCohortSupport
let R : SupportedCell 4 fourCohortSupport → ℝ :=
fun z => fourResidualTable z.1.1 z.2
∀ h ∈ H, c.ip R h = 0 := by
classical
dsimp only
intro h hh
refine Submodule.span_induction ?_ ?_ ?_ ?_ hh
· rintro x ⟨j, rfl⟩
simp only [ip_def]
change (∑ r : SupportedCell 4 fourCohortSupport,
(meanWeightedSupport 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4).weight r *
fourResidualTable r.1.1 r.2 *
collapsedNuisanceRegressor 4 fourCohortSupport r.1.1 r.2 j) = 0
simp_rw [fourMeanWeightedSupport_weight]
rw [show (∑ r : SupportedCell 4 fourCohortSupport,
(1 / 16 : ℝ) * fourResidualTable r.1.1 r.2 *
collapsedNuisanceRegressor 4 fourCohortSupport r.1.1 r.2 j) =
(1 / 16 : ℝ) * ∑ r : SupportedCell 4 fourCohortSupport,
fourResidualTable r.1.1 r.2 *
collapsedNuisanceRegressor 4 fourCohortSupport r.1.1 r.2 j by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro r hr
ring]
rw [fourResidualTable_nuisance_normal, mul_zero]
· simp [ip]
· intro x y _ _ hx hy
rw [ip_add_right, hx, hy, add_zero]
· intro s x _ hx
rw [ip_smul_right, hx, mul_zero]
theorem fourWeightedFWLResidual_table
In the four-cohort zero-effect design, the weighted FWL treatment residual equals the explicit residual-table entry in every cell.
Formal statement
hypotheses
Proof (Lean source)
lemma fourWeightedFWLResidual_table (z : SupportedCell 4 fourCohortSupport) :
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4 z =
fourResidualTable z.1.1 z.2 := by
let c := meanWeightedSupport 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4
let H := collapsedNuisanceSubspace 4 fourCohortSupport
let D : SupportedCell 4 fourCohortSupport → ℝ :=
fun y => treatmentIndicator 4 y.1.1 y.2
let P : SupportedCell 4 fourCohortSupport → ℝ :=
fun y => D y - fourResidualTable y.1.1 y.2
have hP : P ∈ H := fourResidualProjection_mem
have horth : ∀ h ∈ H, c.ip (D - P) h = 0 := by
intro h hh
simpa [c, D, P, Pi.sub_apply] using fourResidualTable_orthogonal h hh
have hproj : c.proj H D z = P z :=
c.proj_apply_eq_of_mem_orthogonal H D hP horth z
(by simp [c, meanWeightedSupport, normalizedPositiveSupport])
rw [weightedFWLResidual]
change D z - c.proj H D z = _
rw [hproj]
simp [P]
theorem fourCohortDelta_eq_multiplier
The specified four-cohort effects coincide with the multiplier-effect family evaluated at multipliers 1.01 and 4.
Formal statement
conclusion
fourCohortDelta = fourMultiplierEffects ((101 : ℝ) / 100) 4
Proof (Lean source)
lemma fourCohortDelta_eq_multiplier :
fourCohortDelta = fourMultiplierEffects ((101 : ℝ) / 100) 4 := by
funext z
simp [fourCohortDelta, fourMultiplierEffects]
theorem fourFrontierEliminationHandle_exact
For the specified four-cohort effects, the frontier elimination handle is exactly negative 11559 divided by 32000.
Formal statement
conclusion
frontierEliminationHandle 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma fourCohortDelta
= -(11559 : ℝ) / 32000
Proof (Lean source)
lemma fourFrontierEliminationHandle_exact :
frontierEliminationHandle 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma fourCohortDelta =
-(11559 : ℝ) / 32000 := by
have hp : frontierEliminationHandle 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma
(fourMultiplierEffects ((101 : ℝ) / 100) 4) =
(5 * ((101 : ℝ) / 100) ^ 2 + 12 * ((101 : ℝ) / 100) - 2 * 4 - 15) / 16 := by
simp [frontierEliminationHandle, primitiveTotal, primitiveTreatedTotal,
primitiveRow, primitiveColumn, primitiveH, fourCohortSupport, fourCohortShare,
fourCohortLimitBaseline, fourCohortGamma, fourMultiplierEffects,
untreatedMean, treatmentIndicator,
absorbingTreatment_eq]
norm_num [Fin.sum_univ_succ]
simp [Real.exp_log (by norm_num : (0 : ℝ) < 101 / 100),
Real.exp_log (by norm_num : (0 : ℝ) < 4)]
ring
rw [fourCohortDelta_eq_multiplier, hp]
norm_num
theorem fourBetaStar_negative
The four-cohort design's pseudo-true PPML treatment coefficient is negative.
Formal statement
Proof (Lean source)
lemma fourBetaStar_negative :
betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma fourCohortDelta < 0 := by
apply (betaStar_sign_frontierEliminationHandle 4 fourCohortSupport
fourHorizonPositive (by simp [fourCohortSupport]) fourCohortShare
fourCohortLimitBaseline fourCohortGamma fourCohortDelta
fourCohortCollapsedDesignRank).1.mpr
rw [fourFrontierEliminationHandle_exact]
norm_num
theorem fourCohortDelta_positive
Every treated cell in the four-cohort example has a strictly positive log treatment effect.
Formal statement
conclusion
∀ g ∈ fourCohortSupport,
Proof (Lean source)
lemma fourCohortDelta_positive :
∀ g ∈ fourCohortSupport, ∀ t : Fin 4,
treatmentIndicator 4 g t = 1 → 0 < fourCohortDelta (g, t) := by
intro g hg t hD
rw [fourCohortDelta, if_pos hD]
split
· exact Real.log_pos (by norm_num)
· exact Real.log_pos (by norm_num)
theorem fourCohortDelta_late_largest
The late treated cell has a strictly larger log treatment effect than every other treated cell.
Formal statement
conclusion
∀ g ∈ fourCohortSupport,
∀ t : Fin 4,
treatmentIndicator 4 g t
= 1 → (g, t) ≠ (fourLateCohort, fourLatePeriod) → fourCohortDelta (g, t) < fourCohortDelta (fourLateCohort, fourLatePeriod)
Proof (Lean source)
lemma fourCohortDelta_late_largest :
∀ g ∈ fourCohortSupport, ∀ t : Fin 4,
treatmentIndicator 4 g t = 1 →
(g, t) ≠ (fourLateCohort, fourLatePeriod) →
fourCohortDelta (g, t) < fourCohortDelta (fourLateCohort, fourLatePeriod) := by
intro g hg t hD hne
have hnot : ¬(g = fourLateCohort ∧ t = fourLatePeriod) := by
intro h
exact hne (Prod.ext h.1 h.2)
rw [fourCohortDelta, if_pos hD]
have hnot' : ¬(g = ((⟨1, by decide⟩ : Fin 4) : Cohort 4) ∧
t = (⟨3, by decide⟩ : Fin 4)) := by
simpa [fourLateCohort, fourLatePeriod] using hnot
rw [if_neg hnot']
have hlateD : treatmentIndicator 4 fourLateCohort fourLatePeriod = 1 := by
norm_num [fourLateCohort, fourLatePeriod, treatmentIndicator,
absorbingTreatment_eq, Fin.mk_le_mk]
rw [fourCohortDelta, if_pos hlateD, if_pos ⟨rfl, rfl⟩]
exact Real.strictMonoOn_log (by norm_num) (by norm_num) (by norm_num)
theorem fourPrimitive_mem_signReversalRegion
The four-cohort primitive data satisfy all conditions defining the sign-reversal region.
Formal statement
Proof (Lean source)
lemma fourPrimitive_mem_signReversalRegion :
restrictSignReversalPrimitive 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma fourCohortDelta ∈
signReversalRegion 4 fourCohortSupport fourCohortGamma := by
unfold signReversalRegion
refine ⟨(by show 4 ≤ 4; norm_num), ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· constructor
· simp [fourCohortSupport]
· intro g hg
simp only [fourCohortSupport, Finset.mem_insert, mem_singleton] at hg
rcases hg with h | h | h | h <;> simp_all
· refine ⟨⟨⟨1, by decide⟩, rfl, by simp [fourCohortSupport]⟩,
⟨⟨2, by decide⟩, rfl, by simp [fourCohortSupport]⟩,
⟨⟨3, by decide⟩, rfl, by simp [fourCohortSupport]⟩,
by simp [fourCohortSupport]⟩
· norm_num [restrictSignReversalPrimitive, fourCohortSupport, fourCohortShare] <;> rfl
· refine ⟨fun _ => ⟨1, zero_lt_one⟩, ?_⟩
intro z
simp [restrictSignReversalPrimitive, untreatedMean, fourCohortLimitBaseline,
fourCohortGamma]
· intro z
exact fourCohortDelta_positive z.1.1.1 z.1.1.2 z.1.2 z.2
· intro a ha
change 0 < ∑ z : SupportedCell 4 fourCohortSupport,
((fourCohortShare z.1.1 : ℝ) / 4) *
collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport z.1.1 z.2) a ^ 2
rw [Fintype.sum_prod_type]
have hr := fourCohortCollapsedDesignRank a ha
rw [show (∑ z : ↑fourCohortSupport, ∑ t : Fin 4,
((fourCohortShare z.1 : ℝ) / 4) *
collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport z.1 t) a ^ 2) =
∑ g ∈ fourCohortSupport, ∑ t : Fin 4,
((fourCohortShare g : ℝ) / 4) *
collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport g t) a ^ 2 by
simpa using Finset.sum_attach (s := fourCohortSupport)
(f := fun g => ∑ t : Fin 4, ((fourCohortShare g : ℝ) / 4) *
collapsedIndex 4 fourCohortSupport
(collapsedRegressor 4 fourCohortSupport g t) a ^ 2)]
simpa [limitingCellMass] using hr
· rw [primitiveBetaStar_restrict]
exact fourBetaStar_negative
theorem fourLateResidual_exact
The weighted FWL residual in the designated late-treated cell is exactly negative one eighth.
Formal statement
Proof (Lean source)
lemma fourLateResidual_exact :
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4
fourLateSupportedCell = -(1 : ℝ) / 8 := by
rw [fourWeightedFWLResidual_table]
norm_num [fourLateSupportedCell, fourLateCohort, fourLatePeriod,
fourResidualTable, fourResidualNumerator]
theorem fourFWLEnergy_zeroEffects
With zero treatment effects, the weighted FWL residual energy is exactly five sixty-fourths.
Formal statement
conclusion
Proof (Lean source)
lemma fourFWLEnergy_zeroEffects :
fwlEnergy 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4 =
(5 : ℝ) / 64 := by
unfold fwlEnergy
have hfit (z : SupportedCell 4 fourCohortSupport) :
fittedMean 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma zeroEffects4 z.1.1 z.2 = 1 :=
fourFittedMean_zeroEffects z.1.1 z.1.2 z.2
simp_rw [hfit, fourWeightedFWLResidual_table]
rw [Fintype.sum_prod_type]
rw [show (∑ g : ↑fourCohortSupport, ∑ t : Fin 4,
limitingCellMass 4 fourCohortShare g.1 * 1 * fourResidualTable g.1 t ^ 2) =
∑ g ∈ fourCohortSupport, ∑ t : Fin 4,
limitingCellMass 4 fourCohortShare g * 1 * fourResidualTable g t ^ 2 by
simpa using Finset.sum_attach (s := fourCohortSupport)
(f := fun g => ∑ t : Fin 4,
limitingCellMass 4 fourCohortShare g * 1 * fourResidualTable g t ^ 2)]
norm_num [fourCohortSupport, limitingCellMass, fourCohortShare,
fourResidualTable, fourResidualNumerator, Fin.sum_univ_succ]
theorem fourLateDerivative_exact
At zero effects, increasing the late cell's log effect changes the pseudo-true PPML treatment coefficient at the exact rate negative one tenth.
Formal statement
conclusion
HasDerivAt (fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma (update zeroEffects4 (fourLateCohort, fourLatePeriod) x)) (-(1 : ℝ) / 10) 0
Proof (Lean source)
lemma fourLateDerivative_exact :
HasDerivAt
(fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma
(update zeroEffects4 (fourLateCohort, fourLatePeriod) x))
(-(1 : ℝ) / 10) 0 := by
have hlateMem : fourLateCohort ∈ fourCohortSupport := by
simp [fourLateCohort, fourCohortSupport]
have hlateD : treatmentIndicator 4 fourLateCohort fourLatePeriod = 1 := by
norm_num [fourLateCohort, fourLatePeriod, treatmentIndicator,
absorbingTreatment_eq, Fin.mk_le_mk]
have hs := (sharp_ppml_forbidden_sign 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
zeroEffects4 fourLateCohort hlateMem fourLatePeriod hlateD
fourCohortCollapsedDesignRank).1
convert hs using 1
· rw [fourFWLEnergy_zeroEffects]
have hW := fourLateResidual_exact
change -(1 : ℝ) / 10 = limitingCellMass 4 fourCohortShare fourLateCohort *
untreatedMean 4 fourCohortLimitBaseline fourCohortGamma fourLateCohort
fourLatePeriod * exp (zeroEffects4 (fourLateCohort, fourLatePeriod)) *
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4
(⟨fourLateCohort, hlateMem⟩, fourLatePeriod) / (5 / 64)
rw [show weightedFWLResidual 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
zeroEffects4 (⟨fourLateCohort, hlateMem⟩, fourLatePeriod) = -1 / 8 by
simpa [fourLateSupportedCell] using hW]
norm_num [limitingCellMass, fourCohortShare, untreatedMean,
fourCohortLimitBaseline, fourCohortGamma, zeroEffects4]
case e'_10 => rfl
theorem limitingCriterion_congr_supported
Changing treatment effects outside the supported cohorts leaves the limiting PPML criterion unchanged.
Formal statement
hypotheses
T :
ℕ
gamma :
Fin T → ℝ
delta delta' :
Cell T → ℝ
hdelta :
∀ g ∈ C, ∀ t, delta (g, t) = delta' (g, t)
conclusion
limitingCriterion T C pi barB gamma delta = limitingCriterion T C pi barB gamma delta'
Proof (Lean source)
lemma limitingCriterion_congr_supported
(T : ℕ) (C : Finset (Cohort T)) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta delta' : Cell T → ℝ)
(hdelta : ∀ g ∈ C, ∀ t, delta (g, t) = delta' (g, t)) :
limitingCriterion T C pi barB gamma delta =
limitingCriterion T C pi barB gamma delta' := by
funext theta
unfold limitingCriterion
apply Finset.sum_congr rfl
intro g hg
apply Finset.sum_congr rfl
intro t ht
rw [show observedCohortMean T barB gamma delta g t =
observedCohortMean T barB gamma delta' g t by
unfold observedCohortMean
rw [hdelta g hg t]]
theorem fittedMean_congr_supported
Changing treatment effects outside the supported cohorts leaves every fitted mean unchanged.
Formal statement
hypotheses
T :
ℕ
gamma :
Fin T → ℝ
delta delta' :
Cell T → ℝ
hdelta :
∀ g ∈ C, ∀ t, delta (g, t) = delta' (g, t)
g :
Cohort T
t :
Fin T
conclusion
fittedMean T C pi barB gamma delta g t = fittedMean T C pi barB gamma delta' g t
Proof (Lean source)
lemma fittedMean_congr_supported
(T : ℕ) (C : Finset (Cohort T)) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta delta' : Cell T → ℝ)
(hdelta : ∀ g ∈ C, ∀ t, delta (g, t) = delta' (g, t))
(g : Cohort T) (t : Fin T) :
fittedMean T C pi barB gamma delta g t =
fittedMean T C pi barB gamma delta' g t := by
unfold fittedMean collapsedPopulationProjection
rw [limitingCriterion_congr_supported T C pi barB gamma delta delta' hdelta]
theorem weightedFWLResidual_congr_supported
Changing treatment effects outside the supported cohorts leaves the weighted FWL treatment residual unchanged.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
delta delta' :
Cell T → ℝ
hdelta :
∀ g ∈ C, ∀ t, delta (g, t) = delta' (g, t)
conclusion
weightedFWLResidual T C hT hC pi barB gamma delta
= weightedFWLResidual T C hT hC pi barB gamma delta'
Proof (Lean source)
lemma weightedFWLResidual_congr_supported
(T : ℕ) (C : Finset (Cohort T)) (hT : 0 < T) (hC : C.Nonempty)
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta delta' : Cell T → ℝ)
(hdelta : ∀ g ∈ C, ∀ t, delta (g, t) = delta' (g, t)) :
weightedFWLResidual T C hT hC pi barB gamma delta =
weightedFWLResidual T C hT hC pi barB gamma delta' := by
have hc : meanWeightedSupport T C hT hC pi barB gamma delta =
meanWeightedSupport T C hT hC pi barB gamma delta' := by
unfold meanWeightedSupport
congr 1
funext z
unfold meanFWLWeight
rw [fittedMean_congr_supported T C pi barB gamma delta delta' hdelta]
unfold weightedFWLResidual
rw [hc]
theorem fourLateDerivative_negative_neighborhood
There is a neighborhood of zero effects in which positive effects still give a negative marginal effect of the late cell on the pseudo-true PPML treatment coefficient.
Formal statement
conclusion
∃ epsilon : ℝ
if
0 < epsilon ∧ ∀ delta' : Cell 4
and
ℝ, (∀ g ∈ fourCohortSupport, ∀ t : Fin 4, |delta' (g, t)| < epsilon)
and
StrictPositiveEffects 4 fourCohortSupport delta'
then
deriv (fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma (update delta' (fourLateCohort, fourLatePeriod) x)) (delta' (fourLateCohort, fourLatePeriod)) < 0
Proof (Lean source)
lemma fourLateDerivative_negative_neighborhood :
∃ epsilon : ℝ, 0 < epsilon ∧
∀ delta' : Cell 4 → ℝ,
(∀ g ∈ fourCohortSupport, ∀ t : Fin 4, |delta' (g, t)| < epsilon) →
StrictPositiveEffects 4 fourCohortSupport delta' →
deriv (fun x => betaStar 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma
(update delta' (fourLateCohort, fourLatePeriod) x))
(delta' (fourLateCohort, fourLatePeriod)) < 0 := by
let W : (Cell 4 → ℝ) → ℝ := fun delta =>
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma delta
fourLateSupportedCell
have hcont : ContinuousAt W zeroEffects4 :=
weightedFWLResidual_continuousAt_effects 4 fourCohortSupport
fourHorizonPositive fourSupportNonempty fourCohortShare fourCohortLimitBaseline
fourCohortGamma fourCohortCollapsedDesignRank zeroEffects4 fourLateSupportedCell
have hWzero : W zeroEffects4 < 0 := by
rw [show W zeroEffects4 = -(1 : ℝ) / 8 by exact fourLateResidual_exact]
norm_num
have hopen : Iio (0 : ℝ) ∈ nhds (W zeroEffects4) :=
IsOpen.mem_nhds isOpen_Iio hWzero
have hpre : W ⁻¹' Iio (0 : ℝ) ∈ nhds zeroEffects4 := hcont hopen
obtain ⟨I, target, htarget, hpi⟩ :
∃ (I : Finset (Cell 4)) (target : Cell 4 → Set ℝ),
(∀ i, target i ∈ nhds (zeroEffects4 i)) ∧
pi I target ⊆ W ⁻¹' Iio (0 : ℝ) := by
rw [nhds_pi, Filter.mem_pi] at hpre
obtain ⟨s, hs, target, htarget, hpi⟩ := hpre
exact ⟨hs.toFinset, target, htarget, by simpa using hpi⟩
have hradius : ∀ i : Cell 4, ∃ r : ℝ, 0 < r ∧
ball (zeroEffects4 i) r ⊆ target i := by
intro i
exact Metric.mem_nhds_iff.mp (htarget i)
choose radius hradiusPos hradiusSub using hradius
let epsilon : ℝ := if hI : I.Nonempty then
(I.image radius).min' (hI.image radius) else 1
have hepsilon : 0 < epsilon := by
by_cases hI : I.Nonempty
· rw [show epsilon = (I.image radius).min' (hI.image radius) by simp [epsilon, hI]]
have hmem := (I.image radius).min'_mem (hI.image radius)
obtain ⟨i, hi, heq⟩ := Finset.mem_image.mp hmem
rw [← heq]
exact hradiusPos i
· simp [epsilon, hI]
have hepsilon_le (i : Cell 4) (hi : i ∈ I) : epsilon ≤ radius i := by
have hI : I.Nonempty := ⟨i, hi⟩
rw [show epsilon = (I.image radius).min' (hI.image radius) by simp [epsilon, hI]]
exact Finset.min'_le _ _ (Finset.mem_image.mpr ⟨i, hi, rfl⟩)
refine ⟨epsilon, hepsilon, ?_⟩
intro delta' hsmall hpositive
let deltaSupported : Cell 4 → ℝ := fun z =>
if z.1 ∈ fourCohortSupport then delta' z else 0
have hdeltaSupported : deltaSupported ∈ pi I target := by
intro z hzI
apply hradiusSub z
rw [Metric.mem_ball]
apply lt_of_lt_of_le _ (hepsilon_le z hzI)
by_cases hz : z.1 ∈ fourCohortSupport
· simpa [deltaSupported, hz, zeroEffects4, Real.dist_eq] using
hsmall z.1 hz z.2
· simpa [deltaSupported, hz, zeroEffects4] using hepsilon
have hWsupported : W deltaSupported < 0 := hpi hdeltaSupported
have hcongr : weightedFWLResidual 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
delta' = weightedFWLResidual 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
deltaSupported := by
apply weightedFWLResidual_congr_supported
intro g hg t
simp [deltaSupported, hg]
have hWneg : weightedFWLResidual 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
delta' fourLateSupportedCell < 0 := by
rw [hcongr]
exact hWsupported
have hlateMem : fourLateCohort ∈ fourCohortSupport := by
simp [fourLateCohort, fourCohortSupport]
have hlateD : treatmentIndicator 4 fourLateCohort fourLatePeriod = 1 := by
norm_num [fourLateCohort, fourLatePeriod, treatmentIndicator,
absorbingTreatment_eq, Fin.mk_le_mk]
have hs := sharp_ppml_forbidden_sign 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
delta' fourLateCohort hlateMem fourLatePeriod hlateD
fourCohortCollapsedDesignRank
have hWneg' : weightedFWLResidual 4 fourCohortSupport fourHorizonPositive
fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma
delta' (⟨fourLateCohort, hlateMem⟩, fourLatePeriod) < 0 := by
simpa [fourLateSupportedCell] using hWneg
have hformulaNeg := hs.2.2.1.mpr hWneg'
rw [hs.1.deriv]
exact hformulaNeg
W4 is an all-positive sign reversal and has the stated negative late-cell derivative.
Formal statement
conclusion
restrictSignReversalPrimitive 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma fourCohortDelta ∈ signReversalRegion 4 fourCohortSupport fourCohortGamma ∧
(∀ g ∈ fourCohortSupport, ∀ t : Fin 4, treatmentIndicator 4 g t = 1 → (g, t) ≠ (fourLateCohort, fourLatePeriod) → fourCohortDelta (g, t) < fourCohortDelta (fourLateCohort, fourLatePeriod)) ∧
(∀ z : SupportedCell 4 fourCohortSupport, weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4 z = fourResidualTable z.1.1 z.2) ∧
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4 fourLateSupportedCell
= -(1 : ℝ) / 8 ∧
HasDerivAt (fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma (update zeroEffects4 (fourLateCohort, fourLatePeriod) x)) (-(1 : ℝ) / 10) 0 ∧
∃ epsilon : ℝ,
0 < epsilon ∧
∀ delta' : Cell 4 → ℝ,
(∀ g ∈ fourCohortSupport, ∀ t : Fin 4, |delta' (g, t)| < epsilon) → StrictPositiveEffects 4 fourCohortSupport delta' → deriv (fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma (update delta' (fourLateCohort, fourLatePeriod) x)) (delta' (fourLateCohort, fourLatePeriod)) < 0
Proof (Lean source)
theorem four_cohort_sign_reversal :
restrictSignReversalPrimitive 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma fourCohortDelta ∈
signReversalRegion 4 fourCohortSupport fourCohortGamma ∧
(∀ g ∈ fourCohortSupport, ∀ t : Fin 4,
treatmentIndicator 4 g t = 1 → 0 < fourCohortDelta (g, t)) ∧
(∀ g ∈ fourCohortSupport, ∀ t : Fin 4,
treatmentIndicator 4 g t = 1 →
(g, t) ≠ (fourLateCohort, fourLatePeriod) →
fourCohortDelta (g, t) <
fourCohortDelta (fourLateCohort, fourLatePeriod)) ∧
(∀ z : SupportedCell 4 fourCohortSupport,
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4
z = fourResidualTable z.1.1 z.2) ∧
weightedFWLResidual 4 fourCohortSupport fourHorizonPositive fourSupportNonempty
fourCohortShare fourCohortLimitBaseline fourCohortGamma zeroEffects4
fourLateSupportedCell = -(1 : ℝ) / 8 ∧
HasDerivAt
(fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma
(update zeroEffects4 (fourLateCohort, fourLatePeriod) x))
(-(1 : ℝ) / 10) 0 ∧
∃ epsilon : ℝ, 0 < epsilon ∧
∀ delta' : Cell 4 → ℝ,
(∀ g ∈ fourCohortSupport, ∀ t : Fin 4, |delta' (g, t)| < epsilon) →
StrictPositiveEffects 4 fourCohortSupport delta' →
deriv (fun x => betaStar 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline
fourCohortGamma
(update delta' (fourLateCohort, fourLatePeriod) x))
(delta' (fourLateCohort, fourLatePeriod)) < 0 := by
exact ⟨fourPrimitive_mem_signReversalRegion, fourCohortDelta_positive,
fourCohortDelta_late_largest, fourWeightedFWLResidual_table,
fourLateResidual_exact, fourLateDerivative_exact,
fourLateDerivative_negative_neighborhood⟩
Helpers.FiniteCollapse 23 declarations This module contains the panel-specific algebra for collapsing a finite unit fixed-effect Poisson criterion to supported cohort-time cells.
Finite unit fixed-effect collapse
This module contains the panel-specific algebra for collapsing a finite unit fixed-effect Poisson criterion to supported cohort-time cells.
theorem finiteCollapsedCriterion_eq_finitePoissonObjective
The finite collapsed criterion is the generic finite Poisson objective on the supported cohort-time table.
Formal statement
hypotheses
conclusion
finiteCollapsedCriterion T C G b gamma delta theta
= finitePoissonObjective (fun z : SupportedCell T C => finiteCellMass T G z.1.1) (fun z : SupportedCell T C => finiteObservedCohortMean T G b gamma delta z.1.1 z.2) (collapsedDesignMap T C) theta
Proof (Lean source)
lemma finiteCollapsedCriterion_eq_finitePoissonObjective (T : ℕ)
(C : Finset (Cohort T)) {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(theta : CollapsedParameter T C) :
finiteCollapsedCriterion T C G b gamma delta theta =
finitePoissonObjective
(fun z : SupportedCell T C => finiteCellMass T G z.1.1)
(fun z : SupportedCell T C =>
finiteObservedCohortMean T G b gamma delta z.1.1 z.2)
(collapsedDesignMap T C) theta := by
classical
rw [finiteCollapsedCriterion, finitePoissonObjective, Fintype.sum_prod_type]
rw [← Finset.sum_attach]
rfl
theorem collapsedDesignMap_injective
The paper's positive-weight rank condition makes the collapsed design map injective.
Formal statement
hypotheses
conclusion
Injective (collapsedDesignMap T C)
Proof (Lean source)
lemma collapsedDesignMap_injective (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (hRank : CollapsedDesignRank T C pi) :
Injective (collapsedDesignMap T C) := by
intro x y hxy
by_contra hne
have hsub : x - y ≠ 0 := sub_ne_zero.mpr hne
have hr := hRank (x - y) hsub
have hmap : collapsedDesignMap T C (x - y) = 0 := by
rw [map_sub, hxy, sub_self]
have hzero :
(∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) (x - y)) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
have hz := congrFun hmap (⟨g, hg⟩, t)
change collapsedIndex T C (collapsedRegressor T C g t) (x - y) = 0 at hz
rw [hz]
simp
linarith
theorem finiteCollapsedCriterion_exists_unique_max
Positive supported counts and collapsed full rank give a unique finite collapsed maximizer.
Formal statement
hypotheses
T :
ℕ
N :
ℕ
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hT :
0 < T
hC :
C.Nonempty
hCount :
∀ g ∈ C, 0 < cohortCount T G g
hRank :
CollapsedDesignRank T C pi
conclusion
∃! theta : CollapsedParameter T C,
∀ eta,
finiteCollapsedCriterion T C G b gamma delta eta
≤ finiteCollapsedCriterion T C G b gamma delta theta
Proof (Lean source)
lemma finiteCollapsedCriterion_exists_unique_max (T : ℕ)
(C : Finset (Cohort T)) {N : ℕ} (G : Fin N → Cohort T)
(b : Fin N → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(pi : Cohort T → OpenUnit) (hT : 0 < T) (hC : C.Nonempty)
(hCount : ∀ g ∈ C, 0 < cohortCount T G g)
(hRank : CollapsedDesignRank T C pi) :
∃! theta : CollapsedParameter T C,
∀ eta, finiteCollapsedCriterion T C G b gamma delta eta ≤
finiteCollapsedCriterion T C G b gamma delta theta := by
classical
let q : SupportedCell T C → ℝ := fun z => finiteCellMass T G z.1.1
let m : SupportedCell T C → ℝ := fun z =>
finiteObservedCohortMean T G b gamma delta z.1.1 z.2
letI : Nonempty (SupportedCell T C) :=
⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩)⟩
have hN : 0 < N := by
obtain ⟨i, hi⟩ := (Finset.card_pos.mp
(show 0 < (Finset.univ.filter fun i => G i = hC.choose).card by
simpa [cohortCount] using hCount hC.choose hC.choose_spec))
exact Nat.zero_lt_of_lt i.isLt
have hq : ∀ z, 0 < q z := by
intro z
exact div_pos (Nat.cast_pos.mpr (hCount z.1.1 z.1.2))
(mul_pos (Nat.cast_pos.mpr hN) (Nat.cast_pos.mpr hT))
have hm : ∀ z, 0 < m z := by
intro z
exact finiteObservedCohortMean_pos T G b gamma delta z.1.1 z.2
(hCount z.1.1 z.1.2)
obtain ⟨theta, hmax, hunique⟩ := finitePoissonObjective_exists_unique_max
q m (collapsedDesignMap T C) hq hm
(collapsedDesignMap_injective T C pi hRank)
refine ⟨theta, ?_, ?_⟩
· intro eta
simpa only [finiteCollapsedCriterion_eq_finitePoissonObjective] using hmax eta
· intro eta heta
apply hunique
intro z
simpa only [finiteCollapsedCriterion_eq_finitePoissonObjective] using heta z
The normalized intercept-plus-unit-effect represented by unit nuisance coordinates.
The normalized time effect represented by unit nuisance coordinates.
Definition (Lean source)
noncomputable def unitTimeLevel (T N : ℕ) (theta : UnitParameter N T) (t : Fin T) : ℝ :=
if ht : t.val ≠ 0 then theta.1 (inr (inr ⟨t, ht⟩)) else 0
theorem unitIndex_eq_levels
At any unit-period observation, the linear index of a unit-and-time fixed-effect parameter splits into three pieces: that unit's level (intercept plus its unit effect), that period's time effect, and the treatment coefficient times the unit's treatment indicator.
Formal statement
hypotheses
conclusion
unitIndex T N (unitRegressor T N G i t) theta
= unitLevel T N theta i
+ unitTimeLevel T N theta t
+ theta.2 * treatmentIndicator T (G i) t
Proof (Lean source)
lemma unitIndex_eq_levels (T N : ℕ) (G : Fin N → Cohort T)
(theta : UnitParameter N T) (i : Fin N) (t : Fin T) :
unitIndex T N (unitRegressor T N G i t) theta =
unitLevel T N theta i + unitTimeLevel T N theta t +
theta.2 * treatmentIndicator T (G i) t := by
classical
unfold unitIndex unitRegressor unitNuisanceRegressor unitTreatment unitLevel unitTimeLevel
simp only [Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton]
have hsumUnit : (∑ x : {j : Fin N // j.val ≠ 0},
if i = x.1 then theta.1 (inr (inl x)) else 0) =
if hi : i.val ≠ 0 then theta.1 (inr (inl ⟨i, hi⟩)) else 0 := by
by_cases hi : i.val ≠ 0
· rw [dif_pos hi, Finset.sum_eq_single ⟨i, hi⟩]
· simp
· intro x hx hne
simp only [ite_eq_right_iff]
intro heq
exact (hne (Subtype.ext heq.symm)).elim
· simp
· rw [dif_neg hi]
apply Finset.sum_eq_zero
intro x hx
simp only [ite_eq_right_iff]
intro heq
exact (hi (heq ▸ x.2)).elim
have hsumTime : (∑ x : {s : Fin T // s.val ≠ 0},
if t = x.1 then theta.1 (inr (inr x)) else 0) =
if ht : t.val ≠ 0 then theta.1 (inr (inr ⟨t, ht⟩)) else 0 := by
by_cases ht : t.val ≠ 0
· rw [dif_pos ht, Finset.sum_eq_single ⟨t, ht⟩]
· simp
· intro x hx hne
simp only [ite_eq_right_iff]
intro heq
exact (hne (Subtype.ext heq.symm)).elim
· simp
· rw [dif_neg ht]
apply Finset.sum_eq_zero
intro x hx
simp only [ite_eq_right_iff]
intro heq
exact (ht (heq ▸ x.2)).elim
simp only [ite_mul, one_mul, zero_mul]
rw [hsumUnit, hsumTime]
ring
The intercept-plus-cohort-effect represented by collapsed nuisance coordinates.
Definition (Lean source)
noncomputable def collapsedCohortLevel (T : ℕ) (C : Finset (Cohort T))
(theta : CollapsedParameter T C) (g : Cohort T) : ℝ :=
theta.1 (inl ()) + if hg : g ≠ ⊤ then
if hmem : g ∈ C then theta.1 (inr (inl ⟨⟨g, hmem⟩, hg⟩)) else 0 else 0
The time effect that a collapsed cohort-time parameter assigns to a calendar period: the period's own time-dummy coordinate, and zero in the omitted base period.
Definition (Lean source)
noncomputable def collapsedTimeLevel (T : ℕ) (C : Finset (Cohort T))
(theta : CollapsedParameter T C) (t : Fin T) : ℝ :=
if ht : t.val ≠ 0 then theta.1 (inr (inr ⟨t, ht⟩)) else 0
theorem collapsedIndex_eq_levels
At any supported cohort-time cell, the linear index of a collapsed parameter splits into three pieces: that cohort's level (intercept plus its cohort effect), that period's time effect, and the treatment coefficient times the cohort's treatment indicator.
Formal statement
hypotheses
conclusion
collapsedIndex T C (collapsedRegressor T C g t) theta
= collapsedCohortLevel T C theta g
+ collapsedTimeLevel T C theta t
+ theta.2 * treatmentIndicator T g t
Proof (Lean source)
lemma collapsedIndex_eq_levels (T : ℕ) (C : Finset (Cohort T))
(theta : CollapsedParameter T C) (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
collapsedIndex T C (collapsedRegressor T C g t) theta =
collapsedCohortLevel T C theta g + collapsedTimeLevel T C theta t +
theta.2 * treatmentIndicator T g t := by
classical
unfold collapsedIndex collapsedRegressor collapsedNuisanceRegressor
collapsedCohortLevel collapsedTimeLevel
simp only [Fintype.sum_sum_type, Finset.univ_unique, Finset.sum_singleton]
have hsumCohort : (∑ x : {c : {g : Cohort T // g ∈ C} // c.1 ≠ ⊤},
if g = x.1.1 then theta.1 (inr (inl x)) else 0) =
if hgt : g ≠ ⊤ then theta.1 (inr (inl ⟨⟨g, hg⟩, hgt⟩)) else 0 := by
by_cases hgt : g ≠ ⊤
· rw [dif_pos hgt, Finset.sum_eq_single ⟨⟨g, hg⟩, hgt⟩]
· simp
· intro x hx hne
simp only [ite_eq_right_iff]
intro heq
exfalso
apply hne
exact Subtype.ext (Subtype.ext heq.symm)
· simp
· rw [dif_neg hgt]
apply Finset.sum_eq_zero
intro x hx
simp only [ite_eq_right_iff]
intro heq
exact (x.2 (by simpa [heq] using not_not.mp hgt)).elim
have hsumTime : (∑ x : {s : Fin T // s.val ≠ 0},
if t = x.1 then theta.1 (inr (inr x)) else 0) =
if ht : t.val ≠ 0 then theta.1 (inr (inr ⟨t, ht⟩)) else 0 := by
by_cases ht : t.val ≠ 0
· rw [dif_pos ht, Finset.sum_eq_single ⟨t, ht⟩]
· simp
· intro x hx hne
simp only [ite_eq_right_iff]
intro heq
exact (hne (Subtype.ext heq.symm)).elim
· simp
· rw [dif_neg ht]
apply Finset.sum_eq_zero
intro x hx
simp only [ite_eq_right_iff]
intro heq
exact (ht (heq ▸ x.2)).elim
simp only [ite_mul, one_mul, zero_mul]
rw [hsumCohort, hsumTime]
simp [hg]
ring
The unit-and-time fixed-effect design as a finite linear map.
Definition (Lean source)
noncomputable def unitDesignMap (T N : ℕ) (G : Fin N → Cohort T) :
UnitParameter N T →ₗ[ℝ] (Fin N × Fin T → ℝ) :=
{ toFun := fun theta z => unitIndex T N (unitRegressor T N G z.1 z.2) theta
map_add' := by
intro x y
funext z
unfold unitIndex
simp [mul_add, Finset.sum_add_distrib]
ring
map_smul' := by
intro c x
funext z
unfold unitIndex
change (∑ j, _ * (c * x.1 j)) + _ * (c * x.2) =
c * ((∑ j, _ * x.1 j) + _ * x.2)
rw [mul_add, Finset.mul_sum]
congr 1
· apply Finset.sum_congr rfl
intro j hj
ring
· ring }
theorem unitDesignMap_injective
If every supported cohort occurs, collapsed full rank implies full column rank of the corresponding unit fixed-effect design.
Formal statement
hypotheses
T :
ℕ
N :
ℕ
hTop :
(⊤ : Cohort T) ∈ C
hT :
0 < T
hG :
∀ i, G i ∈ C
hCount :
∀ g ∈ C, 0 < cohortCount T G g
hRank :
CollapsedDesignRank T C pi
conclusion
Injective (unitDesignMap T N G)
Proof (Lean source)
lemma unitDesignMap_injective (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (pi : Cohort T → OpenUnit)
(hTop : (⊤ : Cohort T) ∈ C) (hT : 0 < T)
(hG : ∀ i, G i ∈ C) (hCount : ∀ g ∈ C, 0 < cohortCount T G g)
(hRank : CollapsedDesignRank T C pi) : Injective (unitDesignMap T N G) := by
classical
have hex (g : Cohort T) (hg : g ∈ C) : ∃ i, G i = g := by
have hc := hCount g hg
rw [cohortCount, Finset.card_pos] at hc
obtain ⟨i, hi⟩ := hc
exact ⟨i, (Finset.mem_filter.mp hi).2⟩
let rep : (g : Cohort T) → g ∈ C → Fin N := fun g hg => choose (hex g hg)
have hrep (g : Cohort T) (hg : g ∈ C) : G (rep g hg) = g :=
Classical.choose_spec (hex g hg)
intro x y hxy
have hmap : unitDesignMap T N G (x - y) = 0 := by
rw [map_sub, hxy, sub_self]
let d := x - y
let a : CollapsedParameter T C :=
(fun j => match j with
| inl _ => unitLevel T N d (rep ⊤ hTop)
| inr (inl c) =>
unitLevel T N d (rep c.1.1 c.1.2) - unitLevel T N d (rep ⊤ hTop)
| inr (inr t) => unitTimeLevel T N d t.1,
d.2)
have haIndex (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
collapsedIndex T C (collapsedRegressor T C g t) a = 0 := by
have hz := congrFun hmap (rep g hg, t)
change unitIndex T N (unitRegressor T N G (rep g hg) t) d = 0 at hz
rw [unitIndex_eq_levels, hrep g hg] at hz
rw [collapsedIndex_eq_levels T C a g hg t]
have hcohort : collapsedCohortLevel T C a g = unitLevel T N d (rep g hg) := by
by_cases hgt : g = ⊤
· subst g
simp [collapsedCohortLevel, a]
· simp [collapsedCohortLevel, a, hgt, hg]
have htime : collapsedTimeLevel T C a t = unitTimeLevel T N d t := by
by_cases ht : t.val = 0
· simp [collapsedTimeLevel, unitTimeLevel, ht]
· simp [collapsedTimeLevel, unitTimeLevel, ht, a]
rw [hcohort, htime]
exact hz
have ha : a = 0 := by
by_contra hane
have hr := hRank a hane
have hz : (∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) a) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
rw [haIndex g hg t]
simp
linarith
have hbeta : d.2 = 0 := congrArg snd ha
have htime (t : Fin T) : unitTimeLevel T N d t = 0 := by
by_cases ht : t.val = 0
· simp [unitTimeLevel, ht]
· have hj := congrFun (congrArg fst ha) (inr (inr ⟨t, ht⟩))
simpa [a, unitTimeLevel, ht] using hj
have hlevel (i : Fin N) : unitLevel T N d i = 0 := by
let t0 : Fin T := ⟨0, hT⟩
have hz := congrFun hmap (i, t0)
change unitIndex T N (unitRegressor T N G i t0) d = 0 at hz
rw [unitIndex_eq_levels] at hz
rw [hbeta, htime t0] at hz
simp at hz
exact hz
have hd : d = 0 := by
apply Prod.ext
· funext j
rcases j with (_ | j)
· have hN : 0 < N := by
obtain ⟨i, hi⟩ := hex ⊤ hTop
exact Nat.zero_lt_of_lt i.isLt
let i0 : Fin N := ⟨0, hN⟩
simpa [unitLevel, i0] using hlevel i0
· rcases j with (j | t)
· have hj := hlevel j.1
have hzero : d.1 (inl ()) = 0 := by
have hN : 0 < N := Nat.zero_lt_of_lt j.1.isLt
let i0 : Fin N := ⟨0, hN⟩
simpa [unitLevel, i0] using hlevel i0
simp [unitLevel, j.2, hzero] at hj
exact hj
· simpa [unitTimeLevel, t.2] using htime t.1
· exact hbeta
exact sub_eq_zero.mp hd
theorem unitCriterion_eq_finitePoissonObjective
The unit-level PPML criterion is exactly the finite Poisson objective with equal weight on each unit-period observation.
Formal statement
hypotheses
conclusion
unitCriterion T N G b gamma delta theta
= finitePoissonObjective (fun _ : Fin N × Fin T => (((N * T : ℕ) : ℝ)⁻¹)) (fun z : Fin N × Fin T => unitObservedMean T N G b gamma delta z.1 z.2) (unitDesignMap T N G) theta
Proof (Lean source)
lemma unitCriterion_eq_finitePoissonObjective (T N : ℕ)
(G : Fin N → Cohort T) (b : Fin N → PosReal) (gamma : Fin T → ℝ)
(delta : Cell T → ℝ) (theta : UnitParameter N T) :
unitCriterion T N G b gamma delta theta =
finitePoissonObjective
(fun _ : Fin N × Fin T => (((N * T : ℕ) : ℝ)⁻¹))
(fun z : Fin N × Fin T => unitObservedMean T N G b gamma delta z.1 z.2)
(unitDesignMap T N G) theta := by
rw [unitCriterion, finitePoissonObjective, Fintype.sum_prod_type]
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.mul_sum]
rfl
A collapsed parameter can be lifted to unit fixed effects by adding each unit's log baseline ratio within its cohort.
Definition (Lean source)
noncomputable def liftCollapsedParameter (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal) (hN : 0 < N)
(theta : CollapsedParameter T C) : UnitParameter N T :=
let i0 : Fin N := ⟨0, hN⟩
let r : Fin N → ℝ := fun i =>
log ((b i : ℝ) / withinCohortBaseline T G b (G i)) +
collapsedCohortLevel T C theta (G i)
(fun j => match j with
| inl _ => r i0
| inr (inl i) => r i.1 - r i0
| inr (inr t) => collapsedTimeLevel T C theta t.1,
theta.2)
theorem unitIndex_liftCollapsedParameter
Lifting a collapsed cohort-time parameter into unit-and-time fixed effects reproduces the collapsed linear index at every unit-period observation, shifted by the log ratio of that unit's baseline to the average baseline of its cohort. Every unit is assumed to belong to a supported cohort.
Formal statement
hypotheses
conclusion
= log ((b i : ℝ) / withinCohortBaseline T G b (G i))
+ collapsedIndex T C (collapsedRegressor T C (G i) t) theta
Proof (Lean source)
lemma unitIndex_liftCollapsedParameter (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal) (hN : 0 < N)
(hG : ∀ i, G i ∈ C) (theta : CollapsedParameter T C) (i : Fin N) (t : Fin T) :
unitIndex T N (unitRegressor T N G i t)
(liftCollapsedParameter T C G b hN theta) =
log ((b i : ℝ) / withinCohortBaseline T G b (G i)) +
collapsedIndex T C (collapsedRegressor T C (G i) t) theta := by
classical
rw [unitIndex_eq_levels, collapsedIndex_eq_levels T C theta (G i) (hG i) t]
have hlevel : unitLevel T N (liftCollapsedParameter T C G b hN theta) i =
log ((b i : ℝ) / withinCohortBaseline T G b (G i)) +
collapsedCohortLevel T C theta (G i) := by
by_cases hi : i.val = 0
· have hii : i = ⟨0, hN⟩ := Fin.ext hi
subst i
simp [unitLevel, liftCollapsedParameter]
· simp [unitLevel, liftCollapsedParameter, hi]
have htime : unitTimeLevel T N (liftCollapsedParameter T C G b hN theta) t =
collapsedTimeLevel T C theta t := by
by_cases ht : t.val = 0
· simp [unitTimeLevel, collapsedTimeLevel, ht]
· simp [unitTimeLevel, collapsedTimeLevel, liftCollapsedParameter, ht]
rw [hlevel, htime]
simp [liftCollapsedParameter]
ring
Baseline ratios sum to the cohort count.
Formal statement
hypotheses
conclusion
Proof (Lean source)
lemma sum_baselineRatio_within_cohort (T : ℕ) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal) (g : Cohort T)
(hCount : 0 < cohortCount T G g) :
∑ i ∈ cohortIndexSet T G g,
(b i : ℝ) / withinCohortBaseline T G b g = cohortCount T G g := by
have hspos : 0 < ∑ i ∈ cohortIndexSet T G g, (b i : ℝ) := by
apply Finset.sum_pos'
· intro i hi
exact (b i).property.le
· rw [cohortCount] at hCount
obtain ⟨i, hi⟩ := Finset.card_pos.mp hCount
exact ⟨i, by simpa [cohortIndexSet] using hi, (b i).property⟩
rw [withinCohortBaseline, ← Finset.sum_div]
have hc : (cohortCount T G g : ℝ) ≠ 0 := ne_of_gt (Nat.cast_pos.mpr hCount)
field_simp
A weighted sum over units whose summand is cohort-constant collapses to a count-weighted sum over supported cohorts.
Formal statement
Proof (Lean source)
lemma sum_baselineRatio_fiberwise (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal)
(hG : ∀ i, G i ∈ C) (hCount : ∀ g ∈ C, 0 < cohortCount T G g)
(f : Cohort T → ℝ) :
∑ i, ((b i : ℝ) / withinCohortBaseline T G b (G i)) * f (G i) =
∑ g ∈ C, (cohortCount T G g : ℝ) * f g := by
classical
calc
∑ i, ((b i : ℝ) / withinCohortBaseline T G b (G i)) * f (G i) =
∑ g ∈ C, ∑ i ∈ cohortIndexSet T G g,
((b i : ℝ) / withinCohortBaseline T G b g) * f g := by
simp_rw [cohortIndexSet, Finset.sum_filter]
rw [Finset.sum_comm]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.sum_eq_single (G i)]
· simp [hG i]
· intro g hg hne
rw [if_neg (fun heq => hne heq.symm)]
· intro hnot
exact (hnot (hG i)).elim
_ = _ := by
apply Finset.sum_congr rfl
intro g hg
rw [← Finset.sum_mul]
congr 1
exact sum_baselineRatio_within_cohort T G b g (hCount g hg)
Summing any quantity over units equals summing it first within each supported adoption cohort and then across cohorts.
Formal statement
Proof (Lean source)
lemma sum_units_by_supported_cohort (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (hG : ∀ i, G i ∈ C) (f : Fin N → ℝ) :
∑ i, f i = ∑ g ∈ C, ∑ i ∈ cohortIndexSet T G g, f i := by
classical
simp_rw [cohortIndexSet, Finset.sum_filter]
rw [Finset.sum_comm]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.sum_eq_single (G i)]
· simp [hG i]
· intro g hg hne
rw [if_neg (fun heq => hne heq.symm)]
· intro hnot
exact (hnot (hG i)).elim
An arbitrary unit-level parameter direction can be collapsed by taking baseline-ratio-weighted averages of unit fixed-effect levels within each cohort.
Definition (Lean source)
noncomputable def aggregateUnitDirection (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal) (hTop : (⊤ : Cohort T) ∈ C)
(d : UnitParameter N T) : CollapsedParameter T C :=
let level : (g : Cohort T) → g ∈ C → ℝ := fun g _ =>
(cohortCount T G g : ℝ)⁻¹ *
∑ i ∈ cohortIndexSet T G g,
((b i : ℝ) / withinCohortBaseline T G b g) * unitLevel T N d i
(fun j => match j with
| inl _ => level ⊤ hTop
| inr (inl c) => level c.1.1 c.1.2 - level ⊤ hTop
| inr (inr t) => unitTimeLevel T N d t.1,
d.2)
theorem collapsedIndex_aggregateUnitDirection
Aggregating a unit-and-time direction into collapsed coordinates gives, at every supported cohort-time cell, the baseline-ratio-weighted within-cohort average of the unit levels, plus the direction's time effect for that period, plus its treatment coefficient times the cohort's treatment indicator.
Formal statement
hypotheses
conclusion
= (cohortCount T G g : ℝ)⁻¹ * ∑ i ∈ cohortIndexSet T G g, ((b i : ℝ) / withinCohortBaseline T G b g) * unitLevel T N d i
+ unitTimeLevel T N d t
+ d.2 * treatmentIndicator T g t
Proof (Lean source)
lemma collapsedIndex_aggregateUnitDirection (T : ℕ) (C : Finset (Cohort T))
{N : ℕ} (G : Fin N → Cohort T) (b : Fin N → PosReal)
(hTop : (⊤ : Cohort T) ∈ C) (d : UnitParameter N T)
(g : Cohort T) (hg : g ∈ C) (t : Fin T) :
collapsedIndex T C (collapsedRegressor T C g t)
(aggregateUnitDirection T C G b hTop d) =
(cohortCount T G g : ℝ)⁻¹ *
∑ i ∈ cohortIndexSet T G g,
((b i : ℝ) / withinCohortBaseline T G b g) * unitLevel T N d i +
unitTimeLevel T N d t + d.2 * treatmentIndicator T g t := by
classical
rw [collapsedIndex_eq_levels T C _ g hg t]
have hc : collapsedCohortLevel T C (aggregateUnitDirection T C G b hTop d) g =
(cohortCount T G g : ℝ)⁻¹ *
∑ i ∈ cohortIndexSet T G g,
((b i : ℝ) / withinCohortBaseline T G b g) * unitLevel T N d i := by
by_cases hgt : g = ⊤
· subst g
simp [collapsedCohortLevel, aggregateUnitDirection]
· simp [collapsedCohortLevel, aggregateUnitDirection, hgt, hg]
have ht : collapsedTimeLevel T C (aggregateUnitDirection T C G b hTop d) t =
unitTimeLevel T N d t := by
by_cases htz : t.val = 0
· simp [collapsedTimeLevel, unitTimeLevel, htz]
· simp [collapsedTimeLevel, unitTimeLevel, aggregateUnitDirection, htz]
rw [hc, ht]
rfl
theorem unitResidual_liftCollapsedParameter
At a lifted parameter, a unit residual is its baseline ratio times the corresponding collapsed cell residual.
Formal statement
hypotheses
T :
ℕ
N :
ℕ
hN :
0 < N
hG :
∀ i, G i ∈ C
hCount :
∀ g ∈ C, 0 < cohortCount T G g
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
theta :
i :
Fin N
t :
Fin T
conclusion
unitObservedMean T N G b gamma delta i t
= ((b i : ℝ) / withinCohortBaseline T G b (G i)) * (finiteObservedCohortMean T G b gamma delta (G i) t - exp (collapsedIndex T C (collapsedRegressor T C (G i) t) theta))
Proof (Lean source)
lemma unitResidual_liftCollapsedParameter (T : ℕ) (C : Finset (Cohort T))
{N : ℕ} (G : Fin N → Cohort T) (b : Fin N → PosReal) (hN : 0 < N)
(hG : ∀ i, G i ∈ C) (hCount : ∀ g ∈ C, 0 < cohortCount T G g)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(theta : CollapsedParameter T C) (i : Fin N) (t : Fin T) :
unitObservedMean T N G b gamma delta i t -
exp (unitIndex T N (unitRegressor T N G i t)
(liftCollapsedParameter T C G b hN theta)) =
((b i : ℝ) / withinCohortBaseline T G b (G i)) *
(finiteObservedCohortMean T G b gamma delta (G i) t -
exp (collapsedIndex T C (collapsedRegressor T C (G i) t) theta)) := by
rw [unitIndex_liftCollapsedParameter T C G b hN hG]
have hb := withinCohortBaseline_pos T G b (G i) (hCount (G i) (hG i))
have hratio : 0 < (b i : ℝ) / withinCohortBaseline T G b (G i) :=
div_pos (b i).property hb
rw [Real.exp_add, Real.exp_log hratio]
unfold unitObservedMean finiteObservedCohortMean finiteUntreatedMean unitTreatment
rw [Real.exp_add]
field_simp [ne_of_gt hb]
theorem unitScore_eq_collapsedScore
The score of a lifted collapsed parameter in any unit direction equals the collapsed score in the baseline-ratio-aggregated direction.
Formal statement
hypotheses
T :
ℕ
N :
ℕ
hN :
0 < N
hT :
0 < T
hTop :
(⊤ : Cohort T) ∈ C
hG :
∀ i, G i ∈ C
hCount :
∀ g ∈ C, 0 < cohortCount T G g
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
theta :
d :
UnitParameter N T
conclusion
∑ z : Fin N × Fin T, (((N * T : ℕ) : ℝ)⁻¹) * unitDesignMap T N G d z * (unitObservedMean T N G b gamma delta z.1 z.2 - exp (unitDesignMap T N G (liftCollapsedParameter T C G b hN theta) z))
= ∑ z : SupportedCell T C, finiteCellMass T G z.1.1 * collapsedDesignMap T C (aggregateUnitDirection T C G b hTop d) z * (finiteObservedCohortMean T G b gamma delta z.1.1 z.2 - exp (collapsedDesignMap T C theta z))
Proof (Lean source)
lemma unitScore_eq_collapsedScore (T : ℕ) (C : Finset (Cohort T)) {N : ℕ}
(G : Fin N → Cohort T) (b : Fin N → PosReal) (hN : 0 < N) (hT : 0 < T)
(hTop : (⊤ : Cohort T) ∈ C) (hG : ∀ i, G i ∈ C)
(hCount : ∀ g ∈ C, 0 < cohortCount T G g)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(theta : CollapsedParameter T C) (d : UnitParameter N T) :
∑ z : Fin N × Fin T,
(((N * T : ℕ) : ℝ)⁻¹) * unitDesignMap T N G d z *
(unitObservedMean T N G b gamma delta z.1 z.2 -
exp (unitDesignMap T N G
(liftCollapsedParameter T C G b hN theta) z)) =
∑ z : SupportedCell T C,
finiteCellMass T G z.1.1 *
collapsedDesignMap T C (aggregateUnitDirection T C G b hTop d) z *
(finiteObservedCohortMean T G b gamma delta z.1.1 z.2 -
exp (collapsedDesignMap T C theta z)) := by
classical
let R : Cohort T → Fin T → ℝ := fun g t =>
finiteObservedCohortMean T G b gamma delta g t -
exp (collapsedIndex T C (collapsedRegressor T C g t) theta)
have hinner (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
∑ i ∈ cohortIndexSet T G g,
(((b i : ℝ) / withinCohortBaseline T G b g) *
unitIndex T N (unitRegressor T N G i t) d * R g t) =
(cohortCount T G g : ℝ) *
collapsedIndex T C (collapsedRegressor T C g t)
(aggregateUnitDirection T C G b hTop d) * R g t := by
have hc0 : (cohortCount T G g : ℝ) ≠ 0 :=
ne_of_gt (Nat.cast_pos.mpr (hCount g hg))
have hratio := sum_baselineRatio_within_cohort T G b g (hCount g hg)
rw [collapsedIndex_aggregateUnitDirection T C G b hTop d g hg t]
simp_rw [unitIndex_eq_levels]
have hGi : ∀ i ∈ cohortIndexSet T G g, G i = g := by
intro i hi
exact (Finset.mem_filter.mp hi).2
have hreplace : (∑ i ∈ cohortIndexSet T G g,
((b i : ℝ) / withinCohortBaseline T G b g) *
(unitLevel T N d i + unitTimeLevel T N d t +
d.2 * treatmentIndicator T (G i) t) * R g t) =
∑ i ∈ cohortIndexSet T G g,
((b i : ℝ) / withinCohortBaseline T G b g) *
(unitLevel T N d i + unitTimeLevel T N d t +
d.2 * treatmentIndicator T g t) * R g t := by
apply Finset.sum_congr rfl
intro i hi
rw [hGi i hi]
rw [hreplace]
simp_rw [mul_add, add_mul, Finset.sum_add_distrib, ← Finset.sum_mul]
rw [hratio]
field_simp
rw [Fintype.sum_prod_type, Fintype.sum_prod_type]
have sum_supported (f : {g : Cohort T // g ∈ C} → ℝ) :
(∑ g, f g) = ∑ g ∈ C.attach, f g := by
rw [show (Finset.univ : Finset {g : Cohort T // g ∈ C}) = C.attach by
ext g
simp]
rw [sum_supported]
simp only [unitDesignMap, collapsedDesignMap]
change (∑ i, ∑ t, (((N * T : ℕ) : ℝ)⁻¹) *
unitIndex T N (unitRegressor T N G i t) d *
(unitObservedMean T N G b gamma delta i t -
exp (unitIndex T N (unitRegressor T N G i t)
(liftCollapsedParameter T C G b hN theta)))) = _
simp_rw [unitResidual_liftCollapsedParameter T C G b hN hG hCount gamma delta theta]
change (∑ i, ∑ t, (((N * T : ℕ) : ℝ)⁻¹) *
unitIndex T N (unitRegressor T N G i t) d *
(((b i : ℝ) / withinCohortBaseline T G b (G i)) * R (G i) t)) = _
simp_rw [mul_assoc]
rw [Finset.sum_comm]
rw [Finset.sum_comm (s := C.attach) (t := Finset.univ)]
apply Finset.sum_congr rfl
intro t ht
rw [sum_units_by_supported_cohort T C G hG]
rw [← Finset.sum_attach]
apply Finset.sum_congr rfl
intro g hg
have hGi : ∀ i ∈ cohortIndexSet T G g.1, G i = g.1 := by
intro i hi
exact (Finset.mem_filter.mp hi).2
have hNT : (((N * T : ℕ) : ℝ)) ≠ 0 := by
exact_mod_cast (Nat.mul_ne_zero (ne_of_gt hN) (ne_of_gt hT))
calc
(∑ i ∈ cohortIndexSet T G g.1, (((N * T : ℕ) : ℝ)⁻¹) *
(unitIndex T N (unitRegressor T N G i t) d *
((b i : ℝ) / withinCohortBaseline T G b (G i) * R (G i) t))) =
(((N * T : ℕ) : ℝ)⁻¹) *
∑ i ∈ cohortIndexSet T G g.1,
((b i : ℝ) / withinCohortBaseline T G b g.1) *
unitIndex T N (unitRegressor T N G i t) d * R g.1 t := by
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro i hi
rw [hGi i hi]
ring
_ = (((N * T : ℕ) : ℝ)⁻¹) *
((cohortCount T G g.1 : ℝ) *
collapsedIndex T C (collapsedRegressor T C g.1 t)
(aggregateUnitDirection T C G b hTop d) * R g.1 t) := by
rw [hinner g.1 g.2 t]
_ = _ := by
unfold finiteCellMass
dsimp [collapsedDesignMap, R]
rw [Nat.cast_mul]
field_simp
theorem finite_unit_and_collapsed_unique_beta
At every finite array with positive supported counts, the unique unit-FE and collapsed maximizers have exactly the same treatment coordinate.
Formal statement
hypotheses
T :
ℕ
N :
ℕ
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hN :
0 < N
hT :
0 < T
hC :
C.Nonempty
hTop :
(⊤ : Cohort T) ∈ C
hG :
∀ i, G i ∈ C
hCount :
∀ g ∈ C, 0 < cohortCount T G g
hRank :
CollapsedDesignRank T C pi
conclusion
IsUniqueGlobalMax (unitCriterion T N G b gamma delta) (maximizerOrZero (unitCriterion T N G b gamma delta)) ∧
IsUniqueGlobalMax (finiteCollapsedCriterion T C G b gamma delta) (maximizerOrZero (finiteCollapsedCriterion T C G b gamma delta)) ∧
(maximizerOrZero (unitCriterion T N G b gamma delta)).2
= (maximizerOrZero (finiteCollapsedCriterion T C G b gamma delta)).2
Proof (Lean source)
lemma finite_unit_and_collapsed_unique_beta (T : ℕ) (C : Finset (Cohort T))
{N : ℕ} (G : Fin N → Cohort T) (b : Fin N → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(pi : Cohort T → OpenUnit) (hN : 0 < N) (hT : 0 < T) (hC : C.Nonempty)
(hTop : (⊤ : Cohort T) ∈ C) (hG : ∀ i, G i ∈ C)
(hCount : ∀ g ∈ C, 0 < cohortCount T G g)
(hRank : CollapsedDesignRank T C pi) :
IsUniqueGlobalMax (unitCriterion T N G b gamma delta)
(maximizerOrZero (unitCriterion T N G b gamma delta)) ∧
IsUniqueGlobalMax (finiteCollapsedCriterion T C G b gamma delta)
(maximizerOrZero (finiteCollapsedCriterion T C G b gamma delta)) ∧
(maximizerOrZero (unitCriterion T N G b gamma delta)).2 =
(maximizerOrZero (finiteCollapsedCriterion T C G b gamma delta)).2 := by
classical
let fc := finiteCollapsedCriterion T C G b gamma delta
obtain ⟨theta, htheta, hthetaUnique⟩ :=
finiteCollapsedCriterion_exists_unique_max T C G b gamma delta pi hT hC hCount hRank
have hcUnique : IsUniqueGlobalMax fc (maximizerOrZero fc) :=
uniqueGlobalMax_maximizerOrZero fc ⟨theta, htheta, hthetaUnique⟩
have hcsel : maximizerOrZero fc = theta := by
exact hthetaUnique _ hcUnique.1
let q : Fin N × Fin T → ℝ := fun _ => (((N * T : ℕ) : ℝ)⁻¹)
let m : Fin N × Fin T → ℝ := fun z =>
unitObservedMean T N G b gamma delta z.1 z.2
let A := unitDesignMap T N G
let lifted := liftCollapsedParameter T C G b hN theta
have hqpos : ∀ z, 0 < q z := by
intro z
exact inv_pos.mpr (Nat.cast_pos.mpr (Nat.mul_pos hN hT))
have hmpos : ∀ z, 0 < m z := by
intro z
exact mul_pos (b z.1).property (Real.exp_pos _)
letI : Nonempty (Fin N × Fin T) := ⟨(⟨0, hN⟩, ⟨0, hT⟩)⟩
have hcollapsedScore (a : CollapsedParameter T C) :
∑ z : SupportedCell T C,
finiteCellMass T G z.1.1 * collapsedDesignMap T C a z *
(finiteObservedCohortMean T G b gamma delta z.1.1 z.2 -
exp (collapsedDesignMap T C theta z)) = 0 := by
apply finitePoissonObjective_score
intro eta
simpa only [← finiteCollapsedCriterion_eq_finitePoissonObjective] using htheta eta
have hunitScore (d : UnitParameter N T) :
∑ z, q z * A d z * (m z - exp (A lifted z)) = 0 := by
rw [unitScore_eq_collapsedScore T C G b hN hT hTop hG hCount gamma delta theta d]
exact hcollapsedScore (aggregateUnitDirection T C G b hTop d)
have hliftMaxObj : ∀ eta, finitePoissonObjective q m A eta ≤
finitePoissonObjective q m A lifted :=
finitePoissonObjective_isMax_of_score q m A lifted
(fun z => (hqpos z).le) hunitScore
have hliftMax : ∀ eta, unitCriterion T N G b gamma delta eta ≤
unitCriterion T N G b gamma delta lifted := by
intro eta
simpa only [unitCriterion_eq_finitePoissonObjective] using hliftMaxObj eta
obtain ⟨ustar, hustar, huunique⟩ := finitePoissonObjective_exists_unique_max
q m A hqpos hmpos (unitDesignMap_injective T C G pi hTop hT hG hCount hRank)
have hulift : ustar = lifted := by
exact (huunique lifted hliftMaxObj).symm
have huExistsUnique : ∃! u, ∀ eta, unitCriterion T N G b gamma delta eta ≤
unitCriterion T N G b gamma delta u := by
refine ⟨lifted, hliftMax, ?_⟩
intro u hu
have huobj : ∀ eta, finitePoissonObjective q m A eta ≤
finitePoissonObjective q m A u := by
intro eta
simpa only [q, m, A, unitCriterion_eq_finitePoissonObjective] using hu eta
calc
u = ustar := huunique u huobj
_ = lifted := hulift
have huUnique := uniqueGlobalMax_maximizerOrZero
(unitCriterion T N G b gamma delta) huExistsUnique
refine ⟨huUnique, hcUnique, ?_⟩
have husel : maximizerOrZero (unitCriterion T N G b gamma delta) = lifted := by
exact huExistsUnique.unique huUnique.1 hliftMax
rw [husel, hcsel]
rfl
theorem selectedFiniteCollapsed_tendsto
The selected finite collapsed projections converge to the limiting collapsed projection under the paper's share and baseline limits.
Formal statement
hypotheses
T :
ℕ
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hHorizon :
hSupport :
hShare :
CohortShareLimit T C G pi
hBaseline :
WithinCohortBaselineLimit T C G b barB
hRank :
CollapsedDesignRank T C pi
conclusion
Tendsto (fun N => maximizerOrZero (finiteCollapsedCriterion T C (G N) (b N) gamma delta)) atTop (nhds (collapsedPopulationProjection T C pi barB gamma delta))
Proof (Lean source)
lemma selectedFiniteCollapsed_tendsto (T : ℕ) (C : Finset (Cohort T))
(G : ∀ N, Fin N → Cohort T) (b : ∀ N, Fin N → PosReal)
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(hHorizon : ValidPanelHorizon T) (hSupport : ValidCohortSupport T C)
(hShare : CohortShareLimit T C G pi)
(hBaseline : WithinCohortBaselineLimit T C G b barB)
(hRank : CollapsedDesignRank T C pi) :
Tendsto
(fun N => maximizerOrZero (finiteCollapsedCriterion T C (G N) (b N) gamma delta))
atTop (nhds (collapsedPopulationProjection T C pi barB gamma delta)) := by
classical
have hT : 0 < T := lt_of_lt_of_le (by norm_num) hHorizon
have hC : C.Nonempty := ⟨⊤, hSupport.1⟩
let qN : ℕ → SupportedCell T C → ℝ := fun N z =>
finiteCellMass T (G N) z.1.1
let mN : ℕ → SupportedCell T C → ℝ := fun N z =>
finiteObservedCohortMean T (G N) (b N) gamma delta z.1.1 z.2
let q : SupportedCell T C → ℝ := fun z => limitingCellMass T pi z.1.1
let m : SupportedCell T C → ℝ := fun z =>
observedCohortMean T barB gamma delta z.1.1 z.2
let A := collapsedDesignMap T C
let arg : ℕ → CollapsedParameter T C := fun N =>
maximizerOrZero (finiteCollapsedCriterion T C (G N) (b N) gamma delta)
let lim := collapsedPopulationProjection T C pi barB gamma delta
have hqpos : ∀ z, 0 < q z := by
intro z
exact div_pos (pi z.1.1).property.1 (Nat.cast_pos.mpr hT)
have hmpos : ∀ z, 0 < m z := by
intro z
exact mul_pos (mul_pos (barB z.1.1).property (Real.exp_pos _)) (Real.exp_pos _)
have hqconv : ∀ z, Tendsto (fun N => qN N z) atTop (nhds (q z)) := by
intro z
have hs := hShare.2 z.1.1 z.1.2
have hd := hs.div_const (T : ℝ)
apply hd.congr'
filter_upwards [Filter.eventually_ge_atTop 1] with N hN
dsimp [qN, q]
unfold finiteCellMass cohortShare
have hN0 : (N : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hN)
have hT0 : (T : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hT)
norm_num [Nat.cast_mul]
field_simp
have hmconv : ∀ z, Tendsto (fun N => mN N z) atTop (nhds (m z)) := by
intro z
have hb := hBaseline z.1.1 z.1.2
have hh := (hb.mul_const (exp (gamma z.2))).mul_const
(exp (treatmentIndicator T z.1.1 z.2 * delta (z.1.1, z.2)))
simpa [mN, m, finiteObservedCohortMean, finiteUntreatedMean,
observedCohortMean, untreatedMean, mul_assoc] using hh
have hargmax : ∀ᶠ N in atTop, ∀ y,
finitePoissonObjective (qN N) (mN N) A y ≤
finitePoissonObjective (qN N) (mN N) A (arg N) := by
filter_upwards [Filter.eventually_ge_atTop C.card] with N hcard
have hcounts := (hShare.1 N hcard).2
have hu := finiteCollapsedCriterion_exists_unique_max T C (G N) (b N) gamma delta
pi hT hC hcounts hRank
have hs := uniqueGlobalMax_maximizerOrZero
(finiteCollapsedCriterion T C (G N) (b N) gamma delta) hu
intro y
simpa only [finiteCollapsedCriterion_eq_finitePoissonObjective] using hs.1 y
have hlimit : IsUniqueGlobalMax (finitePoissonObjective q m A) lim := by
have hp := (pseudo_true_ppml_projection T C pi barB gamma delta hRank).1
constructor
· intro y
simpa only [q, m, A, lim, limitingCriterion_eq_finitePoissonObjective] using hp.1 y
· intro y hy
apply hp.2 y
simpa only [q, m, A, lim, limitingCriterion_eq_finitePoissonObjective] using hy
exact finitePoissonObjective_argmax_tendsto qN mN q m A arg lim hqpos hmpos
(collapsedDesignMap_injective T C pi hRank) hqconv hmconv hargmax hlimit
Helpers.Frontier 22 declarations This file defines the all-positive sign-reversal region, the concrete four-cohort fixture, and the row/column-margin elimination polynomial Phi.
Primitive sign-frontier constructions
This file defines the all-positive sign-reversal region, the concrete
four-cohort fixture, and the row/column-margin elimination polynomial Phi.
def TreatedSupportedCell
Treated cells within the declared cohort support.
Definition (Lean source)
abbrev TreatedSupportedCell (T : ℕ) (C : Finset (Cohort T)) :=
{z : SupportedCell T C // treatmentIndicator T z.1.1 z.2 = 1}
def SignReversalPrimitive
Primitive tuples indexed only by the paper's declared cohort and cell domains.
Definition (Lean source)
abbrev SignReversalPrimitive (T : ℕ) (C : Finset (Cohort T)) :=
(↑C → OpenUnit) ×
((SupportedCell T C → PosReal) × (TreatedSupportedCell T C → ℝ))
def primitiveLimitingCriterion
The collapsed PPML objective written directly in the C-indexed primitive coordinates.
Definition (Lean source)
noncomputable def primitiveLimitingCriterion (T : ℕ) (C : Finset (Cohort T))
(p : SignReversalPrimitive T C) (theta : CollapsedParameter T C) : ℝ :=
∑ z : SupportedCell T C,
((p.1 z.1 : ℝ) / T) *
((p.2.1 z : ℝ) *
exp (treatmentIndicator T z.1.1 z.2 *
if h : treatmentIndicator T z.1.1 z.2 = 1
then p.2.2 ⟨z, h⟩ else 0) *
collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) theta -
exp (collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) theta))
def primitiveBetaStar
Treatment coordinate selected by the primitive collapsed objective.
Definition (Lean source)
noncomputable def primitiveBetaStar (T : ℕ) (C : Finset (Cohort T))
(p : SignReversalPrimitive T C) : ℝ :=
(maximizerOrZero (primitiveLimitingCriterion T C p)).2
def restrictSignReversalPrimitive
Restrict full-array primitives to exactly the coordinates declared in R_T.
Definition (Lean source)
noncomputable def restrictSignReversalPrimitive (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) : SignReversalPrimitive T C :=
(fun g => pi g.1,
(fun z => ⟨untreatedMean T barB gamma z.1.1 z.2,
mul_pos (barB z.1.1).property (Real.exp_pos _)⟩,
fun z => delta (z.1.1.1, z.1.2)))
The all-positive-effect PPML sign-reversal region R_T.
Definition (Lean source)
noncomputable def signReversalRegion (T : ℕ) (C : Finset (Cohort T))
(gamma : Fin T → ℝ) : Set (SignReversalPrimitive T C) :=
{p | ValidPanelHorizon T ∧
ValidCohortSupport T C ∧
MulticohortFrontierScope T C ∧
(∑ g : ↑C, (p.1 g : ℝ)) = 1 ∧
(∃ barB : ↑C → PosReal, ∀ z : SupportedCell T C,
(p.2.1 z : ℝ) = (barB z.1 : ℝ) * exp (gamma z.2)) ∧
(∀ z : TreatedSupportedCell T C, 0 < p.2.2 z) ∧
(∀ a : CollapsedParameter T C, a ≠ 0 →
0 < ∑ z : SupportedCell T C,
((p.1 z.1 : ℝ) / T) *
(collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) a) ^ 2) ∧
primitiveBetaStar T C p < 0}
def fourCohortSupport
Four adoption cohorts: paper dates 2, 3, 4, and never treated.
def fourCohortCount
Equal cohort counts along the cofinal sequence N = 4(m+1).
Definition (Lean source)
theorem fourCohortCount_pos
Every cohort in the declared four-cohort support has positive count.
Formal statement
Proof (Lean source)
lemma fourCohortCount_pos (m : ℕ) (g : Cohort 4) (hg : g ∈ fourCohortSupport) :
0 < fourCohortCount m g := by
simp [fourCohortCount, hg]
def fourCohortBaseline
Unit baselines are identically one in the fixture.
Definition (Lean source)
def fourCohortGamma
Untreated time effects are identically zero in the fixture.
Definition (Lean source)
def fourCohortGamma (_t : Fin 4) : ℝ := 0
def fourCohortDelta
The W4 effect vector: log(4) at paper cell (2,4), and log(101/100) elsewhere treated.
Definition (Lean source)
noncomputable def fourCohortDelta (z : Cell 4) : ℝ :=
if treatmentIndicator 4 z.1 z.2 = 1 then
if z.1 = (⟨1, by decide⟩ : Fin 4) ∧ z.2 = ⟨3, by decide⟩ then
log 4
else log (101 / 100 : ℝ)
else 0
def fourCohortLimitBaseline
Unit limiting cohort baselines in W4.
Definition (Lean source)
def FourCohortConfiguration
The data specifying a four-period triangular-array configuration: a cohort support, the cohort counts along the array, the unit baselines at each array size, the untreated time effects, and the cohort-time log proportional effects. The paper's explicit counterexample world is a single element of this type.
The concrete four-cohort triangular-array configuration W4.
Definition (Lean source)
noncomputable def fourCohortWitness : FourCohortConfiguration :=
(fourCohortSupport,
(fourCohortCount,
(fourCohortBaseline, (fourCohortGamma, fourCohortDelta))))
def primitiveH
Primitive positive cell mass before division by the common time factor.
Definition (Lean source)
noncomputable def primitiveH (T : ℕ) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (t : Fin T) : ℝ :=
(pi g : ℝ) * untreatedMean T barB gamma g t *
exp (treatmentIndicator T g t * delta (g, t))
def primitiveRow
Row margin R_g.
Definition (Lean source)
noncomputable def primitiveRow (T : ℕ) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) : ℝ :=
∑ t : Fin T, primitiveH T pi barB gamma delta g t
def primitiveColumn
Column margin C_t.
def primitiveTotal
Total primitive mass M.
Definition (Lean source)
noncomputable def primitiveTotal (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) : ℝ :=
∑ g ∈ C, primitiveRow T pi barB gamma delta g
def primitiveTreatedTotal
Treated primitive total A.
Definition (Lean source)
noncomputable def primitiveTreatedTotal (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) : ℝ :=
∑ g ∈ C, ∑ t : Fin T,
treatmentIndicator T g t * primitiveH T pi barB gamma delta g t
The nuisance-free frontier polynomial Phi = M*A - sum D_gt R_g C_t.
Definition (Lean source)
noncomputable def frontierEliminationHandle (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) : ℝ :=
primitiveTotal T C pi barB gamma delta *
primitiveTreatedTotal T C pi barB gamma delta -
∑ g ∈ C, ∑ t : Fin T,
treatmentIndicator T g t * primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t
Helpers.FrontierSign 18 declarations Algebra connecting the primitive margin frontier to the conditional Poisson score.
Algebra connecting the primitive margin frontier to the conditional Poisson score.
Every primitive cohort-period mass is strictly positive.
Formal statement
Proof (Lean source)
lemma frontierPrimitiveH_pos (T : ℕ) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (t : Fin T) :
0 < primitiveH T pi barB gamma delta g t := by
exact mul_pos
(mul_pos (pi g).property.1
(mul_pos (barB g).property (Real.exp_pos (gamma t))))
(Real.exp_pos _)
The primitive mass summed over all periods is strictly positive for every cohort.
Formal statement
Proof (Lean source)
lemma frontierPrimitiveRow_pos (T : ℕ) (hT : 0 < T) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) : 0 < primitiveRow T pi barB gamma delta g := by
unfold primitiveRow
apply Finset.sum_pos'
· intro t _
exact (frontierPrimitiveH_pos T pi barB gamma delta g t).le
· exact ⟨⟨0, hT⟩, Finset.mem_univ _,
frontierPrimitiveH_pos T pi barB gamma delta g ⟨0, hT⟩⟩
The primitive mass summed over supported cohorts is strictly positive in every period.
Formal statement
Proof (Lean source)
lemma frontierPrimitiveColumn_pos (T : ℕ) (C : Finset (Cohort T))
(hC : C.Nonempty) (pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) (t : Fin T) :
0 < primitiveColumn T C pi barB gamma delta t := by
unfold primitiveColumn
apply Finset.sum_pos'
· intro g hg
exact (frontierPrimitiveH_pos T pi barB gamma delta g t).le
· obtain ⟨g, hg⟩ := hC
exact ⟨g, hg, frontierPrimitiveH_pos T pi barB gamma delta g t⟩
The total primitive mass over all supported cohort-period cells is strictly positive.
Formal statement
Proof (Lean source)
lemma frontierPrimitiveTotal_pos (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
0 < primitiveTotal T C pi barB gamma delta := by
unfold primitiveTotal
apply Finset.sum_pos'
· intro g hg
exact (frontierPrimitiveRow_pos T hT pi barB gamma delta g).le
· obtain ⟨g, hg⟩ := hC
exact ⟨g, hg, frontierPrimitiveRow_pos T hT pi barB gamma delta g⟩
Adding the period-specific primitive masses yields the total primitive mass.
Formal statement
hypotheses
conclusion
(∑ t, primitiveColumn T C pi barB gamma delta t) = primitiveTotal T C pi barB gamma delta
Proof (Lean source)
lemma frontierPrimitiveColumn_sum (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
(∑ t, primitiveColumn T C pi barB gamma delta t) =
primitiveTotal T C pi barB gamma delta := by
classical
unfold primitiveColumn primitiveTotal primitiveRow
rw [Finset.sum_comm]
The beta-zero fixed-effects parameter matches primitive row and column margins through a normalized row-column construction.
Definition (Lean source)
noncomputable def frontierNuisanceParameter (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
CollapsedParameter T C :=
let rowLog := fun g => log (primitiveRow T pi barB gamma delta g / (pi g : ℝ))
let columnLog := fun t => log (primitiveColumn T C pi barB gamma delta t)
let totalLog := log (primitiveTotal T C pi barB gamma delta)
((fun j => match j with
| inl _ => rowLog ⊤ + columnLog ⟨0, hT⟩ - totalLog
| inr (inl g) => rowLog g.1.1 - rowLog ⊤
| inr (inr t) => columnLog t.1 - columnLog ⟨0, hT⟩), 0)
theorem frontierNuisanceParameter_index
At the zero-treatment-coefficient frontier parameter, the linear index of every supported cohort-time cell is the log of that cohort's row margin divided by its limiting cohort share, plus the log of that period's column margin, minus the log of the total primitive mass. This is the row-column (independence-table) form of the fitted log mean.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hTop :
(⊤ : Cohort T) ∈ C
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
g :
Cohort T
hg :
g ∈ C
t :
Fin T
conclusion
collapsedDesignMap T C (frontierNuisanceParameter T C hT hTop pi barB gamma delta) (⟨g, hg⟩, t)
= log (primitiveRow T pi barB gamma delta g / (pi g : ℝ))
+ log (primitiveColumn T C pi barB gamma delta t)
- log (primitiveTotal T C pi barB gamma delta)
Proof (Lean source)
lemma frontierNuisanceParameter_index (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (hg : g ∈ C) (t : Fin T) :
collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) (⟨g, hg⟩, t) =
log (primitiveRow T pi barB gamma delta g / (pi g : ℝ)) +
log (primitiveColumn T C pi barB gamma delta t) -
log (primitiveTotal T C pi barB gamma delta) := by
classical
change collapsedIndex T C (collapsedRegressor T C g t)
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) = _
rw [collapsedIndex_eq_levels T C _ g hg t]
unfold collapsedCohortLevel collapsedTimeLevel frontierNuisanceParameter
dsimp only
by_cases hgTop : g = ⊤
· subst g
rw [dif_neg (by simp)]
by_cases ht : t.val ≠ 0
· rw [dif_pos ht]
simp
ring
· rw [dif_neg ht]
have ht0 : t = ⟨0, hT⟩ := Fin.ext (Nat.eq_zero_of_not_pos (by omega))
subst t
simp
· rw [dif_pos hgTop, dif_pos hg]
by_cases ht : t.val ≠ 0
· rw [dif_pos ht]
simp
ring
· rw [dif_neg ht]
have ht0 : t = ⟨0, hT⟩ := Fin.ext (Nat.eq_zero_of_not_pos (by omega))
subst t
simp
ring
theorem frontierNuisanceParameter_exp
At the frontier parameter, each fitted mean is the product of its row and column primitive margins, divided by its cohort share and the total primitive mass.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hTop :
(⊤ : Cohort T) ∈ C
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
g :
Cohort T
hg :
g ∈ C
t :
Fin T
conclusion
exp (collapsedDesignMap T C (frontierNuisanceParameter T C hT hTop pi barB gamma delta) (⟨g, hg⟩, t))
= primitiveRow T pi barB gamma delta g * primitiveColumn T C pi barB gamma delta t / ((pi g : ℝ) * primitiveTotal T C pi barB gamma delta)
Proof (Lean source)
lemma frontierNuisanceParameter_exp (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (hg : g ∈ C) (t : Fin T) :
exp (collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) (⟨g, hg⟩, t)) =
primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t /
((pi g : ℝ) * primitiveTotal T C pi barB gamma delta) := by
rw [frontierNuisanceParameter_index T C hT hTop pi barB gamma delta g hg t]
have hrow := frontierPrimitiveRow_pos T hT pi barB gamma delta g
have hcol := frontierPrimitiveColumn_pos T C ⟨⊤, hTop⟩ pi barB gamma delta t
have htotal := frontierPrimitiveTotal_pos T C hT ⟨⊤, hTop⟩ pi barB gamma delta
have hpi := (pi g).property.1
rw [Real.exp_sub, Real.exp_add, Real.exp_log (div_pos hrow hpi),
Real.exp_log hcol, Real.exp_log htotal]
field_simp
<;> ring
The conditional residual is the cell-mass-weighted difference between the observed mean and the beta-zero row-column fitted mean.
Definition (Lean source)
noncomputable def frontierConditionalResidual (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (hg : g ∈ C) (t : Fin T) : ℝ :=
limitingCellMass T pi g *
(observedCohortMean T barB gamma delta g t -
exp (collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) (⟨g, hg⟩, t)))
theorem frontierConditionalResidual_eq
The conditional residual at the zero-treatment-coefficient frontier equals the cell's primitive mass minus the product of its row and column margins divided by the total primitive mass, the whole difference divided by the number of periods. In other words the residual table is exactly the independence-table residual of the primitive mass matrix, rescaled by the panel length.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hTop :
(⊤ : Cohort T) ∈ C
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
g :
Cohort T
hg :
g ∈ C
t :
Fin T
conclusion
frontierConditionalResidual T C hT hTop pi barB gamma delta g hg t
= (primitiveH T pi barB gamma delta g t - primitiveRow T pi barB gamma delta g * primitiveColumn T C pi barB gamma delta t / primitiveTotal T C pi barB gamma delta) / T
Proof (Lean source)
lemma frontierConditionalResidual_eq (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (hg : g ∈ C) (t : Fin T) :
frontierConditionalResidual T C hT hTop pi barB gamma delta g hg t =
(primitiveH T pi barB gamma delta g t -
primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta) / T := by
rw [frontierConditionalResidual, frontierNuisanceParameter_exp T C hT hTop]
unfold limitingCellMass primitiveH observedCohortMean
have hpi : (pi g : ℝ) ≠ 0 := ne_of_gt (pi g).property.1
have htotal : primitiveTotal T C pi barB gamma delta ≠ 0 :=
ne_of_gt (frontierPrimitiveTotal_pos T C hT ⟨⊤, hTop⟩ pi barB gamma delta)
field_simp
theorem frontierConditionalResidual_row_sum
The conditional residuals sum to zero within every supported cohort.
Formal statement
Proof (Lean source)
lemma frontierConditionalResidual_row_sum (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (hg : g ∈ C) :
(∑ t, frontierConditionalResidual T C hT hTop pi barB gamma delta g hg t) = 0 := by
simp_rw [frontierConditionalResidual_eq]
rw [← Finset.sum_div, Finset.sum_sub_distrib]
change (primitiveRow T pi barB gamma delta g -
∑ t, primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta) / T = 0
rw [← Finset.sum_div, ← Finset.mul_sum, frontierPrimitiveColumn_sum]
have htotal : primitiveTotal T C pi barB gamma delta ≠ 0 :=
ne_of_gt (frontierPrimitiveTotal_pos T C hT ⟨⊤, hTop⟩ pi barB gamma delta)
field_simp
ring
theorem frontierConditionalResidual_column_sum
The conditional residuals sum to zero across supported cohorts in every period.
Formal statement
Proof (Lean source)
lemma frontierConditionalResidual_column_sum (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(t : Fin T) :
(∑ g : ↑C, frontierConditionalResidual T C hT hTop pi barB gamma delta
g.1 g.2 t) = 0 := by
simp_rw [frontierConditionalResidual_eq]
rw [← Finset.sum_div, Finset.sum_sub_distrib]
rw [show (∑ g : ↑C, primitiveH T pi barB gamma delta g.1 t) =
primitiveColumn T C pi barB gamma delta t by
unfold primitiveColumn
simpa using Finset.sum_attach (s := C)
(f := fun g => primitiveH T pi barB gamma delta g t)]
change (primitiveColumn T C pi barB gamma delta t -
∑ g : ↑C, primitiveRow T pi barB gamma delta g.1 *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta) / T = 0
rw [← Finset.sum_div]
simp_rw [mul_comm (primitiveRow T pi barB gamma delta _)]
rw [← Finset.mul_sum]
rw [show (∑ g : ↑C, primitiveRow T pi barB gamma delta g.1) =
primitiveTotal T C pi barB gamma delta by
unfold primitiveTotal
simpa using Finset.sum_attach (s := C)
(f := fun g => primitiveRow T pi barB gamma delta g)]
change (primitiveColumn T C pi barB gamma delta t -
primitiveColumn T C pi barB gamma delta t *
primitiveTotal T C pi barB gamma delta /
primitiveTotal T C pi barB gamma delta) / T = 0
have htotal : primitiveTotal T C pi barB gamma delta ≠ 0 :=
ne_of_gt (frontierPrimitiveTotal_pos T C hT ⟨⊤, hTop⟩ pi barB gamma delta)
field_simp
ring
theorem frontierConditionalNuisanceScore
At the beta-zero frontier fit, every nuisance-regressor score of the PPML objective is zero.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hTop :
(⊤ : Cohort T) ∈ C
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
u :
CollapsedNuisanceIndex T C → ℝ
conclusion
∑ z : SupportedCell T C, limitingCellMass T pi z.1.1 * collapsedDesignMap T C (u, 0) z * (observedCohortMean T barB gamma delta z.1.1 z.2 - exp (collapsedDesignMap T C (frontierNuisanceParameter T C hT hTop pi barB gamma delta) z))
= 0
Proof (Lean source)
lemma frontierConditionalNuisanceScore (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(u : CollapsedNuisanceIndex T C → ℝ) :
∑ z : SupportedCell T C,
limitingCellMass T pi z.1.1 * collapsedDesignMap T C (u, 0) z *
(observedCohortMean T barB gamma delta z.1.1 z.2 -
exp (collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) z)) = 0 := by
classical
rw [Fintype.sum_prod_type]
have hreg (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
collapsedDesignMap T C (u, 0) (⟨g, hg⟩, t) =
∑ j, collapsedNuisanceRegressor T C g t j * u j := by
simp [collapsedDesignMap, collapsedIndex, collapsedRegressor]
simp_rw [hreg]
rw [show (∑ g : ↑C, ∑ t,
(limitingCellMass T pi g.1 *
∑ j, collapsedNuisanceRegressor T C g.1 t j * u j) *
(observedCohortMean T barB gamma delta g.1 t -
exp (collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) (g, t)))) =
∑ g : ↑C, ∑ t,
(∑ j, collapsedNuisanceRegressor T C g.1 t j * u j) *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t by
apply Finset.sum_congr rfl
intro g _
apply Finset.sum_congr rfl
intro t _
unfold frontierConditionalResidual
ring]
rw [show (∑ g : ↑C, ∑ t, (∑ j, collapsedNuisanceRegressor T C g.1 t j * u j) *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t) =
∑ j, u j * ∑ g : ↑C, ∑ t,
collapsedNuisanceRegressor T C g.1 t j *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t by
simp_rw [Finset.sum_mul]
calc
(∑ g : ↑C, ∑ t, ∑ j,
collapsedNuisanceRegressor T C g.1 t j * u j *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t) =
∑ g : ↑C, ∑ j, ∑ t,
collapsedNuisanceRegressor T C g.1 t j * u j *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t := by
apply Finset.sum_congr rfl
intro g _
rw [Finset.sum_comm]
_ = ∑ j, ∑ g : ↑C, ∑ t,
collapsedNuisanceRegressor T C g.1 t j * u j *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t := by
rw [Finset.sum_comm]
_ = _ := by
simp_rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro j _
apply Finset.sum_congr rfl
intro g _
apply Finset.sum_congr rfl
intro t _
ring]
apply Finset.sum_eq_zero
intro j _
apply mul_eq_zero_of_right
rcases j with (_ | j)
· simp only [collapsedNuisanceRegressor, one_mul]
rw [Finset.sum_eq_zero]
intro g _
exact frontierConditionalResidual_row_sum T C hT hTop pi barB gamma delta g.1 g.2
· rcases j with (j | j)
· simp only [collapsedNuisanceRegressor]
rw [Finset.sum_eq_single j.1]
· simpa using frontierConditionalResidual_row_sum T C hT hTop pi barB gamma delta
j.1.1 j.1.2
· intro g hg hne
simp [hne]
· simp
· simp only [collapsedNuisanceRegressor]
rw [Finset.sum_comm, Finset.sum_eq_single j.1]
· simpa using frontierConditionalResidual_column_sum T C hT hTop pi barB gamma delta j.1
· intro t ht hne
simp [hne]
· simp
theorem frontierConditionalScalarScore
At the beta-zero frontier fit, the treatment score equals the frontier elimination handle divided by the horizon and total primitive mass.
Formal statement
hypotheses
conclusion
∑ z : SupportedCell T C, limitingCellMass T pi z.1.1 * collapsedDesignMap T C (0, 1) z * (observedCohortMean T barB gamma delta z.1.1 z.2 - exp (collapsedDesignMap T C (frontierNuisanceParameter T C hT hTop pi barB gamma delta) z))
= frontierEliminationHandle T C pi barB gamma delta / (T * primitiveTotal T C pi barB gamma delta)
Proof (Lean source)
lemma frontierConditionalScalarScore (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
∑ z : SupportedCell T C,
limitingCellMass T pi z.1.1 * collapsedDesignMap T C (0, 1) z *
(observedCohortMean T barB gamma delta z.1.1 z.2 -
exp (collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) z)) =
frontierEliminationHandle T C pi barB gamma delta /
(T * primitiveTotal T C pi barB gamma delta) := by
classical
rw [Fintype.sum_prod_type]
have hD (g : ↑C) (t : Fin T) :
collapsedDesignMap T C (0, 1) (g, t) = treatmentIndicator T g.1 t := by
simp [collapsedDesignMap, collapsedIndex, collapsedRegressor]
simp_rw [hD]
rw [show (∑ g : ↑C, ∑ t,
limitingCellMass T pi g.1 * treatmentIndicator T g.1 t *
(observedCohortMean T barB gamma delta g.1 t -
exp (collapsedDesignMap T C
(frontierNuisanceParameter T C hT hTop pi barB gamma delta) (g, t)))) =
∑ g : ↑C, ∑ t, treatmentIndicator T g.1 t *
frontierConditionalResidual T C hT hTop pi barB gamma delta g.1 g.2 t by
apply Finset.sum_congr rfl
intro g _
apply Finset.sum_congr rfl
intro t _
unfold frontierConditionalResidual
ring]
simp_rw [frontierConditionalResidual_eq]
rw [show (∑ g : ↑C, ∑ t, treatmentIndicator T g.1 t *
((primitiveH T pi barB gamma delta g.1 t -
primitiveRow T pi barB gamma delta g.1 *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta) / T)) =
(∑ g : ↑C, ∑ t, treatmentIndicator T g.1 t *
(primitiveH T pi barB gamma delta g.1 t -
primitiveRow T pi barB gamma delta g.1 *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta)) / T by
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro g _
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro t _
ring]
have hattach (f : Cohort T → Fin T → ℝ) :
(∑ g : ↑C, ∑ t, f g.1 t) = ∑ g ∈ C, ∑ t, f g t := by
simpa using Finset.sum_attach (s := C) (f := fun g => ∑ t, f g t)
rw [show (∑ g : ↑C, ∑ t, treatmentIndicator T g.1 t *
(primitiveH T pi barB gamma delta g.1 t -
primitiveRow T pi barB gamma delta g.1 *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta)) =
∑ g ∈ C, ∑ t, treatmentIndicator T g t *
(primitiveH T pi barB gamma delta g t -
primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta) by
exact hattach (fun g t => treatmentIndicator T g t *
(primitiveH T pi barB gamma delta g t -
primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta))]
unfold frontierEliminationHandle primitiveTreatedTotal
rw [show (∑ g ∈ C, ∑ t,
treatmentIndicator T g t *
(primitiveH T pi barB gamma delta g t -
primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t /
primitiveTotal T C pi barB gamma delta)) =
primitiveTreatedTotal T C pi barB gamma delta -
(∑ g ∈ C, ∑ t, treatmentIndicator T g t *
primitiveRow T pi barB gamma delta g *
primitiveColumn T C pi barB gamma delta t) /
primitiveTotal T C pi barB gamma delta by
unfold primitiveTreatedTotal
simp_rw [mul_sub]
simp_rw [Finset.sum_sub_distrib]
apply congrArg₂ (· - ·) rfl
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro g hg
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro t ht
ring]
have htotal : primitiveTotal T C pi barB gamma delta ≠ 0 :=
ne_of_gt (frontierPrimitiveTotal_pos T C hT ⟨⊤, hTop⟩ pi barB gamma delta)
field_simp
unfold primitiveTreatedTotal
ring
theorem betaStar_sign_frontierEliminationHandle
The collapsed pseudo-true treatment coefficient has exactly the sign of the primitive elimination handle.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hTop :
(⊤ : Cohort T) ∈ C
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hRank :
CollapsedDesignRank T C pi
conclusion
(betaStar T C pi barB gamma delta < 0 ↔ frontierEliminationHandle T C pi barB gamma delta < 0) ∧
(betaStar T C pi barB gamma delta = 0 ↔ frontierEliminationHandle T C pi barB gamma delta = 0) ∧
(0 < betaStar T C pi barB gamma delta ↔ 0 < frontierEliminationHandle T C pi barB gamma delta)
Proof (Lean source)
lemma betaStar_sign_frontierEliminationHandle (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hTop : (⊤ : Cohort T) ∈ C) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(hRank : CollapsedDesignRank T C pi) :
(betaStar T C pi barB gamma delta < 0 ↔
frontierEliminationHandle T C pi barB gamma delta < 0) ∧
(betaStar T C pi barB gamma delta = 0 ↔
frontierEliminationHandle T C pi barB gamma delta = 0) ∧
(0 < betaStar T C pi barB gamma delta ↔
0 < frontierEliminationHandle T C pi barB gamma delta) := by
classical
let q : SupportedCell T C → ℝ := fun z => limitingCellMass T pi z.1.1
let m : SupportedCell T C → ℝ := fun z =>
observedCohortMean T barB gamma delta z.1.1 z.2
let A := collapsedDesignMap T C
let theta0 := frontierNuisanceParameter T C hT hTop pi barB gamma delta
let u0 := theta0.1
letI : Nonempty (SupportedCell T C) := ⟨(⟨⊤, hTop⟩, ⟨0, hT⟩)⟩
have hq : ∀ z, 0 < q z := by
intro z
exact div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)
have hm : ∀ z, 0 < m z := by
intro z
unfold m observedCohortMean untreatedMean
exact mul_pos (mul_pos (barB z.1.1).property (Real.exp_pos _)) (Real.exp_pos _)
have htheta : (u0, (0 : ℝ)) = theta0 := by
ext <;> simp [u0, theta0, frontierNuisanceParameter]
have hNuisance (u : CollapsedNuisanceIndex T C → ℝ) :
∑ z, q z * A (u, 0) z * (m z - exp (A (u0, 0) z)) = 0 := by
simpa only [q, m, A, htheta, theta0] using
frontierConditionalNuisanceScore T C hT hTop pi barB gamma delta u
have hs := finitePoissonObjective_snd_sign_of_nuisance_score
q m A u0 hq hm (collapsedDesignMap_injective T C pi hRank) hNuisance
let score : ℝ := ∑ z, q z * A (0, 1) z *
(m z - exp (A (u0, 0) z))
have hscore : score = frontierEliminationHandle T C pi barB gamma delta /
(T * primitiveTotal T C pi barB gamma delta) := by
simpa only [score, q, m, A, htheta, theta0] using
frontierConditionalScalarScore T C hT hTop pi barB gamma delta
have hdenom : 0 < (T : ℝ) * primitiveTotal T C pi barB gamma delta :=
mul_pos (by exact_mod_cast hT)
(frontierPrimitiveTotal_pos T C hT ⟨⊤, hTop⟩ pi barB gamma delta)
have hcriterion : finitePoissonObjective q m A =
limitingCriterion T C pi barB gamma delta := by
funext theta
exact (limitingCriterion_eq_finitePoissonObjective
T C pi barB gamma delta theta).symm
have hbeta : (maximizerOrZero (finitePoissonObjective q m A)).2 =
betaStar T C pi barB gamma delta := by
rw [hcriterion]
rfl
dsimp only at hs
rw [hbeta] at hs
change (betaStar T C pi barB gamma delta < 0 ↔ score < 0) ∧
(betaStar T C pi barB gamma delta = 0 ↔ score = 0) ∧
(0 < betaStar T C pi barB gamma delta ↔ 0 < score) at hs
rw [hscore] at hs
have hnegdiv :
frontierEliminationHandle T C pi barB gamma delta /
((T : ℝ) * primitiveTotal T C pi barB gamma delta) < 0 ↔
frontierEliminationHandle T C pi barB gamma delta < 0 := by
constructor
· intro h
rcases div_neg_iff.mp h with hbad | hgood
· exact (not_lt_of_ge hdenom.le hbad.2).elim
· exact hgood.1
· intro h
exact div_neg_of_neg_of_pos h hdenom
have hzerodiv :
frontierEliminationHandle T C pi barB gamma delta /
((T : ℝ) * primitiveTotal T C pi barB gamma delta) = 0 ↔
frontierEliminationHandle T C pi barB gamma delta = 0 := by
constructor
· intro h
rcases div_eq_zero_iff.mp h with h | h
· exact h
· exact (ne_of_gt hdenom h).elim
· intro h
simp [h]
have hposdiv :
0 < frontierEliminationHandle T C pi barB gamma delta /
((T : ℝ) * primitiveTotal T C pi barB gamma delta) ↔
0 < frontierEliminationHandle T C pi barB gamma delta := by
constructor
· intro h
rcases div_pos_iff.mp h with hgood | hbad
· exact hgood.1
· exact (not_lt_of_ge hdenom.le hbad.2).elim
· intro h
exact div_pos h hdenom
constructor
· exact hs.1.trans hnegdiv
· constructor
· exact hs.2.1.trans hzerodiv
· exact hs.2.2.trans hposdiv
theorem primitiveLimitingCriterion_restrict Lemma primitiveLimitingCriterion_restrict in the paper ↗
The limiting criterion generated by the restricted primitive data is exactly the collapsed limiting PPML criterion.
Formal statement
hypotheses
conclusion
primitiveLimitingCriterion T C (restrictSignReversalPrimitive T C pi barB gamma delta)
= limitingCriterion T C pi barB gamma delta
Proof (Lean source)
lemma primitiveLimitingCriterion_restrict (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
primitiveLimitingCriterion T C
(restrictSignReversalPrimitive T C pi barB gamma delta) =
limitingCriterion T C pi barB gamma delta := by
funext theta
classical
unfold primitiveLimitingCriterion limitingCriterion restrictSignReversalPrimitive
rw [Fintype.sum_prod_type]
rw [show (∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(observedCohortMean T barB gamma delta g t *
collapsedIndex T C (collapsedRegressor T C g t) theta -
exp (collapsedIndex T C (collapsedRegressor T C g t) theta))) =
∑ g : ↑C, ∑ t : Fin T,
limitingCellMass T pi g.1 *
(observedCohortMean T barB gamma delta g.1 t *
collapsedIndex T C (collapsedRegressor T C g.1 t) theta -
exp (collapsedIndex T C (collapsedRegressor T C g.1 t) theta)) by
symm
simpa using Finset.sum_attach (s := C) (f := fun g => ∑ t : Fin T,
limitingCellMass T pi g *
(observedCohortMean T barB gamma delta g t *
collapsedIndex T C (collapsedRegressor T C g t) theta -
exp (collapsedIndex T C (collapsedRegressor T C g t) theta)))]
apply Finset.sum_congr rfl
intro g hg
apply Finset.sum_congr rfl
intro t ht
have hD : treatmentIndicator T g.1 t = 0 ∨ treatmentIndicator T g.1 t = 1 := by
unfold treatmentIndicator
rw [absorbingTreatment_eq]
split <;> simp
rcases hD with hD | hD
· simp [hD, observedCohortMean, limitingCellMass]
· simp [hD, observedCohortMean, limitingCellMass]
The pseudo-true treatment coefficient from the restricted primitive data equals the collapsed-model pseudo-true coefficient.
Formal statement
Proof (Lean source)
lemma primitiveBetaStar_restrict (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
primitiveBetaStar T C (restrictSignReversalPrimitive T C pi barB gamma delta) =
betaStar T C pi barB gamma delta := by
unfold primitiveBetaStar betaStar collapsedPopulationProjection
rw [primitiveLimitingCriterion_restrict]
Helpers.PoissonArgmaxDerivative 1 declarations Panel specialization of the shared one-cell finite-Poisson derivative theorem.
Panel specialization of the shared one-cell finite-Poisson derivative theorem.
theorem betaStar_update_hasDerivAt
Perturbing one treated collapsed cell differentiates the selected PPML treatment coefficient by its weighted-FWL residual contribution.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
k :
Cohort T
hk :
k ∈ C
s :
Fin T
hks :
treatmentIndicator T k s = 1
hRank :
CollapsedDesignRank T C pi
henergy :
0 < ∑ z : SupportedCell T C, meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2
conclusion
HasDerivAt (fun x ↦ betaStar T C pi barB gamma (update delta (k, s) x)) (limitingCellMass T pi k * untreatedMean T barB gamma k s * exp (delta (k, s)) * weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) / (∑ z : SupportedCell T C, meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2)) (delta (k, s))
Proof (Lean source)
lemma betaStar_update_hasDerivAt (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(k : Cohort T) (hk : k ∈ C) (s : Fin T) (hks : treatmentIndicator T k s = 1)
(hRank : CollapsedDesignRank T C pi)
(henergy : 0 < ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2) :
HasDerivAt
(fun x ↦ betaStar T C pi barB gamma (update delta (k, s) x))
(limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) /
(∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2))
(delta (k, s)) := by
classical
let q : SupportedCell T C → ℝ := fun z ↦ limitingCellMass T pi z.1.1
let m : SupportedCell T C → ℝ := fun z ↦
observedCohortMean T barB gamma delta z.1.1 z.2
let A := collapsedDesignMap T C
let j : SupportedCell T C := (⟨k, hk⟩, s)
let B := untreatedMean T barB gamma k s
let betaDot := limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) /
(∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2)
letI : Nonempty (SupportedCell T C) :=
⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩)⟩
have hq : ∀ z, 0 < q z := fun z ↦
div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)
have hm : ∀ z, 0 < m z := fun z ↦
mul_pos (mul_pos (barB z.1.1).property (Real.exp_pos _)) (Real.exp_pos _)
have hB : 0 < B := mul_pos (barB k).property (Real.exp_pos _)
have hA : Injective A := by
intro x y hxy
by_contra hne
have hsub : x - y ≠ 0 := sub_ne_zero.mpr hne
have hr := hRank (x - y) hsub
have hmap : A (x - y) = 0 := by rw [map_sub, hxy, sub_self]
have hzero :
(∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) (x - y)) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
have hz := congrFun hmap (⟨g, hg⟩, t)
change collapsedIndex T C (collapsedRegressor T C g t) (x - y) = 0 at hz
rw [hz]
simp
linarith
have hmeans (x : ℝ) :
(fun z : SupportedCell T C ↦
observedCohortMean T barB gamma (update delta (k, s) x) z.1.1 z.2) =
expCellUpdatedMean m j B x := by
funext z
by_cases hz : z = j
· subst z
simp [observedCohortMean, expCellUpdatedMean, m, j, B, hks]
· have hcell : (z.1.1, z.2) ≠ (k, s) := by
intro heq
rcases z with ⟨⟨g, hg⟩, t⟩
simp only at heq
have hgk : g = k := congrArg Prod.fst heq
have hts : t = s := congrArg snd heq
subst g
subst t
exact hz rfl
simp [observedCohortMean, expCellUpdatedMean, m, j, B, hz, hcell]
have hmean0 : expCellUpdatedMean m j B (delta (k, s)) = m := by
rw [← hmeans]
funext z
simp [m]
have hprojection0 :
maximizerOrZero
(finitePoissonObjective q (expCellUpdatedMean m j B (delta (k, s))) A) =
collapsedPopulationProjection T C pi barB gamma delta := by
unfold collapsedPopulationProjection
apply congrArg maximizerOrZero
funext theta
rw [limitingCriterion_eq_finitePoissonObjective]
simp only [q, A]
rw [hmean0]
have hbeta : ∀ v : CollapsedParameter T C,
(∀ d : CollapsedParameter T C,
∑ z, q z * A d z *
((if z = j then B * exp (delta (k, s)) else 0) -
exp
(A (maximizerOrZero
(finitePoissonObjective q (expCellUpdatedMean m j B (delta (k, s))) A)) z) *
A v z) = 0) →
v.2 = betaDot := by
intro v hv
apply linearizedScore_snd_eq_weightedFWL T C hT hC pi barB gamma delta k hk s v
henergy
intro d
have hs := hv d
rw [hprojection0] at hs
exact hs
have hg := finitePoissonObjective_expCell_argmax_snd_hasDerivAt
q m A j B (delta (k, s)) betaDot hq hm hB hA hbeta
have hfun (x : ℝ) :
betaStar T C pi barB gamma (update delta (k, s) x) =
(maximizerOrZero (finitePoissonObjective q (expCellUpdatedMean m j B x) A)).2 := by
unfold betaStar collapsedPopulationProjection
apply congrArg (fun f : CollapsedParameter T C → ℝ ↦ (maximizerOrZero f).2)
funext theta
rw [limitingCriterion_eq_finitePoissonObjective]
simp only [q, A]
rw [hmeans]
change HasDerivAt _ betaDot (delta (k, s))
apply hg.congr_of_eventuallyEq
exact Filter.Eventually.of_forall hfun
Helpers.WeightedFWL 9 declarations This file normalizes the positive weights q_gt * mu_star_gt, builds the shared WeightedSupport, and applies its nuisance-space residual maker to the treatment regressor.
Mean-weighted FWL residuals
This file normalizes the positive weights q_gt * mu_star_gt, builds the
shared WeightedSupport, and applies its nuisance-space residual maker to the
treatment regressor.
def normalizedPositiveSupport
Normalize positive weights on a nonempty finite support.
Definition (Lean source)
noncomputable def normalizedPositiveSupport {R : Type*} [Fintype R] [DecidableEq R]
(S : Finset R) (hS : S.Nonempty) (w : R → ℝ) (hw : ∀ r ∈ S, 0 < w r) :
WeightedSupport R where
observed := S
observed_nonempty := hS
weight r := if r ∈ S then w r / ∑ s ∈ S, w s else 0
weight_pos := by
intro r hr
rw [if_pos hr]
exact div_pos (hw r hr) (Finset.sum_pos hw hS)
weight_zero_off := by
intro r hr
simp [hr]
weight_sum_one := by
rw [Finset.sum_congr rfl (fun r hr => if_pos hr)]
simp_rw [div_eq_mul_inv]
rw [← Finset.sum_mul]
exact mul_inv_cancel₀ (ne_of_gt (Finset.sum_pos hw hS))
def meanFWLWeight
The raw effect-dependent PPML projection weight.
Definition (Lean source)
noncomputable def meanFWLWeight (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) (z : Cell T) : ℝ :=
limitingCellMass T pi z.1 * fittedMean T C pi barB gamma delta z.1 z.2
def meanWeightedSupport
The normalized support carrying weights proportional to q_gt * mu_star_gt.
Definition (Lean source)
noncomputable def meanWeightedSupport (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
WeightedSupport (SupportedCell T C) :=
normalizedPositiveSupport univ
(by exact ⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩), Finset.mem_univ _⟩)
(fun z => meanFWLWeight T C pi barB gamma delta (z.1.1, z.2))
(by
intro z hz
have hpi : 0 < (pi z.1.1 : ℝ) := (pi z.1.1).property.1
have hTr : 0 < (T : ℝ) := by exact_mod_cast hT
unfold meanFWLWeight limitingCellMass
exact mul_pos (div_pos hpi hTr) (Real.exp_pos _))
def collapsedNuisanceSubspace
The nuisance subspace spanned by the fixed-effect columns X_gt.
Definition (Lean source)
noncomputable def collapsedNuisanceSubspace (T : ℕ) (C : Finset (Cohort T)) :
Submodule ℝ (SupportedCell T C → ℝ) :=
span ℝ (Set.range fun j : CollapsedNuisanceIndex T C =>
fun z => collapsedNuisanceRegressor T C z.1.1 z.2 j)
def nuisanceWLSObjective
The coefficient-vector WLS objective whose minimizer is rho_star.
Definition (Lean source)
noncomputable def nuisanceWLSObjective (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(rho : CollapsedNuisanceIndex T C → ℝ) : ℝ :=
∑ g ∈ C, ∑ t : Fin T,
meanFWLWeight T C pi barB gamma delta (g, t) *
(treatmentIndicator T g t -
∑ j, collapsedNuisanceRegressor T C g t j * rho j) ^ 2
def rhoStar
The selected minimizer of the mean-weighted nuisance projection.
Definition (Lean source)
noncomputable def rhoStar (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
CollapsedNuisanceIndex T C → ℝ :=
let c := meanWeightedSupport T C hT hC pi barB gamma delta
let H := collapsedNuisanceSubspace T C
let D : SupportedCell T C → ℝ := fun z => treatmentIndicator T z.1.1 z.2
choose ((Submodule.mem_span_range_iff_exists_fun ℝ).mp (c.proj_mem H D))
The pseudo-true mean-weighted FWL treatment residual.
Definition (Lean source)
noncomputable def weightedFWLResidual (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
SupportedCell T C → ℝ :=
let c := meanWeightedSupport T C hT hC pi barB gamma delta
c.tildeX (collapsedNuisanceSubspace T C) (fun z => treatmentIndicator T z.1.1 z.2)
theorem weightedFWLResidual_eq_rhoStar
On supported cells, the substrate residual equals the coefficient-form residual.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
g :
Cohort T
hg :
g ∈ C
t :
Fin T
conclusion
weightedFWLResidual T C hT hC pi barB gamma delta (⟨g, hg⟩, t)
= treatmentIndicator T g t
- ∑ j, collapsedNuisanceRegressor T C g t j * rhoStar T C hT hC pi barB gamma delta j
Proof (Lean source)
lemma weightedFWLResidual_eq_rhoStar (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(g : Cohort T) (hg : g ∈ C) (t : Fin T) :
weightedFWLResidual T C hT hC pi barB gamma delta (⟨g, hg⟩, t) =
treatmentIndicator T g t -
∑ j, collapsedNuisanceRegressor T C g t j *
rhoStar T C hT hC pi barB gamma delta j := by
classical
let c := meanWeightedSupport T C hT hC pi barB gamma delta
let H := collapsedNuisanceSubspace T C
let D : SupportedCell T C → ℝ := fun z => treatmentIndicator T z.1.1 z.2
let z : SupportedCell T C := (⟨g, hg⟩, t)
have hrho := Classical.choose_spec
((Submodule.mem_span_range_iff_exists_fun ℝ).mp (c.proj_mem H D))
have hrho_z := congrFun hrho z
rw [weightedFWLResidual, show meanWeightedSupport T C hT hC pi barB gamma delta = c by rfl]
simp only [WeightedSupport.tildeX_eq, Pi.sub_apply]
change D z - c.proj H D z = D z - _
congr 1
rw [← hrho_z]
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
unfold rhoStar
apply Finset.sum_congr rfl
intro j hj
rw [mul_comm]
theorem linearizedScore_snd_eq_weightedFWL
A solution of the one-cell linearized collapsed Poisson score has treatment coordinate equal to the weighted-FWL residual contribution divided by its weighted energy.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
k :
Cohort T
hk :
k ∈ C
s :
Fin T
v :
henergy :
0 < ∑ z : SupportedCell T C, meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2
hscore :
∀ d : CollapsedParameter T C,
∑ z : SupportedCell T C, limitingCellMass T pi z.1.1 * collapsedDesignMap T C d z * ((if z = (⟨k, hk⟩, s) then untreatedMean T barB gamma k s * exp (delta (k, s)) else 0) - fittedMean T C pi barB gamma delta z.1.1 z.2 * collapsedDesignMap T C v z)
= 0
conclusion
v.2
= limitingCellMass T pi k * untreatedMean T barB gamma k s * exp (delta (k, s)) * weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) / (∑ z : SupportedCell T C, meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2)
Proof (Lean source)
lemma linearizedScore_snd_eq_weightedFWL (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(k : Cohort T) (hk : k ∈ C) (s : Fin T)
(v : CollapsedParameter T C)
(henergy : 0 < ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2)
(hscore : ∀ d : CollapsedParameter T C,
∑ z : SupportedCell T C,
limitingCellMass T pi z.1.1 * collapsedDesignMap T C d z *
((if z = (⟨k, hk⟩, s) then
untreatedMean T barB gamma k s * exp (delta (k, s)) else 0) -
fittedMean T C pi barB gamma delta z.1.1 z.2 *
collapsedDesignMap T C v z) = 0) :
v.2 = limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) *
weightedFWLResidual T C hT hC pi barB gamma delta (⟨k, hk⟩, s) /
(∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(weightedFWLResidual T C hT hC pi barB gamma delta z) ^ 2) := by
classical
let c := meanWeightedSupport T C hT hC pi barB gamma delta
let H := collapsedNuisanceSubspace T C
let X : SupportedCell T C → ℝ := fun z ↦ treatmentIndicator T z.1.1 z.2
let W := weightedFWLResidual T C hT hC pi barB gamma delta
let source : SupportedCell T C → ℝ := fun z ↦
if z = (⟨k, hk⟩, s) then
untreatedMean T barB gamma k s * exp (delta (k, s)) else 0
let mu : SupportedCell T C → ℝ := fun z ↦
fittedMean T C pi barB gamma delta z.1.1 z.2
let Y : SupportedCell T C → ℝ := fun z ↦ source z / mu z
let alpha : SupportedCell T C → ℝ := fun z ↦
∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j * v.1 j
let Z : ℝ := ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2)
letI : Nonempty (SupportedCell T C) :=
⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩)⟩
have hZ : 0 < Z := by
apply Finset.sum_pos
· intro z hz
exact mul_pos (div_pos (pi z.1.1).property.1 (by exact_mod_cast hT))
(Real.exp_pos _)
· exact Finset.univ_nonempty
have halpha : alpha ∈ H := by
apply (Submodule.mem_span_range_iff_exists_fun ℝ).mpr
refine ⟨v.1, ?_⟩
funext z
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
dsimp [alpha, H, collapsedNuisanceSubspace]
apply Finset.sum_congr rfl
intro j hj
ring
have hres (z : SupportedCell T C) :
Y z - v.2 * X z - alpha z =
(source z - mu z * collapsedDesignMap T C v z) / mu z := by
dsimp [Y, X, alpha]
have hmu : mu z ≠ 0 := by
dsimp [mu, fittedMean]
exact ne_of_gt (Real.exp_pos _)
rw [show collapsedDesignMap T C v z =
(∑ x, collapsedNuisanceRegressor T C z.1.1 z.2 x * v.1 x) +
treatmentIndicator T z.1.1 z.2 * v.2 by rfl]
field_simp [hmu]
ring
have hnormal (d : CollapsedParameter T C) :
c.ip (Y - v.2 • X - alpha) (fun z ↦ collapsedDesignMap T C d z) = 0 := by
have hs := hscore d
rw [show c.ip (Y - v.2 • X - alpha) (fun z ↦ collapsedDesignMap T C d z) =
(∑ z : SupportedCell T C,
limitingCellMass T pi z.1.1 * collapsedDesignMap T C d z *
(source z - mu z * collapsedDesignMap T C v z)) / Z by
simp [c, meanWeightedSupport, normalizedPositiveSupport, meanFWLWeight,
ip, hres, Pi.sub_apply, Pi.smul_apply,
smul_eq_mul, Z]
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro z hz
have hmu : mu z ≠ 0 := by
dsimp [mu, fittedMean]
exact ne_of_gt (Real.exp_pos _)
field_simp [hmu, ne_of_gt hZ]
ring]
simpa [source, mu] using congrArg (fun x : ℝ ↦ x / Z) hs
have hnormalX : c.ip (Y - v.2 • X - alpha) X = 0 := by
simpa [X, collapsedDesignMap, collapsedIndex, collapsedRegressor] using
hnormal (0, 1)
have hnormalH : ∀ h ∈ H, c.ip (Y - v.2 • X - alpha) h = 0 := by
intro h hh
obtain ⟨rho, hrho⟩ := (Submodule.mem_span_range_iff_exists_fun ℝ).mp hh
rw [← hrho]
have hn := hnormal (rho, 0)
rw [show (∑ i, rho i • fun z ↦ collapsedNuisanceRegressor T C z.1.1 z.2 i) =
(fun z ↦ collapsedDesignMap T C (rho, 0) z) by
funext z
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
change (∑ i, rho i * collapsedNuisanceRegressor T C z.1.1 z.2 i) =
(∑ i, collapsedNuisanceRegressor T C z.1.1 z.2 i * rho i) +
treatmentIndicator T z.1.1 z.2 * 0
rw [mul_zero, add_zero]
apply Finset.sum_congr rfl
intro i hi
ring]
exact hn
have hpos : 0 < c.ip W W := by
rw [show c.ip W W =
(∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (W z) ^ 2) / Z by
simp [c, meanWeightedSupport, normalizedPositiveSupport,
ip, Z, pow_two]
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro z hz
field_simp [ne_of_gt hZ]
]
exact div_pos henergy hZ
have hfwl := scalar_fwl_of_normalEqs c H X Y v.2 alpha halpha (ne_of_gt hpos) hnormalX hnormalH
rw [hfwl]
have hW : c.tildeX H X = W := rfl
rw [hW]
rw [show c.ip W Y =
(limitingCellMass T pi k * untreatedMean T barB gamma k s *
exp (delta (k, s)) * W (⟨k, hk⟩, s)) / Z by
simp [c, meanWeightedSupport, normalizedPositiveSupport,
ip, Y, source, mu, Z,
meanFWLWeight, fittedMean]
rw [Fintype.sum_eq_single (⟨k, hk⟩, s)]
· simp
field_simp [Real.exp_ne_zero]
· intro z hz
simp [hz]
]
rw [show c.ip W W =
(∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (W z) ^ 2) / Z by
simp [c, meanWeightedSupport, normalizedPositiveSupport,
ip, Z, pow_two]
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro z hz
field_simp [ne_of_gt hZ]
]
have hE : (∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (W z) ^ 2) ≠ 0 := by
exact ne_of_gt (by simpa [W] using henergy)
field_simp [ne_of_gt hZ, hE]
ring
Helpers.WeightedFWLContinuity 9 declarations Continuity of the effect-dependent mean-weighted FWL residual.
Continuity of the effect-dependent mean-weighted FWL residual.
theorem collapsedPopulationProjection_continuousAt_effects
The collapsed population parameter varies continuously with the full finite effect array.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
hRank :
CollapsedDesignRank T C pi
delta₀ :
Cell T → ℝ
conclusion
ContinuousAt (fun delta : Cell T → ℝ => collapsedPopulationProjection T C pi barB gamma delta) delta₀
Proof (Lean source)
lemma collapsedPopulationProjection_continuousAt_effects
(T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(hRank : CollapsedDesignRank T C pi) (delta₀ : Cell T → ℝ) :
ContinuousAt
(fun delta : Cell T → ℝ =>
collapsedPopulationProjection T C pi barB gamma delta)
delta₀ := by
let q : SupportedCell T C → ℝ := fun z => limitingCellMass T pi z.1.1
let m : (Cell T → ℝ) → SupportedCell T C → ℝ := fun delta z =>
observedCohortMean T barB gamma delta z.1.1 z.2
let A := collapsedDesignMap T C
letI : Nonempty (SupportedCell T C) :=
⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩)⟩
have hq : ∀ z, 0 < q z := by
intro z
exact div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)
have hm : ∀ z, 0 < m delta₀ z := by
intro z
exact mul_pos (mul_pos (barB z.1.1).property (Real.exp_pos _)) (Real.exp_pos _)
have hmcont : Continuous (m : (Cell T → ℝ) → SupportedCell T C → ℝ) := by
dsimp [m, observedCohortMean, untreatedMean]
fun_prop
have hsel := finitePoissonObjective_argmax_continuousAt_mean
q A (m delta₀) hq hm (collapsedDesignMap_injective T C pi hRank)
have hcomp := hsel.comp hmcont.continuousAt
have heq :
(fun delta : Cell T → ℝ =>
maximizerOrZero (finitePoissonObjective q (m delta) A)) =
(fun delta : Cell T → ℝ =>
collapsedPopulationProjection T C pi barB gamma delta) := by
funext delta
unfold collapsedPopulationProjection
apply congrArg maximizerOrZero
funext theta
exact (limitingCriterion_eq_finitePoissonObjective
T C pi barB gamma delta theta).symm
rw [← heq]
exact hcomp
theorem fittedMean_continuousAt_effects
Every fitted supported-cell mean varies continuously with the full effect array.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
hRank :
CollapsedDesignRank T C pi
delta₀ :
Cell T → ℝ
g :
Cohort T
t :
Fin T
conclusion
Proof (Lean source)
lemma fittedMean_continuousAt_effects
(T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(hRank : CollapsedDesignRank T C pi) (delta₀ : Cell T → ℝ)
(g : Cohort T) (t : Fin T) :
ContinuousAt
(fun delta : Cell T → ℝ => fittedMean T C pi barB gamma delta g t)
delta₀ := by
unfold fittedMean
have htheta := collapsedPopulationProjection_continuousAt_effects
T C hT hC pi barB gamma hRank delta₀
have hindex : Continuous
(fun theta : CollapsedParameter T C =>
collapsedIndex T C (collapsedRegressor T C g t) theta) := by
unfold collapsedIndex
fun_prop
exact Real.continuous_exp.continuousAt.comp (hindex.continuousAt.comp htheta)
def meanFWLNuisanceGram
Raw-weight nuisance Gram matrix for the fixed collapsed nuisance basis.
Definition (Lean source)
noncomputable def meanFWLNuisanceGram (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
Matrix (CollapsedNuisanceIndex T C) (CollapsedNuisanceIndex T C) ℝ :=
fun j k => ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
collapsedNuisanceRegressor T C z.1.1 z.2 j *
collapsedNuisanceRegressor T C z.1.1 z.2 k
def meanFWLNuisanceRhs
Raw-weight nuisance normal-equation right-hand side.
Definition (Lean source)
noncomputable def meanFWLNuisanceRhs (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) :
CollapsedNuisanceIndex T C → ℝ :=
fun j => ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
collapsedNuisanceRegressor T C z.1.1 z.2 j *
treatmentIndicator T z.1.1 z.2
def continuousNuisanceCoefficient
Continuous finite-basis coefficient formula for the nuisance projection.
Definition (Lean source)
noncomputable def continuousNuisanceCoefficient (T : ℕ)
(C : Finset (Cohort T)) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta : Cell T → ℝ) : CollapsedNuisanceIndex T C → ℝ :=
(meanFWLNuisanceGram T C pi barB gamma delta)⁻¹.mulVec
(meanFWLNuisanceRhs T C pi barB gamma delta)
theorem meanFWLNuisanceGram_quadratic
The quadratic form of the mean-weighted nuisance Gram matrix is a weighted sum of squares over the supported cohort-time cells: for any coefficient direction, it equals the sum over cells of that cell's mean weight times the square of the cell's nuisance regressor evaluated in the direction. Since the mean weights are nonnegative, this exhibits the Gram matrix as positive semidefinite.
Formal statement
hypotheses
conclusion
= ∑ z : SupportedCell T C, meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) * (∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j * rho j) ^ 2
Proof (Lean source)
lemma meanFWLNuisanceGram_quadratic (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(rho : CollapsedNuisanceIndex T C → ℝ) :
dotProduct rho
((meanFWLNuisanceGram T C pi barB gamma delta).mulVec rho) =
∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j * rho j) ^ 2 := by
classical
simp only [dotProduct, mulVec, meanFWLNuisanceGram]
calc
_ = ∑ j, ∑ k, ∑ z : SupportedCell T C,
rho j * (meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
collapsedNuisanceRegressor T C z.1.1 z.2 j *
collapsedNuisanceRegressor T C z.1.1 z.2 k * rho k) := by
apply Finset.sum_congr rfl
intro j hj
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro k hk
rw [Finset.sum_mul]
rw [Finset.mul_sum]
_ = ∑ j, ∑ z : SupportedCell T C, ∑ k,
rho j * (meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
collapsedNuisanceRegressor T C z.1.1 z.2 j *
collapsedNuisanceRegressor T C z.1.1 z.2 k * rho k) := by
apply Finset.sum_congr rfl
intro j hj
exact Finset.sum_comm
_ = ∑ z : SupportedCell T C, ∑ j, ∑ k,
rho j * (meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
collapsedNuisanceRegressor T C z.1.1 z.2 j *
collapsedNuisanceRegressor T C z.1.1 z.2 k * rho k) := Finset.sum_comm
_ = _ := by
apply Finset.sum_congr rfl
intro z hz
rw [pow_two, Finset.mul_sum]
simp_rw [Finset.sum_mul]
conv_rhs => rw [Finset.sum_comm]
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro j hj
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro k hk
ring
theorem meanFWLNuisanceGram_isUnit
Positive fitted means and collapsed full rank make the fixed nuisance Gram matrix nonsingular at every effect array.
Formal statement
Proof (Lean source)
lemma meanFWLNuisanceGram_isUnit (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta : Cell T → ℝ) (hRank : CollapsedDesignRank T C pi) :
IsUnit (meanFWLNuisanceGram T C pi barB gamma delta).det := by
classical
rw [← Matrix.isUnit_iff_isUnit_det]
apply Matrix.mulVec_injective_iff_isUnit.mp
intro rho sigma heq
let v : CollapsedNuisanceIndex T C → ℝ := rho - sigma
have hzero : (meanFWLNuisanceGram T C pi barB gamma delta).mulVec v = 0 := by
dsimp [v]
rw [Matrix.mulVec_sub, heq, sub_self]
have hquad : ∑ z : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) *
(∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j * v j) ^ 2 = 0 := by
rw [← meanFWLNuisanceGram_quadratic]
rw [hzero]
simp
have hx (z : SupportedCell T C) :
(∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j * v j) = 0 := by
let f : SupportedCell T C → ℝ := fun y =>
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
(∑ j, collapsedNuisanceRegressor T C y.1.1 y.2 j * v j) ^ 2
have hnonneg (y : SupportedCell T C) : 0 ≤ f y := by
exact mul_nonneg
(mul_pos (div_pos (pi y.1.1).property.1 (by exact_mod_cast hT))
(Real.exp_pos _)).le
(sq_nonneg _)
have hterm : f z ≤ ∑ y, f y :=
Finset.single_le_sum (fun y _ => hnonneg y) (Finset.mem_univ z)
have hsum : ∑ y, f y = 0 := by simpa [f] using hquad
have hfzero : f z = 0 := le_antisymm (by simpa [hsum] using hterm) (hnonneg z)
have hw : meanFWLWeight T C pi barB gamma delta (z.1.1, z.2) ≠ 0 := by
exact ne_of_gt (mul_pos
(div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)) (Real.exp_pos _))
exact sq_eq_zero_iff.mp ((mul_eq_zero.mp hfzero).resolve_left hw)
have hv : v = 0 := by
by_contra hv0
let a : CollapsedParameter T C := (v, 0)
have ha : a ≠ 0 := by
intro ha0
apply hv0
exact congrArg fst ha0
have hr := hRank a ha
have hrzero :
(∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) a) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
have hz := hx (⟨g, hg⟩, t)
change limitingCellMass T pi g *
((∑ j, collapsedNuisanceRegressor T C g t j * v j) +
treatmentIndicator T g t * 0) ^ 2 = 0
rw [hz]
ring
rw [hrzero] at hr
exact (lt_irrefl 0) hr
exact sub_eq_zero.mp hv
theorem weightedFWLResidual_eq_continuousNuisanceCoefficient
The chosen semidefinite projection agrees on the full supported table with the nonsingular finite Gram formula.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hRank :
CollapsedDesignRank T C pi
z :
SupportedCell T C
conclusion
weightedFWLResidual T C hT hC pi barB gamma delta z
= treatmentIndicator T z.1.1 z.2
- ∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j * continuousNuisanceCoefficient T C pi barB gamma delta j
Proof (Lean source)
lemma weightedFWLResidual_eq_continuousNuisanceCoefficient
(T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(delta : Cell T → ℝ) (hRank : CollapsedDesignRank T C pi)
(z : SupportedCell T C) :
weightedFWLResidual T C hT hC pi barB gamma delta z =
treatmentIndicator T z.1.1 z.2 -
∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j *
continuousNuisanceCoefficient T C pi barB gamma delta j := by
classical
letI : Nonempty (SupportedCell T C) :=
⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩)⟩
let G := meanFWLNuisanceGram T C pi barB gamma delta
let r := meanFWLNuisanceRhs T C pi barB gamma delta
let rho := continuousNuisanceCoefficient T C pi barB gamma delta
let c := meanWeightedSupport T C hT hC pi barB gamma delta
let H := collapsedNuisanceSubspace T C
let D : SupportedCell T C → ℝ := fun y => treatmentIndicator T y.1.1 y.2
let P : SupportedCell T C → ℝ := fun y =>
∑ j, collapsedNuisanceRegressor T C y.1.1 y.2 j * rho j
have hsolve : G.mulVec rho = r := by
dsimp [rho, continuousNuisanceCoefficient]
rw [Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv _
(meanFWLNuisanceGram_isUnit T C hT pi barB gamma delta hRank),
Matrix.one_mulVec]
have hnormal (j : CollapsedNuisanceIndex T C) :
∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j * (D y - P y) = 0 := by
have hj := congrFun hsolve j
have hlhs : G.mulVec rho j = ∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j * P y := by
dsimp [G, P]
simp only [mulVec, meanFWLNuisanceGram]
calc
_ = ∑ k, ∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j *
collapsedNuisanceRegressor T C y.1.1 y.2 k * rho k := by
apply Finset.sum_congr rfl
intro k hk
rw [Finset.sum_mul]
_ = ∑ y : SupportedCell T C, ∑ k,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j *
collapsedNuisanceRegressor T C y.1.1 y.2 k * rho k := Finset.sum_comm
_ = _ := by
apply Finset.sum_congr rfl
intro y hy
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro k hk
ring
have hrhs : r j = ∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j * D y := by
rfl
rw [hlhs, hrhs] at hj
calc
_ = (∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j * D y) -
(∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j * P y) := by
rw [← Finset.sum_sub_distrib]
apply Finset.sum_congr rfl
intro y hy
ring
_ = 0 := sub_eq_zero.mpr hj.symm
have hP : P ∈ H := by
apply (Submodule.mem_span_range_iff_exists_fun ℝ).mpr
refine ⟨rho, ?_⟩
funext y
simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
dsimp [P, H, collapsedNuisanceSubspace]
apply Finset.sum_congr rfl
intro j hj
ring
have horth : ∀ h ∈ H, c.ip (D - P) h = 0 := by
intro h hh
refine Submodule.span_induction ?_ ?_ ?_ ?_ hh
· rintro x ⟨j, rfl⟩
let Z : ℝ := ∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2)
have hZ : Z ≠ 0 := by
exact ne_of_gt (Finset.sum_pos
(fun y _ => mul_pos
(div_pos (pi y.1.1).property.1 (by exact_mod_cast hT)) (Real.exp_pos _))
Finset.univ_nonempty)
simp [c, meanWeightedSupport, normalizedPositiveSupport,
ip, Pi.sub_apply, Z]
calc
_ = (∑ y : SupportedCell T C,
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2) *
collapsedNuisanceRegressor T C y.1.1 y.2 j * (D y - P y)) / Z := by
rw [Finset.sum_div]
apply Finset.sum_congr rfl
intro y hy
ring
_ = 0 := by rw [hnormal j, zero_div]
· simp [ip]
· intro x y _ _ hx hy
rw [c.ip_add_right, hx, hy, add_zero]
· intro s x _ hx
rw [c.ip_smul_right, hx, mul_zero]
have hproj : c.proj H D z = P z :=
c.proj_apply_eq_of_mem_orthogonal H D hP horth z
(by simp [c, meanWeightedSupport, normalizedPositiveSupport])
rw [weightedFWLResidual]
change D z - c.proj H D z = _
rw [hproj]
theorem weightedFWLResidual_continuousAt_effects
Under collapsed full rank, the fitted-mean-weighted treatment residual at each supported cell is continuous under simultaneous perturbation of the entire finite effect vector.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hC :
C.Nonempty
gamma :
Fin T → ℝ
hRank :
CollapsedDesignRank T C pi
delta₀ :
Cell T → ℝ
z :
SupportedCell T C
conclusion
Proof (Lean source)
lemma weightedFWLResidual_continuousAt_effects
(T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hC : C.Nonempty) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ)
(hRank : CollapsedDesignRank T C pi)
(delta₀ : Cell T → ℝ) (z : SupportedCell T C) :
ContinuousAt
(fun delta : Cell T → ℝ =>
weightedFWLResidual T C hT hC pi barB gamma delta z)
delta₀ := by
classical
let G := fun delta : Cell T → ℝ =>
meanFWLNuisanceGram T C pi barB gamma delta
let r := fun delta : Cell T → ℝ =>
meanFWLNuisanceRhs T C pi barB gamma delta
have hw (y : SupportedCell T C) : ContinuousAt
(fun delta : Cell T → ℝ =>
meanFWLWeight T C pi barB gamma delta (y.1.1, y.2)) delta₀ := by
unfold meanFWLWeight
exact continuousAt_const.mul (fittedMean_continuousAt_effects
T C hT hC pi barB gamma hRank delta₀ y.1.1 y.2)
have hG : ContinuousAt G delta₀ := by
apply continuousAt_pi.mpr
intro j
apply continuousAt_pi.mpr
intro k
exact tendsto_finset_sum univ fun y hy =>
((hw y).mul continuousAt_const).mul continuousAt_const
have hr : ContinuousAt r delta₀ := by
apply continuousAt_pi.mpr
intro j
exact tendsto_finset_sum univ fun y hy =>
((hw y).mul continuousAt_const).mul continuousAt_const
have hdet : (G delta₀).det ≠ 0 :=
(meanFWLNuisanceGram_isUnit T C hT pi barB gamma delta₀ hRank).ne_zero
have hringInv : ContinuousAt Ring.inverse (G delta₀).det := by
have heq : (Ring.inverse : ℝ → ℝ) = inv := by
funext x
exact Ring.inverse_eq_inv x
rw [heq]
exact continuousAt_inv₀ hdet
have hinv : ContinuousAt (fun delta => (G delta)⁻¹) delta₀ :=
(continuousAt_matrix_inv (G delta₀) hringInv).comp hG
have hcoeff : ContinuousAt
(fun delta => continuousNuisanceCoefficient T C pi barB gamma delta)
delta₀ := by
apply continuousAt_pi.mpr
intro j
unfold continuousNuisanceCoefficient
simp only [mulVec]
exact tendsto_finset_sum univ fun k hk =>
((continuous_apply k).continuousAt.comp
((continuous_apply j).continuousAt.comp hinv)).mul
((continuous_apply k).continuousAt.comp hr)
have hexplicit : ContinuousAt
(fun delta : Cell T → ℝ =>
treatmentIndicator T z.1.1 z.2 -
∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j *
continuousNuisanceCoefficient T C pi barB gamma delta j)
delta₀ := by
apply continuousAt_const.sub
exact tendsto_finset_sum univ fun j hj =>
continuousAt_const.mul ((continuous_apply j).continuousAt.comp hcoeff)
have heq :
(fun delta : Cell T → ℝ =>
weightedFWLResidual T C hT hC pi barB gamma delta z) =
(fun delta : Cell T → ℝ =>
treatmentIndicator T z.1.1 z.2 -
∑ j, collapsedNuisanceRegressor T C z.1.1 z.2 j *
continuousNuisanceCoefficient T C pi barB gamma delta j) := by
funext delta
exact weightedFWLResidual_eq_continuousNuisanceCoefficient
T C hT hC pi barB gamma delta hRank z
rw [heq]
exact hexplicit
Homogeneous 1 declarations Correct-specification reduction under a homogeneous proportional effect.
Correct-specification reduction under a homogeneous proportional effect.
A common treated-cell log effect is recovered exactly by the collapsed PPML projection.
Formal statement
hypotheses
T :
ℕ
Omega :
ℕ → Type*
P :
∀ N, SamplingLaw (Omega N)
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
delta0 :
ℝ
hMean :
UnitUntreatedExponentialMean T Omega P Y b gamma
hRank :
CollapsedDesignRank T C pi
hHomogeneous :
∀ g ∈ C, ∀ t : Fin T, treatmentIndicator T g t = 1 → delta (g, t) = delta0
conclusion
betaStar T C pi barB gamma delta = delta0 ∧
∀ g ∈ C,
∀ t : Fin T,
fittedMean T C pi barB gamma delta g t
Proof (Lean source)
theorem homogeneous_effect_reduction (T : ℕ) (C : Finset (Cohort T))
(Omega : ℕ → Type*) (P : ∀ N, SamplingLaw (Omega N))
(Y : ∀ N, Fin N → Fin T → Fin 2 → Omega N → ℝ)
(b : ∀ N, Fin N → PosReal) (pi : Cohort T → OpenUnit)
(barB : Cohort T → PosReal) (gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(delta0 : ℝ)
(hMean : UnitUntreatedExponentialMean T Omega P Y b gamma)
(hRank : CollapsedDesignRank T C pi)
(hHomogeneous : ∀ g ∈ C, ∀ t : Fin T,
treatmentIndicator T g t = 1 → delta (g, t) = delta0) :
betaStar T C pi barB gamma delta = delta0 ∧
∀ g ∈ C, ∀ t : Fin T,
fittedMean T C pi barB gamma delta g t =
untreatedMean T barB gamma g t * exp (treatmentIndicator T g t * delta0) := by
classical
let theta0 : CollapsedParameter T C :=
(fun j => match j with
| inl _ => log (barB ⊤ : ℝ)
| inr (inl c) =>
log (barB c.1.1 : ℝ) - log (barB ⊤ : ℝ)
| inr (inr u) => gamma u.1,
delta0)
have hgamma : ∀ t : Fin T, t.val = 0 → gamma t = 0 := hMean.2
have htime (t : Fin T) :
(∑ u : TimeDummy T, if t = u.1 then gamma u.1 else 0) = gamma t := by
by_cases ht : t.val = 0
· have hne : ∀ u : TimeDummy T, t ≠ u.1 := by
intro u heq
exact u.2 (by simpa [← heq] using ht)
simp [hne, hgamma t ht]
· let u : TimeDummy T := ⟨t, ht⟩
rw [Fintype.sum_eq_single u]
· simp [u]
· intro v hv
split_ifs with heq
· exact elim (hv (Subtype.ext heq.symm))
· rfl
have hcohort (g : Cohort T) (hg : g ∈ C) :
(∑ c : CohortDummy T C,
if g = c.1.1 then
log (barB c.1.1 : ℝ) - log (barB ⊤ : ℝ) else 0) =
if g = ⊤ then 0 else log (barB g : ℝ) - log (barB ⊤ : ℝ) := by
by_cases hgTop : g = ⊤
· subst g
simp only [if_pos]
apply Fintype.sum_eq_zero
intro c
split_ifs with heq
· exact elim (c.2 heq.symm)
· rfl
· let c : CohortDummy T C := ⟨⟨g, hg⟩, hgTop⟩
rw [Fintype.sum_eq_single c]
· simp [c, hgTop]
· intro d hd
split_ifs with heq
· exact elim (hd (Subtype.ext (Subtype.ext heq.symm)))
· rfl
have hindex (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
collapsedIndex T C (collapsedRegressor T C g t) theta0 =
log (barB g : ℝ) + gamma t + treatmentIndicator T g t * delta0 := by
rw [collapsedIndex, collapsedRegressor]
rcases eq_or_ne g (⊤ : Cohort T) with rfl | hgTop
· simp [theta0, collapsedNuisanceRegressor, htime, hcohort _ hg]
· obtain ⟨g0, rfl⟩ := WithTop.ne_top_iff_exists.mp hgTop
simp [theta0, collapsedNuisanceRegressor, htime, hcohort _ hg]
ring
have heffect (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
treatmentIndicator T g t * delta (g, t) = treatmentIndicator T g t * delta0 := by
unfold treatmentIndicator
rw [absorbingTreatment_eq]
split_ifs with htreated
· rw [hHomogeneous g hg t (by simp [treatmentIndicator, htreated])]
· simp
have hfit (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
observedCohortMean T barB gamma delta g t =
exp (collapsedIndex T C (collapsedRegressor T C g t) theta0) := by
rw [observedCohortMean, untreatedMean, hindex g hg t, heffect g hg t]
rw [Real.exp_add, Real.exp_add, Real.exp_log (barB g).property]
have hobserved_pos (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
0 < observedCohortMean T barB gamma delta g t := by
rw [hfit g hg t]
exact Real.exp_pos _
have hcell_le (m eta : ℝ) (hm : 0 < m) :
m * eta - exp eta ≤ m * log m - exp (log m) := by
have h := mul_le_mul_of_nonneg_left
(Real.add_one_le_exp (eta - log m)) hm.le
rw [Real.exp_sub, Real.exp_log hm] at h
field_simp at h ⊢
rw [Real.exp_log hm]
linarith
have hcell_lt (m eta : ℝ) (hm : 0 < m) (hne : eta ≠ log m) :
m * eta - exp eta < m * log m - exp (log m) := by
have hd : eta - log m ≠ 0 := sub_ne_zero.mpr hne
have h := mul_lt_mul_of_pos_left (Real.add_one_lt_exp hd) hm
rw [Real.exp_sub, Real.exp_log hm] at h
field_simp at h ⊢
rw [Real.exp_log hm]
linarith
have hmass (g : Cohort T) (t : Fin T) : 0 < limitingCellMass T pi g := by
have hT : 0 < T := by
by_contra h
have hT0 : T = 0 := Nat.eq_zero_of_not_pos h
subst T
have hr := hRank (0, 1) (by simp)
simp at hr
exact div_pos (pi g).property.1 (by exact_mod_cast hT)
have hmax (theta : CollapsedParameter T C) :
limitingCriterion T C pi barB gamma delta theta ≤
limitingCriterion T C pi barB gamma delta theta0 := by
rw [limitingCriterion, limitingCriterion]
apply Finset.sum_le_sum
intro g hg
apply Finset.sum_le_sum
intro t ht
apply mul_le_mul_of_nonneg_left _ (hmass g t).le
have hlog : log (observedCohortMean T barB gamma delta g t) =
collapsedIndex T C (collapsedRegressor T C g t) theta0 := by
rw [hfit g hg t, Real.log_exp]
rw [← hlog]
exact hcell_le _ _ (hobserved_pos g hg t)
have hunique (theta : CollapsedParameter T C)
(htheta : limitingCriterion T C pi barB gamma delta theta =
limitingCriterion T C pi barB gamma delta theta0) : theta = theta0 := by
by_contra hne
have hneSub : theta - theta0 ≠ 0 := sub_ne_zero.mpr hne
have hrank := hRank (theta - theta0) hneSub
have hex : ∃ g ∈ C, ∃ t : Fin T,
collapsedIndex T C (collapsedRegressor T C g t) theta ≠
collapsedIndex T C (collapsedRegressor T C g t) theta0 := by
by_contra hnone
push_neg at hnone
have hzero :
(∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) (theta - theta0)) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
have heq := hnone g hg t
have hind : collapsedIndex T C (collapsedRegressor T C g t) (theta - theta0) = 0 := by
unfold collapsedIndex at heq ⊢
change (∑ j, (collapsedRegressor T C g t).1 j *
(theta.1 j - theta0.1 j)) +
(collapsedRegressor T C g t).2 * (theta.2 - theta0.2) = 0
simp_rw [mul_sub]
rw [Finset.sum_sub_distrib]
linarith
rw [hind]
simp
linarith
obtain ⟨g0, hg0, t0, hdiff⟩ := hex
have hstrictCell :
limitingCellMass T pi g0 *
(observedCohortMean T barB gamma delta g0 t0 *
collapsedIndex T C (collapsedRegressor T C g0 t0) theta -
exp (collapsedIndex T C (collapsedRegressor T C g0 t0) theta)) <
limitingCellMass T pi g0 *
(observedCohortMean T barB gamma delta g0 t0 *
collapsedIndex T C (collapsedRegressor T C g0 t0) theta0 -
exp (collapsedIndex T C (collapsedRegressor T C g0 t0) theta0)) := by
apply mul_lt_mul_of_pos_left _ (hmass g0 t0)
have hlog : log (observedCohortMean T barB gamma delta g0 t0) =
collapsedIndex T C (collapsedRegressor T C g0 t0) theta0 := by
rw [hfit g0 hg0 t0, Real.log_exp]
have hdiff' : collapsedIndex T C (collapsedRegressor T C g0 t0) theta ≠
log (observedCohortMean T barB gamma delta g0 t0) := by
rw [hlog]
exact hdiff
rw [← hlog]
exact hcell_lt _ _ (hobserved_pos g0 hg0 t0) hdiff'
have hstrict : limitingCriterion T C pi barB gamma delta theta <
limitingCriterion T C pi barB gamma delta theta0 := by
rw [limitingCriterion, limitingCriterion]
apply Finset.sum_lt_sum
· intro g hg
apply Finset.sum_le_sum
intro t ht
apply mul_le_mul_of_nonneg_left _ (hmass g t).le
have hlog : log (observedCohortMean T barB gamma delta g t) =
collapsedIndex T C (collapsedRegressor T C g t) theta0 := by
rw [hfit g hg t, Real.log_exp]
rw [← hlog]
exact hcell_le _ _ (hobserved_pos g hg t)
· refine ⟨g0, hg0, ?_⟩
apply Finset.sum_lt_sum
· intro t ht
apply mul_le_mul_of_nonneg_left _ (hmass g0 t).le
have hlog : log (observedCohortMean T barB gamma delta g0 t) =
collapsedIndex T C (collapsedRegressor T C g0 t) theta0 := by
rw [hfit g0 hg0 t, Real.log_exp]
rw [← hlog]
exact hcell_le _ _ (hobserved_pos g0 hg0 t)
· exact ⟨t0, Finset.mem_univ _, hstrictCell⟩
exact (hstrict.ne htheta)
have hexists : ∃ x, ∀ y,
limitingCriterion T C pi barB gamma delta y ≤
limitingCriterion T C pi barB gamma delta x := ⟨theta0, hmax⟩
have hprojection : collapsedPopulationProjection T C pi barB gamma delta = theta0 := by
rw [collapsedPopulationProjection, maximizerOrZero, dif_pos hexists]
apply hunique
apply le_antisymm
· exact hmax _
· exact (Classical.choose_spec hexists) theta0
constructor
· rw [betaStar, hprojection]
· intro g hg t
rw [fittedMean, hprojection, hindex g hg t]
rw [Real.exp_add, Real.exp_add, Real.exp_log (barB g).property, untreatedMean]
PrimitiveFrontier 8 declarations The nuisance-free global frontier and the distinct counterfactual-share PTT target.
The nuisance-free global frontier and the distinct counterfactual-share PTT target.
def treatedCells
The treated supported cells.
Definition (Lean source)
noncomputable def treatedCells (T : ℕ) (C : Finset (Cohort T)) : Finset (SupportedCell T C) :=
Finset.univ.filter fun z => treatmentIndicator T z.1.1 z.2 = 1
def observedCounterfactualBaseline
Observed-population untreated baseline formed from period one and never-treated means.
Definition (Lean source)
noncomputable def observedCounterfactualBaseline (T : ℕ) (hT : 0 < T)
(m : Cell T → ℝ) (g : Cohort T) (t : Fin T) : ℝ :=
m (g, ⟨0, hT⟩) * m (⊤, t) / m (⊤, ⟨0, hT⟩)
def granularTau
The granular observed proportional effect.
Definition (Lean source)
noncomputable def granularTau (T : ℕ) (hT : 0 < T) (m : Cell T → ℝ)
(g : Cohort T) (t : Fin T) : ℝ :=
m (g, t) / observedCounterfactualBaseline T hT m g t - 1
def pttNormalizer
Counterfactual-share normalizing constant.
Definition (Lean source)
noncomputable def pttNormalizer (T : ℕ) (C : Finset (Cohort T)) (hT : 0 < T)
(pi : Cohort T → OpenUnit) (m : Cell T → ℝ) : ℝ :=
∑ z ∈ treatedCells T C,
limitingCellMass T pi z.1.1 * observedCounterfactualBaseline T hT m z.1.1 z.2
def pttWeight
Counterfactual-share weight on a treated cell.
Definition (Lean source)
noncomputable def pttWeight (T : ℕ) (C : Finset (Cohort T)) (hT : 0 < T)
(pi : Cohort T → OpenUnit) (m : Cell T → ℝ) (z : SupportedCell T C) : ℝ :=
limitingCellMass T pi z.1.1 * observedCounterfactualBaseline T hT m z.1.1 z.2 /
pttNormalizer T C hT pi m
def fourMultiplierEffects
Four-period multiplier family used for the exact threshold calculation.
Definition (Lean source)
noncomputable def fourMultiplierEffects (x y : ℝ) (z : Cell 4) : ℝ :=
if treatmentIndicator 4 z.1 z.2 = 1 then
if z.1 = ((⟨1, by decide⟩ : Fin 4) : Cohort 4) ∧ z.2 = ⟨3, by decide⟩
then log y else log x
else 0
Phi has exactly the sign of the pseudo-true beta and yields the stated PTT diagnosis.
Formal statement
hypotheses
T :
ℕ
hT :
0 < T
hHorizon :
@realizes T(standing 4 ≤ T premise)
hSupport :
@realizes C(paper cohort-support premise)
Omega :
ℕ → Type*
P :
∀ N, SamplingLaw (Omega N)
gamma :
Fin T → ℝ
delta :
Cell T → ℝ
hGSupport :
∀ N i, G N i ∈ C
@realizes G_i(every deterministic label lies in C)
hShare :
CohortShareLimit T C G pi
hMean :
UnitUntreatedExponentialMean T Omega P Y b gamma
hBaseline :
WithinCohortBaselineLimit T C G b barB
hEffects :
ProportionalEffects T Omega P Y G delta
hRank :
CollapsedDesignRank T C pi
hScope :
hPositive :
StrictPositiveEffects T C delta
conclusion
let Phi := frontierEliminationHandle T C pi barB gamma delta let m : Cell T → ℝ := fun z
=> observedCohortMean T barB gamma delta z.1 z.2 (betaStar T C pi barB gamma delta < 0 ↔ Phi < 0) ∧
(betaStar T C pi barB gamma delta = 0 ↔ Phi = 0) ∧
(0 < betaStar T C pi barB gamma delta ↔ 0 < Phi) ∧
((restrictSignReversalPrimitive T C pi barB gamma delta ∈ signReversalRegion T C gamma) ↔ Phi < 0) ∧
(∀ x y : ℝ, 1 < x → 1 < y → frontierEliminationHandle 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma (fourMultiplierEffects x y) = (5 * x ^ 2 + 12 * x - 2 * y - 15) / 16) ∧
((5 * ((101 : ℝ) / 100) ^ 2 + 12 * ((101 : ℝ) / 100) - 15) / 2 = (4441 : ℝ) / 4000) ∧
frontierEliminationHandle 4 fourCohortSupport fourCohortShare fourCohortLimitBaseline fourCohortGamma fourCohortDelta
= -(11559 : ℝ) / 32000 ∧
(∀ z ∈ treatedCells T C, observedCounterfactualBaseline T hT m z.1.1 z.2 = untreatedMean T barB gamma z.1.1 z.2 ∧ granularTau T hT m z.1.1 z.2 = exp (delta (z.1.1, z.2)) - 1 ∧ 0 < pttWeight T C hT pi m z) ∧
(∑ z ∈ treatedCells T C, pttWeight T C hT pi m z) = 1 ∧
counterfactualSharePTT T C hT pi m
= (∑ z ∈ treatedCells T C, limitingCellMass T pi z.1.1 * m (z.1.1, z.2)) / (∑ z ∈ treatedCells T C, limitingCellMass T pi z.1.1 * observedCounterfactualBaseline T hT m z.1.1 z.2)
- 1 ∧
(Phi < 0 → betaStar T C pi barB gamma delta < 0 ∧ 0 < counterfactualSharePTT T C hT pi m)
Proof (Lean source)
theorem primitive_global_frontier (T : ℕ) (C : Finset (Cohort T))
(hT : 0 < T) (hHorizon : ValidPanelHorizon T) -- @realizes T(standing 4 ≤ T premise)
(hSupport : ValidCohortSupport T C) -- @realizes C(paper cohort-support premise)
(Omega : ℕ → Type*) (P : ∀ N, SamplingLaw (Omega N))
(Y : ∀ N, Fin N → Fin T → Fin 2 → Omega N → ℝ)
(G : ∀ N, Fin N → Cohort T) (b : ∀ N, Fin N → PosReal)
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(hGSupport : ∀ N i, G N i ∈ C) -- @realizes G_i(every deterministic label lies in C)
(hShare : CohortShareLimit T C G pi)
(hMean : UnitUntreatedExponentialMean T Omega P Y b gamma)
(hBaseline : WithinCohortBaselineLimit T C G b barB)
(hEffects : ProportionalEffects T Omega P Y G delta)
(hRank : CollapsedDesignRank T C pi)
(hScope : MulticohortFrontierScope T C)
(hPositive : StrictPositiveEffects T C delta) :
let Phi := frontierEliminationHandle T C pi barB gamma delta
let m : Cell T → ℝ := fun z => observedCohortMean T barB gamma delta z.1 z.2
(betaStar T C pi barB gamma delta < 0 ↔ Phi < 0) ∧
(betaStar T C pi barB gamma delta = 0 ↔ Phi = 0) ∧
(0 < betaStar T C pi barB gamma delta ↔ 0 < Phi) ∧
((restrictSignReversalPrimitive T C pi barB gamma delta ∈
signReversalRegion T C gamma) ↔ Phi < 0) ∧
(∀ x y : ℝ, 1 < x → 1 < y →
frontierEliminationHandle 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma (fourMultiplierEffects x y) =
(5 * x ^ 2 + 12 * x - 2 * y - 15) / 16) ∧
((5 * ((101 : ℝ) / 100) ^ 2 + 12 * ((101 : ℝ) / 100) - 15) / 2 =
(4441 : ℝ) / 4000) ∧
frontierEliminationHandle 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma fourCohortDelta = -(11559 : ℝ) / 32000 ∧
(∀ z ∈ treatedCells T C,
observedCounterfactualBaseline T hT m z.1.1 z.2 = untreatedMean T barB gamma z.1.1 z.2 ∧
granularTau T hT m z.1.1 z.2 = exp (delta (z.1.1, z.2)) - 1 ∧
0 < pttWeight T C hT pi m z) ∧
(∑ z ∈ treatedCells T C, pttWeight T C hT pi m z) = 1 ∧
counterfactualSharePTT T C hT pi m =
(∑ z ∈ treatedCells T C, limitingCellMass T pi z.1.1 * m (z.1.1, z.2)) /
(∑ z ∈ treatedCells T C, limitingCellMass T pi z.1.1 *
observedCounterfactualBaseline T hT m z.1.1 z.2) - 1 ∧
(Phi < 0 → betaStar T C pi barB gamma delta < 0 ∧
0 < counterfactualSharePTT T C hT pi m) := by
dsimp only
have hTpos : 0 < T := lt_of_lt_of_le (by norm_num) hHorizon
have hsign := betaStar_sign_frontierEliminationHandle T C hTpos hSupport.1
pi barB gamma delta hRank
have hDzero (g : Cohort T) (hg : g ∈ C) :
treatmentIndicator T g ⟨0, hT⟩ = 0 := by
induction g using WithTop.recTopCoe with
| top => simp [treatmentIndicator, absorbingTreatment_eq]
| coe g =>
have hg0 := hSupport.2 g hg
rw [treatmentIndicator, absorbingTreatment_eq]
simp only [ite_eq_right_iff]
intro hle
have hle' : g ≤ (⟨0, hT⟩ : Fin T) := by simpa using hle
have hval := Fin.le_iff_val_le_val.mp hle'
have hzero : (⟨0, hT⟩ : Fin T).val = 0 := rfl
have : g.val = 0 := Nat.eq_zero_of_le_zero (by simpa [hzero] using hval)
exact (hg0 this).elim
have hDtop (t : Fin T) : treatmentIndicator T ⊤ t = 0 := by
simp [treatmentIndicator, absorbingTreatment_eq]
have hgamma0 : gamma ⟨0, hT⟩ = 0 := hMean.2 _ rfl
have hbase (g : Cohort T) (hg : g ∈ C) (t : Fin T) :
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) g t =
untreatedMean T barB gamma g t := by
unfold observedCounterfactualBaseline observedCohortMean untreatedMean
dsimp only
rw [hDzero g hg, hDtop t, hDtop ⟨0, hT⟩, hgamma0]
simp only [zero_mul, Real.exp_zero, mul_one]
field_simp [ne_of_gt (barB ⊤).property]
have htreated : (treatedCells T C).Nonempty := by
obtain ⟨g, hgval, hgC⟩ := hScope.1
let t : Fin T := ⟨1, by omega⟩
have hD : treatmentIndicator T (g : Cohort T) t = 1 := by
rw [treatmentIndicator, absorbingTreatment_eq]
have hle : (g : Cohort T) ≤ (t : Cohort T) := by
simp only [WithTop.coe_le_coe]
apply Fin.le_iff_val_le_val.mpr
simp [t, hgval]
simp [hle]
refine ⟨(⟨(g : Cohort T), hgC⟩, t), ?_⟩
simp [treatedCells, hD]
have hnormalizer : 0 < pttNormalizer T C hT pi
(fun z => observedCohortMean T barB gamma delta z.1 z.2) := by
unfold pttNormalizer
apply Finset.sum_pos'
· intro z hz
exact mul_nonneg
(div_nonneg (pi z.1.1).property.1.le (by exact_mod_cast hTpos.le))
(by rw [hbase z.1.1 z.1.2 z.2]; exact (mul_pos
(barB z.1.1).property (Real.exp_pos _)).le)
· obtain ⟨z, hz⟩ := htreated
refine ⟨z, hz, mul_pos ?_ ?_⟩
· exact div_pos (pi z.1.1).property.1 (by exact_mod_cast hTpos)
· rw [hbase z.1.1 z.1.2 z.2]
exact mul_pos (barB z.1.1).property (Real.exp_pos _)
refine ⟨hsign.1, hsign.2.1, hsign.2.2, ?_, ?_, by norm_num, ?_, ?_, ?_, ?_, ?_⟩
· constructor
· intro hmem
have hb := hmem.2.2.2.2.2.2.2
rw [primitiveBetaStar_restrict] at hb
exact hsign.1.mp hb
· intro hPhi
unfold signReversalRegion
refine ⟨hHorizon, hSupport, hScope,
cohortShareLimit_sum_eq_one T C G pi hGSupport hShare, ?_, ?_, ?_, ?_⟩
· refine ⟨fun g => barB g.1, ?_⟩
intro z
rfl
· intro z
exact hPositive z.1.1.1 z.1.1.2 z.1.2 z.2
· intro a ha
rw [Fintype.sum_prod_type]
change 0 < ∑ z : ↑C, ∑ t : Fin T, (pi z.1 : ℝ) / T *
collapsedIndex T C (collapsedRegressor T C z.1 t) a ^ 2
have hr := hRank a ha
rw [show (∑ z : ↑C, ∑ t : Fin T,
(pi z.1 : ℝ) / T *
collapsedIndex T C (collapsedRegressor T C z.1 t) a ^ 2) =
∑ g ∈ C, ∑ t : Fin T, (pi g : ℝ) / T *
collapsedIndex T C (collapsedRegressor T C g t) a ^ 2 by
simpa using Finset.sum_attach (s := C) (f := fun g => ∑ t : Fin T,
(pi g : ℝ) / T *
collapsedIndex T C (collapsedRegressor T C g t) a ^ 2)]
simpa [limitingCellMass] using hr
· rw [primitiveBetaStar_restrict]
exact hsign.1.mpr hPhi
· intro x y hx hy
simp [frontierEliminationHandle, primitiveTotal, primitiveTreatedTotal,
primitiveRow, primitiveColumn, primitiveH, fourCohortSupport, fourCohortShare,
fourCohortLimitBaseline, fourCohortGamma, fourMultiplierEffects,
untreatedMean, treatmentIndicator,
absorbingTreatment_eq]
norm_num [Fin.sum_univ_succ]
simp [Real.exp_log (lt_trans zero_lt_one hx),
Real.exp_log (lt_trans zero_lt_one hy)]
ring
· have hp := show frontierEliminationHandle 4 fourCohortSupport fourCohortShare
fourCohortLimitBaseline fourCohortGamma
(fourMultiplierEffects ((101 : ℝ) / 100) 4) =
(5 * ((101 : ℝ) / 100) ^ 2 + 12 * ((101 : ℝ) / 100) - 2 * 4 - 15) / 16 by
simp [frontierEliminationHandle, primitiveTotal, primitiveTreatedTotal,
primitiveRow, primitiveColumn, primitiveH, fourCohortSupport, fourCohortShare,
fourCohortLimitBaseline, fourCohortGamma, fourMultiplierEffects,
untreatedMean, treatmentIndicator,
absorbingTreatment_eq]
norm_num [Fin.sum_univ_succ]
simp [Real.exp_log (by norm_num : (0 : ℝ) < 101 / 100),
Real.exp_log (by norm_num : (0 : ℝ) < 4)]
ring
rw [show fourCohortDelta = fourMultiplierEffects ((101 : ℝ) / 100) 4 by
funext z
simp [fourCohortDelta, fourMultiplierEffects]]
rw [hp]
norm_num
· intro z hz
have hD : treatmentIndicator T z.1.1 z.2 = 1 :=
(Finset.mem_filter.mp hz).2
refine ⟨hbase z.1.1 z.1.2 z.2, ?_, ?_⟩
· unfold granularTau
rw [hbase z.1.1 z.1.2 z.2]
unfold observedCohortMean
dsimp only
rw [hD, one_mul]
have hB : untreatedMean T barB gamma z.1.1 z.2 ≠ 0 := by
exact ne_of_gt (mul_pos (barB z.1.1).property (Real.exp_pos _))
field_simp
· unfold pttWeight
exact div_pos (mul_pos
(div_pos (pi z.1.1).property.1 (by exact_mod_cast hTpos))
(by rw [hbase z.1.1 z.1.2 z.2]; exact
mul_pos (barB z.1.1).property (Real.exp_pos _))) hnormalizer
· unfold pttWeight
rw [← Finset.sum_div]
change pttNormalizer T C hT pi
(fun z => observedCohortMean T barB gamma delta z.1 z.2) /
pttNormalizer T C hT pi
(fun z => observedCohortMean T barB gamma delta z.1 z.2) = 1
exact div_self (ne_of_gt hnormalizer)
· unfold counterfactualSharePTT pttWeight pttNormalizer granularTau
have hZ : (∑ z ∈ treatedCells T C,
limitingCellMass T pi z.1.1 *
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z.1.1 z.2) ≠ 0 :=
ne_of_gt hnormalizer
rw [show (∑ z ∈ treatedCells T C,
limitingCellMass T pi z.1.1 *
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z.1.1 z.2 /
(∑ w ∈ treatedCells T C, limitingCellMass T pi w.1.1 *
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) w.1.1 w.2) *
(observedCohortMean T barB gamma delta z.1.1 z.2 /
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z.1.1 z.2 - 1)) =
(∑ z ∈ treatedCells T C,
(limitingCellMass T pi z.1.1 *
observedCohortMean T barB gamma delta z.1.1 z.2 /
(∑ w ∈ treatedCells T C, limitingCellMass T pi w.1.1 *
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) w.1.1 w.2) -
limitingCellMass T pi z.1.1 *
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z.1.1 z.2 /
(∑ w ∈ treatedCells T C, limitingCellMass T pi w.1.1 *
observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) w.1.1 w.2))) by
apply Finset.sum_congr rfl
intro z hz
have hB : observedCounterfactualBaseline T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z.1.1 z.2 ≠ 0 := by
rw [hbase z.1.1 z.1.2 z.2]
exact ne_of_gt (mul_pos (barB z.1.1).property (Real.exp_pos _))
field_simp
]
rw [Finset.sum_sub_distrib]
rw [← Finset.sum_div, ← Finset.sum_div]
rw [div_self hZ]
· intro hPhi
refine ⟨hsign.1.mpr hPhi, ?_⟩
unfold counterfactualSharePTT
apply Finset.sum_pos'
· intro z hz
have hD : treatmentIndicator T z.1.1 z.2 = 1 := (Finset.mem_filter.mp hz).2
have hw : 0 < pttWeight T C hT pi
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z := by
unfold pttWeight
exact div_pos (mul_pos
(div_pos (pi z.1.1).property.1 (by exact_mod_cast hTpos))
(by rw [hbase z.1.1 z.1.2 z.2]; exact
mul_pos (barB z.1.1).property (Real.exp_pos _))) hnormalizer
have htau : 0 < granularTau T hT
(fun z => observedCohortMean T barB gamma delta z.1 z.2) z.1.1 z.2 := by
unfold granularTau
rw [hbase z.1.1 z.1.2 z.2]
unfold observedCohortMean
dsimp only
rw [hD, one_mul]
have hd := hPositive z.1.1 z.1.2 z.2 hD
have he : 1 < exp (delta (z.1.1, z.2)) := by simpa using Real.exp_lt_exp.mpr hd
have hB : untreatedMean T barB gamma z.1.1 z.2 ≠ 0 := by
exact ne_of_gt (mul_pos (barB z.1.1).property (Real.exp_pos _))
field_simp
exact sub_pos.mpr he
exact (mul_pos hw htau).le
· obtain ⟨z, hz⟩ := htreated
refine ⟨z, hz, ?_⟩
-- … truncated; follow the source link for the rest …
Projection 3 declarations Existence, uniqueness, and score characterization of the collapsed PPML projection.
Existence, uniqueness, and score characterization of the collapsed PPML projection.
The collapsed design as a linear map into its finite supported-cell table.
Definition (Lean source)
noncomputable def collapsedDesignMap (T : ℕ) (C : Finset (Cohort T)) :
CollapsedParameter T C →ₗ[ℝ] (SupportedCell T C → ℝ) :=
{ toFun := fun theta z =>
collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) theta
map_add' := by
intro x y
funext z
unfold collapsedIndex
simp [mul_add, Finset.sum_add_distrib]
ring
map_smul' := by
intro c x
funext z
unfold collapsedIndex
change (∑ j, _ * (c * x.1 j)) + _ * (c * x.2) = c * ((∑ j, _ * x.1 j) + _ * x.2)
rw [mul_add, Finset.mul_sum]
congr 1
· apply Finset.sum_congr rfl
intro j hj
ring
· ring }
theorem limitingCriterion_eq_finitePoissonObjective
The nested cohort/time criterion is the generic finite Poisson objective on the supported-cell product.
Formal statement
hypotheses
conclusion
limitingCriterion T C pi barB gamma delta theta
= finitePoissonObjective (fun z : SupportedCell T C => limitingCellMass T pi z.1.1) (fun z : SupportedCell T C => observedCohortMean T barB gamma delta z.1.1 z.2) (collapsedDesignMap T C) theta
Proof (Lean source)
lemma limitingCriterion_eq_finitePoissonObjective (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ) (theta : CollapsedParameter T C) :
limitingCriterion T C pi barB gamma delta theta =
finitePoissonObjective
(fun z : SupportedCell T C => limitingCellMass T pi z.1.1)
(fun z : SupportedCell T C => observedCohortMean T barB gamma delta z.1.1 z.2)
(collapsedDesignMap T C) theta := by
classical
rw [limitingCriterion, finitePoissonObjective, Fintype.sum_prod_type]
rw [← Finset.sum_attach]
rfl
The pseudo-true collapsed parameter is unique and solves every score equation.
Formal statement
hypotheses
conclusion
IsUniqueGlobalMax (limitingCriterion T C pi barB gamma delta) (collapsedPopulationProjection T C pi barB gamma delta) ∧
(∀ j : CollapsedNuisanceIndex T C, ∑ g ∈ C, ∑ t : Fin T, limitingCellMass T pi g * collapsedNuisanceRegressor T C g t j * (observedCohortMean T barB gamma delta g t - fittedMean T C pi barB gamma delta g t) = 0) ∧
∑ g ∈ C, ∑ t : Fin T, limitingCellMass T pi g * treatmentIndicator T g t * (observedCohortMean T barB gamma delta g t - fittedMean T C pi barB gamma delta g t)
= 0
Proof (Lean source)
lemma pseudo_true_ppml_projection (T : ℕ) (C : Finset (Cohort T))
(pi : Cohort T → OpenUnit) (barB : Cohort T → PosReal)
(gamma : Fin T → ℝ) (delta : Cell T → ℝ)
(hRank : CollapsedDesignRank T C pi) :
IsUniqueGlobalMax (limitingCriterion T C pi barB gamma delta)
(collapsedPopulationProjection T C pi barB gamma delta) ∧
(∀ j : CollapsedNuisanceIndex T C,
∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g * collapsedNuisanceRegressor T C g t j *
(observedCohortMean T barB gamma delta g t -
fittedMean T C pi barB gamma delta g t) = 0) ∧
∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g * treatmentIndicator T g t *
(observedCohortMean T barB gamma delta g t -
fittedMean T C pi barB gamma delta g t) = 0 := by
classical
have hT : 0 < T := by
by_contra h
have hT0 : T = 0 := Nat.eq_zero_of_not_pos h
subst T
have hr := hRank (0, 1) (by simp)
simp [CollapsedDesignRank] at hr
have hC : C.Nonempty := by
by_contra h
have hC0 : C = ∅ := Finset.not_nonempty_iff_eq_empty.mp h
subst C
have hr := hRank (0, 1) (by simp)
simp [CollapsedDesignRank] at hr
let q : SupportedCell T C → ℝ := fun z => limitingCellMass T pi z.1.1
let m : SupportedCell T C → ℝ := fun z =>
observedCohortMean T barB gamma delta z.1.1 z.2
let A := collapsedDesignMap T C
have hq : ∀ z, 0 < q z := by
intro z
exact div_pos (pi z.1.1).property.1 (by exact_mod_cast hT)
have hm : ∀ z, 0 < m z := by
intro z
exact mul_pos (mul_pos (barB z.1.1).property (Real.exp_pos _)) (Real.exp_pos _)
have hA : Injective A := by
intro x y hxy
by_contra hne
have hsub : x - y ≠ 0 := sub_ne_zero.mpr hne
have hr := hRank (x - y) hsub
have hmap : A (x - y) = 0 := by rw [map_sub, hxy, sub_self]
have hzero :
(∑ g ∈ C, ∑ t : Fin T,
limitingCellMass T pi g *
(collapsedIndex T C (collapsedRegressor T C g t) (x - y)) ^ 2) = 0 := by
apply Finset.sum_eq_zero
intro g hg
apply Finset.sum_eq_zero
intro t ht
have hz := congrFun hmap (⟨g, hg⟩, t)
change collapsedIndex T C (collapsedRegressor T C g t) (x - y) = 0 at hz
rw [hz]
simp
linarith
letI : Nonempty (SupportedCell T C) :=
⟨(⟨hC.choose, hC.choose_spec⟩, ⟨0, hT⟩)⟩
obtain ⟨xstar, hxmax, hxunique⟩ :=
finitePoissonObjective_exists_unique_max q m A hq hm hA
have hcriterion (theta : CollapsedParameter T C) :
limitingCriterion T C pi barB gamma delta theta =
finitePoissonObjective q m A theta := by
exact limitingCriterion_eq_finitePoissonObjective T C pi barB gamma delta theta
have hlimmax : ∀ y, limitingCriterion T C pi barB gamma delta y ≤
limitingCriterion T C pi barB gamma delta xstar := by
intro y
simpa only [hcriterion] using hxmax y
have hexists : ∃ x, ∀ y, limitingCriterion T C pi barB gamma delta y ≤
limitingCriterion T C pi barB gamma delta x := ⟨xstar, hlimmax⟩
have hprojection : collapsedPopulationProjection T C pi barB gamma delta = xstar := by
rw [collapsedPopulationProjection, maximizerOrZero, dif_pos hexists]
apply hxunique
intro y
rw [← hcriterion, ← hcriterion]
exact Classical.choose_spec hexists y
have hisUnique : IsUniqueGlobalMax (limitingCriterion T C pi barB gamma delta)
(collapsedPopulationProjection T C pi barB gamma delta) := by
rw [hprojection]
refine ⟨hlimmax, ?_⟩
intro y hy
apply hxunique
intro z
rw [← hcriterion, ← hcriterion]
exact (hlimmax z).trans_eq hy.symm
have hscore (d : CollapsedParameter T C) :
∑ z : SupportedCell T C,
q z * A d z * (m z - exp (A xstar z)) = 0 :=
finitePoissonObjective_score q m A xstar d hxmax
refine ⟨hisUnique, ?_, ?_⟩
· intro j
let d : CollapsedParameter T C := (fun k => if k = j then 1 else 0, 0)
have hs := hscore d
have hd (z : SupportedCell T C) : A d z =
collapsedNuisanceRegressor T C z.1.1 z.2 j := by
change (∑ k, collapsedNuisanceRegressor T C z.1.1 z.2 k *
(if k = j then 1 else 0)) + treatmentIndicator T z.1.1 z.2 * 0 = _
rw [Fintype.sum_eq_single j]
· simp
· intro k hk
simp [hk]
have hx (z : SupportedCell T C) : A xstar z =
collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) xstar := rfl
simp only [hd, hx] at hs
rw [Fintype.sum_prod_type] at hs
rw [← Finset.sum_attach]
simpa [q, m, fittedMean, hprojection] using hs
· let d : CollapsedParameter T C := (0, 1)
have hs := hscore d
have hd (z : SupportedCell T C) : A d z = treatmentIndicator T z.1.1 z.2 := by
simp [A, d, collapsedDesignMap, collapsedIndex, collapsedRegressor]
have hx (z : SupportedCell T C) : A xstar z =
collapsedIndex T C (collapsedRegressor T C z.1.1 z.2) xstar := rfl
simp only [hd, hx] at hs
rw [Fintype.sum_prod_type] at hs
rw [← Finset.sum_attach]
simpa [q, m, fittedMean, hprojection] using hs