Mathlib
Mathlib-shaped helper lemmas staged for upstreaming: conditional distributions, conditional independence, and integration gaps.
AlgebraicGeometry 28 core · 42 supporting · 1 submodule Algebraic-geometry infrastructure for affine Zariski closures, coordinate rings, and exact dimension of polynomial images. Analysis 196 to review
271 core · 292 supporting · 19 submodules Analysis helpers staged for upstreaming: Bernoulli KL inequalities, functional-equation facts, scalar arithmetic, half-disc polar integration, and one-dimensional smooth descent bounds. CondIndep 8 core · 7 supporting · 3 submodules This file gathers conditional-independence tools used across the causal library, including conditional-expectation identities, almost-everywhere transfer under overlap, and integrability facts. InformationTheory 6 to review
27 core · 60 supporting · 8 submodules Information-theoretic helpers staged for Mathlib: KL divergence under binding/composition, common-statistic Bernoulli kernels, and the product-KL ingredients of Le Cam two-point arguments. LinearAlgebra 21 core · 28 supporting · 5 submodules Linear-algebra helpers staged for Mathlib: monomial-matrix and generalized-permutation lemmas used by causal-discovery identification proofs. MeasureTheory 8 to review
36 core · 37 supporting · 13 submodules Measure-theoretic helpers staged for Mathlib: integral-bind lemmas for kernel compositions. Optimization 24 core · 15 supporting · 11 submodules Optimization helpers staged for Mathlib: weighted-simplex KKT certificates, active-set minimizers, truncation reductions, and boundary-slice selectors. Probability 37 to review
81 core · 157 supporting · 14 submodules Probability helpers staged for Mathlib: Bernoulli and signed two-point laws, Gaussian calculations, convergence in distribution, kernel composition, finite marked Poisson experiments, and Stein-method CLT tools.
CondDistrib 3 core · 1 supporting This file proves general-purpose lemmas for conditional distributions under measurable equivalences and disintegration through bind form. ★ map_compProd_prodMap_left_eq_compProd_comap★ measure_eq_bind_marginal_condDistrib★ condDistrib_map_comp
Conditional-Distribution Transport Lemmas
This file proves general-purpose lemmas for conditional distributions under measurable equivalences and disintegration through bind form. The statements are independent of the causal-model infrastructure and serve as Mathlib-adjacent measure-theoretic support for identification proofs.
The exported results are map_compProd_prodMap_left_eq_compProd_comap,
condDistrib_comp_right_measurableEquiv,
measure_eq_bind_marginal_condDistrib, and condDistrib_map_comp. Together
they move regular conditional distributions across measurable equivalences,
package finite-measure disintegration as a bind identity, and compare
conditional distributions before and after pushing the source measure forward.
theorem map_compProd_prodMap_left_eq_compProd_comap reviewed
⚑ flagged
Causalean
Pushforward of compProd through a measurable equivalence on the first coordinate. For a measurable equivalence e between the first-coordinate spaces, an s-finite measure ν on the source first coordinate, and an s-finite kernel κ from that coordinate to a second space, pushing the composed-product measure of ν and κ forward through e on the first coordinate (identity on the second) equals the composed-product measure of the pushed-forward ν and κ transported back along e's inverse.
Formal statement
hypotheses
Proof (Lean source)
theorem map_compProd_prodMap_left_eq_compProd_comap
{β β' γ : Type*} [MeasurableSpace β] [MeasurableSpace β']
[MeasurableSpace γ]
(ν : Measure β) [SFinite ν]
(e : β ≃ᵐ β')
(κ : Kernel β γ)
[IsSFiniteKernel κ] :
map (map e (id : γ → γ)) (ν.compProd κ)
= (map e ν).compProd
(κ.comap e.symm e.symm.measurable) := by
ext s hs
rw [MeasureTheory.Measure.map_apply
(e.measurable.prodMap measurable_id) hs]
rw [MeasureTheory.Measure.compProd_apply
(e.measurable.prodMap measurable_id hs)]
rw [MeasureTheory.Measure.compProd_apply hs]
rw [MeasureTheory.lintegral_map
(ProbabilityTheory.Kernel.measurable_kernel_prodMk_left hs)
e.measurable]
apply MeasureTheory.lintegral_congr
intro b
rw [ProbabilityTheory.Kernel.comap_apply, e.symm_apply_apply]
rfl
theorem measure_eq_bind_marginal_condDistrib reviewed
⚑ flagged
Causalean
Measure-theoretic chain rule / disintegration (Mathlib gap). For a finite measure μ on a product space, μ equals the composition obtained by first drawing the second coordinate from its marginal distribution and then drawing the first coordinate from its regular conditional distribution given that second coordinate.
Formal statement
hypotheses
β γ :
μ :
Measure (β × γ)
Proof (Lean source)
theorem measure_eq_bind_marginal_condDistrib
{β γ : Type*} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
[StandardBorelSpace β] [Nonempty β]
(μ : Measure (β × γ))
[IsFiniteMeasure μ] :
μ = (μ.map Prod.snd).bind
(fun c : γ =>
(ProbabilityTheory.condDistrib Prod.fst Prod.snd μ c).map
(fun b : β => (b, c))) := by
classical
let κ : Kernel γ β :=
ProbabilityTheory.condDistrib Prod.fst Prod.snd μ
have hcomp :
map Prod.snd μ ⊗ₘ κ
= map (fun p : β × γ => (p.2, p.1)) μ := by
simpa [κ] using
(ProbabilityTheory.compProd_map_condDistrib
(μ := μ) (X := Prod.snd) (Y := Prod.fst) (by fun_prop))
have hswap :
μ = map swap
(map (fun p : β × γ => (p.2, p.1)) μ) := by
rw [MeasureTheory.Measure.map_map measurable_swap]
· simp [Function.comp_def]
· fun_prop
have hprod_swap :
((ProbabilityTheory.Kernel.id ×ₖ κ).map swap)
= (κ ×ₖ ProbabilityTheory.Kernel.id) := by
ext c
rw [ProbabilityTheory.Kernel.map_apply _ measurable_swap,
ProbabilityTheory.Kernel.prod_apply,
ProbabilityTheory.Kernel.prod_apply,
MeasureTheory.Measure.prod_swap]
have hkernel :
(fun c : γ => map (fun b : β => (b, c)) (κ c))
=ᵐ[map Prod.snd μ]
((κ ×ₖ ProbabilityTheory.Kernel.id)) := by
filter_upwards with c
rw [ProbabilityTheory.Kernel.prod_apply]
exact (MeasureTheory.Measure.prod_dirac (μ := κ c) c).symm
simpa [κ] using (calc
μ = map swap
(map (fun p : β × γ => (p.2, p.1)) μ) := hswap
_ = map swap
(map Prod.snd μ ⊗ₘ κ) := by
rw [hcomp]
_ = (κ ×ₖ ProbabilityTheory.Kernel.id) ∘ₘ
map Prod.snd μ := by
rw [MeasureTheory.Measure.compProd_eq_comp_prod]
rw [MeasureTheory.Measure.map_comp _ _ measurable_swap]
rw [hprod_swap]
_ = (fun c : γ =>
map (fun b : β => (b, c)) (κ c)) ∘ₘ
map Prod.snd μ := by
exact MeasureTheory.Measure.bind_congr_right hkernel.symm)
theorem condDistrib_map_comp reviewed
⚑ flagged
Causalean
Reparameterization of condDistrib through a pushforward. For a measurable map φ from the sample space Ω to Ω', a measurable outcome map g, and a measurable conditioning map f, the conditional distribution of g given f, computed under the pushforward of μ by φ, agrees almost everywhere on the f-marginal with the conditional distribution of the pullbacks g ∘ φ given f ∘ φ, computed under μ directly.
Formal statement
hypotheses
Ω Ω' 𝒳 𝒴 :
Type*
Nonempty 𝒴
μ :
φ :
Ω → Ω'
g :
Ω' → 𝒴
f :
Ω' → 𝒳
hφ :
hg :
hf :
conclusion
condDistrib g f (μ.map φ)
=ᵐ[(μ.map φ).map f] condDistrib (g ∘ φ) (f ∘ φ) μ
Proof (Lean source)
theorem condDistrib_map_comp
{Ω Ω' 𝒳 𝒴 : Type*}
[MeasurableSpace Ω] [MeasurableSpace Ω'] [MeasurableSpace 𝒳]
[MeasurableSpace 𝒴] [StandardBorelSpace 𝒴] [Nonempty 𝒴]
(μ : Measure Ω) [IsFiniteMeasure μ]
{φ : Ω → Ω'} {g : Ω' → 𝒴} {f : Ω' → 𝒳}
(hφ : Measurable φ) (hg : Measurable g) (hf : Measurable f) :
condDistrib g f (μ.map φ)
=ᵐ[(μ.map φ).map f] condDistrib (g ∘ φ) (f ∘ φ) μ := by
haveI : IsFiniteMeasure (μ.map φ) := μ.isFiniteMeasure_map φ
refine ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable
hf hg ?_
have h1 : (μ.map φ).map (fun x => (f x, g x))
= μ.map (fun ω => ((f ∘ φ) ω, (g ∘ φ) ω)) := by
rw [MeasureTheory.Measure.map_map (hf.prodMk hg) hφ]; rfl
have h2 : (μ.map φ).map f = μ.map (f ∘ φ) :=
MeasureTheory.Measure.map_map hf hφ
rw [h1, h2]
exact (ProbabilityTheory.compProd_map_condDistrib (hg.comp hφ).aemeasurable).symm
1 supporting declaration (lemmas, instances)
-
condDistrib_comp_right_measurableEquivtheorem — Push-forward invariance of condDistrib under a measurable equivalence of the conditioning variable.hypothesesα β Ω γ :Type*Nonempty Ωμ :Y :γ → ΩX :γ → αe :α ≃ᵐ βhY :hX :conclusion∀ᵐ x ∂(μ.map X),condDistrib Y (e ∘ X) μ (e x) = condDistrib Y X μ xProof (Lean source)
theorem condDistrib_comp_right_measurableEquiv {α β Ω γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mΩ : MeasurableSpace Ω} [StandardBorelSpace Ω] [Nonempty Ω] {mγ : MeasurableSpace γ} (μ : Measure γ) [IsFiniteMeasure μ] {Y : γ → Ω} {X : γ → α} (e : α ≃ᵐ β) (hY : Measurable Y) (hX : Measurable X) : ∀ᵐ x ∂(μ.map X), ProbabilityTheory.condDistrib Y (e ∘ X) μ (e x) = ProbabilityTheory.condDistrib Y X μ x := by classical set κ : Kernel α Ω := ProbabilityTheory.condDistrib Y X μ with hκ_def set κ' : Kernel β Ω := κ.comap e.symm e.symm.measurable with hκ'_def -- (1) Pushforward of the joint `(X, Y)` map under `(e × id)`. have hpush : map (fun a => ((e ∘ X) a, Y a)) μ = map (map e (id : Ω → Ω)) (map (fun a => (X a, Y a)) μ) := by rw [MeasureTheory.Measure.map_map (e.measurable.prodMap measurable_id) (hX.prodMk hY)] rfl -- (2) Compose with `compProd_map_condDistrib` and the pushforward lemma -- `map_compProd_prodMap_left_eq_compProd_comap` to express the -- `(e ∘ X, Y)`-pushforward as a compProd against `κ'`. have hcompProd_eX : map (fun a => ((e ∘ X) a, Y a)) μ = (map (e ∘ X) μ).compProd κ' := by rw [hpush, ← ProbabilityTheory.compProd_map_condDistrib (X := X) hY.aemeasurable, map_compProd_prodMap_left_eq_compProd_comap (map X μ) e κ] congr 1 exact MeasureTheory.Measure.map_map e.measurable hX -- (3) Uniqueness of disintegration gives ae-equality of `κ'` with -- `condDistrib Y (e ∘ X) μ` under `μ.map (e ∘ X)`. have hae : (fun b => ProbabilityTheory.condDistrib Y (e ∘ X) μ b) =ᵐ[map (e ∘ X) μ] κ' := ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd (e ∘ X) hY.aemeasurable hcompProd_eX -- (4) Transport the ae-equality through `e`. Since -- `μ.map (e ∘ X) = (μ.map X).map e`, an a.e. statement on the former -- becomes an a.e. statement on `μ.map X` after precomposing with `e`. have hmap : map (e ∘ X) μ = map e (map X μ) := (MeasureTheory.Measure.map_map e.measurable hX).symm rw [hmap] at hae have hae' : ∀ᵐ x ∂(map X μ), ProbabilityTheory.condDistrib Y (e ∘ X) μ (e x) = κ' (e x) := MeasureTheory.ae_of_ae_map (μ := map X μ) (f := e) e.measurable.aemeasurable hae -- (5) Finally, `κ' (e x) = κ (e.symm (e x)) = κ x`. filter_upwards [hae'] with x hx rw [hx, hκ'_def, ProbabilityTheory.Kernel.comap_apply, e.symm_apply_apply]
CondDistribWitness 3 core · 2 supporting This file states the measure-theoretic core of a backdoor or Rule-2 argument purely in terms of Mathlib's conditional distributions, with no SCM machinery. ★ condDistrib_map_of_condDistrib_fst_eq★ condDistrib_map_of_funext
Witness-kernel form of conditional distributions
This file states the measure-theoretic core of a backdoor or Rule-2 argument purely in terms of Mathlib's conditional distributions, with no SCM machinery. When an outcome is a measurable function of the conditioning variable and a residual coordinate, its conditional law is the pushforward of the residual coordinate's conditional law by that function.
The main construction is witnessKernel, a Markov kernel sending a treatment-
covariate pair to the residual conditional law pushed through a structural
response. The theorem condDistrib_map_of_condDistrib_fst_eq proves this
witness-kernel form under a conditional-independence hypothesis, while
condDistrib_map_of_funext gives the no-treatment specialization where the
conditioning variable already contains the full non-residual information.
def witnessKernel reviewed
⚑ flagged
ProbabilityTheory
For each treatment-covariate pair, this kernel gives the conditional law of the outcome obtained by drawing the residual coordinate from its conditional law given the covariates and then applying the structural response function.
Definition (Lean source)
noncomputable def witnessKernel (μ : Measure Ω) [IsFiniteMeasure μ]
{Z : Ω → 𝒵} {C : Ω → 𝒞} {h : 𝒳 → 𝒵 → 𝒞 → 𝒴}
(hh : Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)) :
Kernel (𝒳 × 𝒵) 𝒴 where
toFun p := (condDistrib C Z μ p.2).map (h p.1 p.2)
measurable' := by
-- Measurability of `c ↦ h p.1 p.2 c` for fixed `p`, derived from the joint measurability `hh`.
have hhp : ∀ p : 𝒳 × 𝒵, Measurable (h p.1 p.2) := fun p =>
hh.comp (measurable_const.prodMk measurable_id)
refine Measure.measurable_of_measurable_coe _ (fun B hB => ?_)
-- `((condDistrib C Z μ p.2).map (h p.1 p.2)) B = (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B)`
have hmap : ∀ p : 𝒳 × 𝒵,
((condDistrib C Z μ p.2).map (h p.1 p.2)) B
= (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) := by
intro p
rw [Measure.map_apply (hhp p) hB]
simp_rw [hmap]
-- Express the inner measure as a kernel lintegral and use measurability of the integrand.
set κ' : Kernel (𝒳 × 𝒵) 𝒞 :=
(condDistrib C Z μ).comap (Prod.snd : 𝒳 × 𝒵 → 𝒵) measurable_snd with hκ'
have hker : ∀ p : 𝒳 × 𝒵,
(condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B)
= ∫⁻ c, B.indicator (1 : 𝒴 → ℝ≥0∞) (h p.1 p.2 c) ∂(κ' p) := by
intro p
rw [hκ', Kernel.comap_apply, ← lintegral_indicator_one ((hhp p) hB)]
refine lintegral_congr (fun c => ?_)
by_cases hc : h p.1 p.2 c ∈ B <;> simp [Set.mem_preimage, hc]
simp_rw [hker]
refine Measurable.lintegral_kernel_prod_right ?_
-- `(p, c) ↦ B.indicator 1 (h p.1 p.2 c)` is measurable from `hh`.
exact (measurable_const.indicator hB).comp hh
theorem condDistrib_map_of_condDistrib_fst_eq reviewed
⚑ flagged
ProbabilityTheory
Witness-kernel form of a conditional distribution under conditional independence. For measurable maps X, Z, and C and a jointly measurable structural-response function h, if the conditional distribution of C given the pair (X,Z) agrees almost everywhere with the conditional distribution of C given Z alone — conditional independence of C from X given Z, then the conditional distribution of the outcome h(X,Z,C) given (X,Z) agrees almost everywhere with the pushforward, by the map h x z, of the conditional distribution of C given Z.
Formal statement
hypotheses
μ :
X :
Ω → 𝒳
Z :
Ω → 𝒵
C :
Ω → 𝒞
h :
𝒳 → 𝒵 → 𝒞 → 𝒴
hX :
hZ :
hC :
hh :
Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)
hCI :
(fun p : 𝒳 × 𝒵 => condDistrib C (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))] (fun p => condDistrib C Z μ p.2)
conclusion
(fun p : 𝒳 × 𝒵 => condDistrib (fun ω => h (X ω) (Z ω) (C ω)) (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))] (fun p => (condDistrib C Z μ p.2).map (h p.1 p.2))
Proof (Lean source)
theorem condDistrib_map_of_condDistrib_fst_eq
(μ : Measure Ω) [IsFiniteMeasure μ]
{X : Ω → 𝒳} {Z : Ω → 𝒵} {C : Ω → 𝒞} {h : 𝒳 → 𝒵 → 𝒞 → 𝒴}
(hX : Measurable X) (hZ : Measurable Z) (hC : Measurable C)
(hh : Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2))
(hCI : (fun p : 𝒳 × 𝒵 => condDistrib C (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))]
(fun p => condDistrib C Z μ p.2)) :
(fun p : 𝒳 × 𝒵 => condDistrib (fun ω => h (X ω) (Z ω) (C ω)) (fun ω => (X ω, Z ω)) μ p)
=ᵐ[μ.map (fun ω => (X ω, Z ω))]
(fun p => (condDistrib C Z μ p.2).map (h p.1 p.2)) := by
set W : Ω → 𝒳 × 𝒵 := fun ω => (X ω, Z ω) with hW
set Y : Ω → 𝒴 := fun ω => h (X ω) (Z ω) (C ω) with hY
have hWmeas : Measurable W := hX.prodMk hZ
have hYmeas : Measurable Y := by
have : Y = (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2) ∘ (fun ω => (W ω, C ω)) := rfl
rw [this]; exact hh.comp ((hWmeas).prodMk hC)
-- The candidate witness kernel.
set κ : Kernel (𝒳 × 𝒵) 𝒴 := witnessKernel μ (Z := Z) (C := C) hh with hκ
-- It suffices, by uniqueness of `condDistrib`, to verify the disintegration identity.
suffices hgoal : condDistrib Y W μ =ᵐ[μ.map W] κ by
filter_upwards [hgoal] with p hp
rw [hp, hκ, witnessKernel_apply]
refine condDistrib_ae_eq_of_measure_eq_compProd W hYmeas.aemeasurable ?_
-- Verify `μ.map (W, Y) = μ.map W ⊗ₘ κ` on rectangles.
refine Measure.ext_prod (fun {A B} hA hB => ?_)
-- RHS: `(μ.map W ⊗ₘ κ) (A ×ˢ B) = ∫⁻ p in A, κ p B ∂(μ.map W)`.
rw [Measure.compProd_apply_prod hA hB]
-- Rewrite `κ p B` using `condDistrib C Z μ p.2 = condDistrib C W μ p` (a.e. via `hCI`).
have hκB : ∀ p : 𝒳 × 𝒵, κ p B = (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) := by
intro p
have hhp : Measurable (h p.1 p.2) := hh.comp (measurable_const.prodMk measurable_id)
rw [hκ, witnessKernel_apply μ Z C hh, Measure.map_apply hhp hB]
simp_rw [hκB]
-- Replace `condDistrib C Z μ p.2` by `condDistrib C W μ p` on `A` using `hCI`.
have hint : ∫⁻ p in A, (condDistrib C Z μ p.2) ((h p.1 p.2) ⁻¹' B) ∂(μ.map W)
= ∫⁻ p in A, (condDistrib C W μ p) ((h p.1 p.2) ⁻¹' B) ∂(μ.map W) := by
refine lintegral_congr_ae (ae_restrict_of_ae ?_)
filter_upwards [hCI] with p hp
rw [hp]
rw [hint]
-- This integral is `(μ.map W ⊗ₘ condDistrib C W μ)` on `{(p,c) | p ∈ A ∧ h p.1 p.2 c ∈ B}`.
have hCWmarkov : IsMarkovKernel (condDistrib C W μ) := inferInstance
have hset : MeasurableSet {q : (𝒳 × 𝒵) × 𝒞 | q.1 ∈ A ∧ h q.1.1 q.1.2 q.2 ∈ B} := by
apply MeasurableSet.inter
· exact measurable_fst hA
· exact hh hB
have hcompProd :
∫⁻ p in A, (condDistrib C W μ p) ((h p.1 p.2) ⁻¹' B) ∂(μ.map W)
= (μ.map W ⊗ₘ condDistrib C W μ)
{q : (𝒳 × 𝒵) × 𝒞 | q.1 ∈ A ∧ h q.1.1 q.1.2 q.2 ∈ B} := by
rw [Measure.compProd_apply hset]
rw [← lintegral_indicator hA]
refine lintegral_congr (fun p => ?_)
by_cases hpA : p ∈ A
· rw [Set.indicator_of_mem hpA]
congr 1
ext c
simp [hpA]
· rw [Set.indicator_of_notMem hpA]
have : (Prod.mk p ⁻¹' {q : (𝒳 × 𝒵) × 𝒞 | q.1 ∈ A ∧ h q.1.1 q.1.2 q.2 ∈ B}) = ∅ := by
ext c; simp [hpA]
rw [this]; simp
rw [hcompProd, compProd_map_condDistrib hC.aemeasurable]
-- Finally identify with `μ.map (W, Y) (A ×ˢ B)`.
rw [Measure.map_apply (hWmeas.prodMk hC) hset]
rw [Measure.map_apply (hWmeas.prodMk hYmeas) (hA.prod hB)]
-- The two preimage events `{W ∈ A ∧ Y ∈ B}` and `{(W,C) ∈ {q | q.1 ∈ A ∧ h … ∈ B}}` coincide.
congr 1
theorem condDistrib_map_of_funext reviewed
⚑ flagged
ProbabilityTheory
No-treatment witness-kernel form of a conditional distribution. For measurable maps Z and C and a jointly measurable response function H, the conditional distribution of the outcome H(Z,C) given Z agrees almost everywhere with the pushforward, by the map H z, of the conditional distribution of C given Z.
Formal statement
hypotheses
conclusion
(fun z : 𝒵 => condDistrib (fun ω => H (Z ω) (C ω)) Z μ z)
=ᵐ[μ.map Z] (fun z => (condDistrib C Z μ z).map (H z))
Proof (Lean source)
theorem condDistrib_map_of_funext
(μ : Measure Ω) [IsFiniteMeasure μ]
{Z : Ω → 𝒵} {C : Ω → 𝒞} {H : 𝒵 → 𝒞 → 𝒴}
(hZ : Measurable Z) (hC : Measurable C)
(hH : Measurable (fun p : 𝒵 × 𝒞 => H p.1 p.2)) :
(fun z : 𝒵 => condDistrib (fun ω => H (Z ω) (C ω)) Z μ z)
=ᵐ[μ.map Z]
(fun z => (condDistrib C Z μ z).map (H z)) := by
set Y : Ω → 𝒴 := fun ω => H (Z ω) (C ω) with hY
have hYmeas : Measurable Y := by
have : Y = (fun p : 𝒵 × 𝒞 => H p.1 p.2) ∘ (fun ω => (Z ω, C ω)) := rfl
rw [this]; exact hH.comp (hZ.prodMk hC)
-- The candidate witness kernel `z ↦ (condDistrib C Z μ z).map (H z)`.
have hHz : ∀ z : 𝒵, Measurable (H z) := fun z =>
hH.comp (measurable_const.prodMk measurable_id)
let κ : Kernel 𝒵 𝒴 :=
{ toFun := fun z => (condDistrib C Z μ z).map (H z)
measurable' := by
refine Measure.measurable_of_measurable_coe _ (fun B hB => ?_)
have hmap : ∀ z : 𝒵,
((condDistrib C Z μ z).map (H z)) B
= (condDistrib C Z μ z) ((H z) ⁻¹' B) := fun z => by
rw [Measure.map_apply (hHz z) hB]
simp_rw [hmap]
have hker : ∀ z : 𝒵,
(condDistrib C Z μ z) ((H z) ⁻¹' B)
= ∫⁻ c, B.indicator (1 : 𝒴 → ℝ≥0∞) (H z c) ∂(condDistrib C Z μ z) := by
intro z
rw [← lintegral_indicator_one ((hHz z) hB)]
refine lintegral_congr (fun c => ?_)
by_cases hc : H z c ∈ B <;> simp [Set.mem_preimage, hc]
simp_rw [hker]
refine Measurable.lintegral_kernel_prod_right ?_
exact (measurable_const.indicator hB).comp hH }
have hκ_apply : ∀ z, κ z = (condDistrib C Z μ z).map (H z) := fun _ => rfl
haveI hκmarkov : IsMarkovKernel κ := by
constructor
intro z
rw [hκ_apply]
have : IsMarkovKernel (condDistrib C Z μ) := inferInstance
exact Measure.isProbabilityMeasure_map (hHz z).aemeasurable
suffices hgoal : condDistrib Y Z μ =ᵐ[μ.map Z] κ by
filter_upwards [hgoal] with z hz
rw [hz, hκ_apply]
refine condDistrib_ae_eq_of_measure_eq_compProd Z hYmeas.aemeasurable ?_
refine Measure.ext_prod (fun {A B} hA hB => ?_)
rw [Measure.compProd_apply_prod hA hB]
have hκB : ∀ z : 𝒵, κ z B = (condDistrib C Z μ z) ((H z) ⁻¹' B) := by
intro z; rw [hκ_apply]; exact Measure.map_apply (hHz z) hB
simp_rw [hκB]
have hCmarkov : IsMarkovKernel (condDistrib C Z μ) := inferInstance
have hset : MeasurableSet {q : 𝒵 × 𝒞 | q.1 ∈ A ∧ H q.1 q.2 ∈ B} := by
apply MeasurableSet.inter
· exact measurable_fst hA
· exact hH hB
have hcompProd :
∫⁻ z in A, (condDistrib C Z μ z) ((H z) ⁻¹' B) ∂(μ.map Z)
= (μ.map Z ⊗ₘ condDistrib C Z μ)
{q : 𝒵 × 𝒞 | q.1 ∈ A ∧ H q.1 q.2 ∈ B} := by
rw [Measure.compProd_apply hset, ← lintegral_indicator hA]
refine lintegral_congr (fun z => ?_)
by_cases hzA : z ∈ A
· rw [Set.indicator_of_mem hzA]
congr 1; ext c; simp [hzA]
· rw [Set.indicator_of_notMem hzA]
have : (Prod.mk z ⁻¹' {q : 𝒵 × 𝒞 | q.1 ∈ A ∧ H q.1 q.2 ∈ B}) = ∅ := by
ext c; simp [hzA]
rw [this]; simp
rw [hcompProd, compProd_map_condDistrib hC.aemeasurable]
rw [Measure.map_apply (hZ.prodMk hC) hset]
rw [Measure.map_apply (hZ.prodMk hYmeas) (hA.prod hB)]
congr 1
2 supporting declarations (lemmas, instances)
-
witnessKernel_applylemma — Evaluating the witness kernel at a conditioning pair gives the residual conditional law pushed through the corresponding structural slice.hypothesesμ :Z :Ω → 𝒵C :Ω → 𝒞h :𝒳 → 𝒵 → 𝒞 → 𝒴hh :Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)p :𝒳 × 𝒵conclusionProof (Lean source)
@[simp] lemma witnessKernel_apply (μ : Measure Ω) [IsFiniteMeasure μ] (Z : Ω → 𝒵) (C : Ω → 𝒞) {h : 𝒳 → 𝒵 → 𝒞 → 𝒴} (hh : Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)) (p : 𝒳 × 𝒵) : witnessKernel μ (Z := Z) (C := C) hh p = (condDistrib C Z μ p.2).map (h p.1 p.2) := rfl -
instIsMarkovKernel_witnessKernelinstance — The witness kernel is a Markov kernel when the base measure is finite.instance instIsMarkovKernel_witnessKernel (μ : Measure Ω) [IsFiniteMeasure μ] {Z : Ω → 𝒵} {C : Ω → 𝒞} {h : 𝒳 → 𝒵 → 𝒞 → 𝒴} (hh : Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)) : IsMarkovKernel (witnessKernel μ (Z := Z) (C := C) hh) := by constructor intro p rw [witnessKernel_apply] have hhp : Measurable (h p.1 p.2) := hh.comp (measurable_const.prodMk measurable_id) have : IsMarkovKernel (condDistrib C Z μ) := inferInstance exact Measure.isProbabilityMeasure_map hhp.aemeasurable
ConvergenceInDistribution 2 core · 3 supporting This file collects general convergence-in-distribution lemmas that are not specific to the causal-inference layer. ★ const_mul_of_tendsto_const★ tendsto_map_mul_of_tendsto
Convergence in Distribution Helpers
This file collects general convergence-in-distribution lemmas that are not specific to the causal-inference layer. It provides deterministic-scalar Slutsky results for random variables and for weak convergence of probability measures on the real line.
The lemma tendstoInMeasure_const_of_tendsto_real converts ordinary
convergence of deterministic real scalars into convergence in measure for
constant random variables. TendstoInDistribution.const_mul_of_tendsto_const
then proves random-variable Slutsky for deterministic scalar multiplication,
and ProbabilityMeasure.tendsto_map_mul_of_tendsto gives the analogous
probability-measure pushforward theorem.
theorem const_mul_of_tendsto_const reviewed
⚑ flagged
MeasureTheory.TendstoInDistribution
Deterministic-scalar Slutsky theorem for random variables. If a sequence of random variables X n converges in distribution to Z, all under the same probability measure μ and a sequence of deterministic real scalars a n converges to a limit a₀, then the scaled sequence a n · X n converges in distribution to a₀ · Z.
Formal statement
hypotheses
l.IsCountablyGenerated
X :
ι → Ω → ℝ
Z :
Ω → ℝ
a :
ι → ℝ
a₀ :
ℝ
hXZ :
TendstoInDistribution X l Z (fun _ => μ) μ
ha :
Tendsto a l (𝓝 a₀)
conclusion
TendstoInDistribution (fun n ω => a n * X n ω) l (fun ω => a₀ * Z ω) (fun _ => μ) μ
Proof (Lean source)
theorem TendstoInDistribution.const_mul_of_tendsto_const
[IsProbabilityMeasure μ] [l.IsCountablyGenerated]
{X : ι → Ω → ℝ} {Z : Ω → ℝ} {a : ι → ℝ} {a₀ : ℝ}
(hXZ : TendstoInDistribution X l Z (fun _ => μ) μ)
(ha : Tendsto a l (𝓝 a₀)) :
TendstoInDistribution (fun n ω => a n * X n ω) l (fun ω => a₀ * Z ω) (fun _ => μ) μ := by
have hY : TendstoInMeasure μ (fun n => fun _ : Ω => a n) l (fun _ => a₀) :=
tendstoInMeasure_const_of_tendsto_real (μ := μ) ha
have hY_meas : ∀ n, AEMeasurable (fun _ : Ω => a n) μ := by
intro n
fun_prop
simpa using
(hXZ.continuous_comp_prodMk_of_tendstoInMeasure_const
(g := fun p : ℝ × ℝ => p.2 * p.1) (by fun_prop) hY hY_meas)
theorem tendsto_map_mul_of_tendsto reviewed
⚑ flagged
MeasureTheory.ProbabilityMeasure
Measure-level deterministic-scalar Slutsky theorem for weak convergence. For a filter l along which a family of probability measures on the reals converges weakly to a limit measure ν and a family of real scalars converges to a limit a₀, then the pushforwards of the measures by scalar multiplication x ↦ aᵢ·x converge weakly to the pushforward of ν by x ↦ a₀·x.
Formal statement
hypotheses
conclusion
Tendsto (fun i => (νs i).map ((measurable_const.mul measurable_id).aemeasurable : AEMeasurable (fun x : ℝ => a i * x) (νs i : Measure ℝ))) l (𝓝 (ν.map ((measurable_const.mul measurable_id).aemeasurable : AEMeasurable (fun x : ℝ => a₀ * x) (ν : Measure ℝ))))
Proof (Lean source)
theorem tendsto_map_mul_of_tendsto {ι : Type*} {l : Filter ι}
{νs : ι → ProbabilityMeasure ℝ} {ν : ProbabilityMeasure ℝ}
{a : ι → ℝ} {a₀ : ℝ}
(hν : Tendsto νs l (𝓝 ν)) (ha : Tendsto a l (𝓝 a₀)) :
Tendsto
(fun i => (νs i).map ((measurable_const.mul measurable_id).aemeasurable :
AEMeasurable (fun x : ℝ => a i * x) (νs i : Measure ℝ)))
l
(𝓝 (ν.map ((measurable_const.mul measurable_id).aemeasurable :
AEMeasurable (fun x : ℝ => a₀ * x) (ν : Measure ℝ)))) := by
let mulMap : ℝ × ℝ → ℝ := fun p => p.1 * p.2
have hdirac : Tendsto (fun i => diracProba (a i)) l (𝓝 (diracProba a₀)) :=
(continuous_diracProba.tendsto a₀).comp ha
have hprod :
Tendsto (fun i => (diracProba (a i)).prod (νs i)) l
(𝓝 ((diracProba a₀).prod ν)) := by
exact (continuous_prod.tendsto (diracProba a₀, ν)).comp
(hdirac.prodMk_nhds hν)
have hmap :
Tendsto
(fun i => ((diracProba (a i)).prod (νs i)).map
((by fun_prop : Measurable mulMap).aemeasurable))
l
(𝓝 (((diracProba a₀).prod ν).map
((by fun_prop : Measurable mulMap).aemeasurable))) := by
exact tendsto_map_of_tendsto_of_continuous _ _ hprod
(by fun_prop : Continuous mulMap)
simpa [mulMap, map_mul_eq_map_prod_dirac] using hmap
3 supporting declarations (lemmas, instances)
-
tendstoInMeasure_const_of_tendsto_reallemma — A deterministic sequence in a seminormed additive commutative group that converges in the usual topological sense also converges in measure when regarded as a sequence of constant random variables.hypothesesE :ha :Tendsto a l (𝓝 a₀)conclusionTendstoInMeasure μ (fun n => fun _ : Ω => a n) l (fun _ => a₀)Proof (Lean source)
lemma tendstoInMeasure_const_of_tendsto_real {E : Type*} [SeminormedAddCommGroup E] {a : ι → E} {a₀ : E} (ha : Tendsto a l (𝓝 a₀)) : TendstoInMeasure μ (fun n => fun _ : Ω => a n) l (fun _ => a₀) := by rw [tendstoInMeasure_iff_norm] intro ε hε have hev : ∀ᶠ n in l, ‖a n - a₀‖ < ε := by filter_upwards [(Metric.tendsto_nhds.mp ha) ε hε] with n hn simpa [dist_eq_norm] using hn refine tendsto_const_nhds.congr' ?_ filter_upwards [hev] with n hn have hset : {x : Ω | ε ≤ ‖(fun _ : Ω => a n) x - (fun _ : Ω => a₀) x‖} = ∅ := by ext x simp [not_le.mpr hn] rw [hset] simp -
tendstoInMeasure_const_of_tendstolemma — Alias for tendstoInMeasure_const_of_tendsto_real whose name reflects that the result holds in any seminormed additive commutative group.hypothesesE :ha :Tendsto a l (𝓝 a₀)conclusionTendstoInMeasure μ (fun n => fun _ : Ω => a n) l (fun _ => a₀)Proof (Lean source)
lemma tendstoInMeasure_const_of_tendsto {E : Type*} [SeminormedAddCommGroup E] {a : ι → E} {a₀ : E} (ha : Tendsto a l (𝓝 a₀)) : TendstoInMeasure μ (fun n => fun _ : Ω => a n) l (fun _ => a₀) := tendstoInMeasure_const_of_tendsto_real ha -
map_mul_eq_map_prod_diraclemma — Multiplying a deterministic real value and a random draw has the same distribution as scaling that random draw by the deterministic value.hypothesesc :ℝν :conclusion= ν.map ((measurable_const.mul measurable_id).aemeasurable : AEMeasurable (fun x : ℝ => c * x) (ν : Measure ℝ))Proof (Lean source)
lemma map_mul_eq_map_prod_dirac (c : ℝ) (ν : ProbabilityMeasure ℝ) : ((diracProba c).prod ν).map ((by fun_prop : Measurable (fun p : ℝ × ℝ => p.1 * p.2)).aemeasurable) = ν.map ((measurable_const.mul measurable_id).aemeasurable : AEMeasurable (fun x : ℝ => c * x) (ν : Measure ℝ)) := by apply Subtype.ext change Measure.map (fun p : ℝ × ℝ => p.1 * p.2) ((Measure.dirac c).prod (ν : Measure ℝ)) = Measure.map (fun x : ℝ => c * x) (ν : Measure ℝ) rw [Measure.dirac_prod] rw [Measure.map_map] · rfl · fun_prop · fun_prop
ELpNormMeasurable 2 core · 2 supporting This file proves that the parameter map sending a jointly measurable integrand to its finite nonzero Lp norm under a fixed measure is measurable. ★ measurable_eLpNorm_two_toReal_of_uncurry★ measurable_eLpNorm_two_toReal_of_uncurry_of_factor
Measurability of Parametric L2 Norms
This file proves that the parameter map sending a jointly measurable integrand to its finite nonzero Lp norm under a fixed measure is measurable. It supplies a causal-agnostic Tonelli-based measurability tool for empirical-process and sample-splitting arguments.
The top-σ-algebra lemma is measurable_eLpNorm_two_toReal_of_uncurry; the
sub-σ-algebra version, where joint measurability factors through
mΩ × MeasurableSpace X, is
measurable_eLpNorm_two_toReal_of_uncurry_of_factor.
lemma measurable_eLpNorm_two_toReal_of_uncurry reviewed
⚑ flagged
Causalean.Mathlib
Lp-norm measurable from joint measurability (top σ-algebra). For a σ-finite base measure P and an exponent p that is neither zero nor infinite, if the map (ω, x) ↦ g ω x is jointly measurable on the product of Ω and X, then the real-valued Lp norm ω ↦ ‖g ω‖_{Lp(P)} is measurable as a function of ω.
Formal statement
hypotheses
conclusion
Measurable (fun ω => (eLpNorm (g ω) p P).toReal)
Proof (Lean source)
lemma measurable_eLpNorm_two_toReal_of_uncurry
[MeasurableSpace Ω] {P : Measure X} [SFinite P]
{E : Type*} [MeasurableSpace E] [TopologicalSpace E] [ContinuousENorm E]
[OpensMeasurableSpace E]
{g : Ω → X → E} {p : ℝ≥0∞} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤)
(hg : Measurable (uncurry g)) :
Measurable (fun ω => (eLpNorm (g ω) p P).toReal) := by
have h_int :
Measurable (fun ω => ∫⁻ x, ‖g ω x‖ₑ ^ p.toReal ∂P) := by
exact Measurable.lintegral_prod_right' ((hg.enorm).pow_const p.toReal)
have h_norm : Measurable (fun ω => eLpNorm (g ω) p P) := by
simpa [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
hp_zero hp_top] using
(h_int.pow_const (1 / p.toReal))
exact ENNReal.measurable_toReal.comp h_norm
lemma measurable_eLpNorm_two_toReal_of_uncurry_of_factor reviewed
⚑ flagged
Causalean.Mathlib
Lp-norm measurable with respect to a sub-σ-algebra. For a σ-finite base measure P and an exponent p that is neither zero nor infinite, if the map (ω, x) ↦ g ω x is jointly measurable with respect to the product of a sub-σ-algebra mΩ on Ω and the σ-algebra on X, then the real-valued Lp norm ω ↦ ‖g ω‖_{Lp(P)} is measurable with respect to mΩ.
Formal statement
hypotheses
mΩ :
E :
p :
ℝ≥0∞
hp_zero :
p ≠ 0
hp_top :
p ≠ ⊤
hg_uncurry :
conclusion
Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal)
Proof (Lean source)
lemma measurable_eLpNorm_two_toReal_of_uncurry_of_factor
{mΩ : MeasurableSpace Ω}
{P : Measure X} [SFinite P]
{E : Type*} [MeasurableSpace E] [TopologicalSpace E] [ContinuousENorm E]
[OpensMeasurableSpace E]
{g : Ω → X → E} {p : ℝ≥0∞} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤)
(hg_uncurry :
@Measurable (Ω × X) E
(@instMeasurableSpace Ω X mΩ inferInstance) inferInstance
(uncurry g)) :
Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal) := by
have h_int :
Measurable[mΩ] (fun ω => ∫⁻ x, ‖g ω x‖ₑ ^ p.toReal ∂P) := by
exact Measurable.lintegral_prod_right' ((hg_uncurry.enorm).pow_const p.toReal)
have h_norm : Measurable[mΩ] (fun ω => eLpNorm (g ω) p P) := by
simpa [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
hp_zero hp_top] using
(h_int.pow_const (1 / p.toReal))
exact ENNReal.measurable_toReal.comp h_norm
2 supporting declarations (lemmas, instances)
-
measurable_eLpNorm_toReal_of_uncurrylemma — Alias for measurable_eLpNorm_two_toReal_of_uncurry whose name reflects that the exponent may be any finite nonzero value.hypothesesconclusionMeasurable (fun ω => (eLpNorm (g ω) p P).toReal)Proof (Lean source)
lemma measurable_eLpNorm_toReal_of_uncurry [MeasurableSpace Ω] {P : Measure X} [SFinite P] {E : Type*} [MeasurableSpace E] [TopologicalSpace E] [ContinuousENorm E] [OpensMeasurableSpace E] {g : Ω → X → E} {p : ℝ≥0∞} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤) (hg : Measurable (uncurry g)) : Measurable (fun ω => (eLpNorm (g ω) p P).toReal) := measurable_eLpNorm_two_toReal_of_uncurry hp_zero hp_top hg -
measurable_eLpNorm_toReal_of_uncurry_of_factorlemma — Alias for measurable_eLpNorm_two_toReal_of_uncurry_of_factor whose name reflects that the exponent may be any finite nonzero value.hypothesesmΩ :E :p :ℝ≥0∞hp_zero :p ≠ 0hp_top :p ≠ ⊤hg_uncurry :conclusionMeasurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal)Proof (Lean source)
lemma measurable_eLpNorm_toReal_of_uncurry_of_factor {mΩ : MeasurableSpace Ω} {P : Measure X} [SFinite P] {E : Type*} [MeasurableSpace E] [TopologicalSpace E] [ContinuousENorm E] [OpensMeasurableSpace E] {g : Ω → X → E} {p : ℝ≥0∞} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤) (hg_uncurry : @Measurable (Ω × X) E (@instMeasurableSpace Ω X mΩ inferInstance) inferInstance (uncurry g)) : Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal) := measurable_eLpNorm_two_toReal_of_uncurry_of_factor hp_zero hp_top hg_uncurry
FWL 10 core · 18 supporting This file formalizes the finite-dimensional Frisch--Waugh--Lovell residualization theorem on a real inner-product space with a nuisance subspace admitting an orthogonal projection. ★ fwlCoef_original_minimizes★ original_minimizer_eq_fwlCoef_projection
Frisch-Waugh-Lovell Algebra
This file formalizes the finite-dimensional Frisch--Waugh--Lovell residualization theorem on a real inner-product space with a nuisance subspace admitting an orthogonal projection. It is a causal-agnostic linear-algebra layer: downstream estimand-characterization modules instantiate this result, but the statements here only mention inner products, finite regressor tuples, Gram matrices, and least-squares objectives.
Main definitions:
* residualize H v is the orthogonal residual v - P_H v.
* fittedValue X β is the finite linear combination of regressors X.
* gramResid H X is the Gram matrix of the residualized regressors.
* residInnerVec H X Y is the right-hand side of the residualized normal
equations.
* fwlCoef H X Y is the coefficient vector obtained by multiplying that
right-hand side by the nonsingular inverse of gramResid H X.
* residualizedObjective and originalObjective are the least-squares
objectives after residualization and before residualizing out the nuisance
term.
Main results:
* residualize_inner_swap_right shows that the outcome can be residualized in
inner products against a residualized regressor.
* gramResid_mulVec_fwlCoef gives the residualized normal equations.
* fwlCoef_residualized_minimizes proves that fwlCoef minimizes the
residualized objective.
* fwlCoef_original_minimizes lifts that optimizer to the original objective
with an explicit nuisance term in H.
* fwlCoef_eq_of_original_minimizer and
original_minimizer_eq_fwlCoef_projection give the coefficient and full
optimizer uniqueness characterizations.
def residualize reviewed
⚑ flagged
Causalean.Mathlib.FWL
Orthogonal residual operator M_H v := v - P_H v as a function V → V. We use Submodule.orthogonalProjectionFn (which lands in V, not in ↥H) so that residualize H v : V.
Definition (Lean source)
noncomputable def residualize (v : V) : V := v - H.orthogonalProjectionFn v
def residualizeL reviewed
⚑ flagged
Causalean.Mathlib.FWL
The residual maker as a continuous linear map. This bundled form is used only to transfer linearity facts back to residualize.
Definition (Lean source)
noncomputable def residualizeL : V →L[ℝ] V :=
id ℝ V - H.starProjection
def fittedValue reviewed
⚑ flagged
Causalean.Mathlib.FWL
Fitted value for a finite tuple of regressors.
Definition (Lean source)
noncomputable def fittedValue (β : Fin K → ℝ) : V :=
∑ j, β j • X j
def gramResid reviewed
⚑ flagged
Causalean.Mathlib.FWL
The residualized Gram matrix Q_{XX} with entries ⟨residualize H (X j), residualize H (X k)⟩.
def residInnerVec reviewed
⚑ flagged
Causalean.Mathlib.FWL
The right-hand side of the residualized normal equations, r_j := ⟨residualize H (X j), Y⟩.
Definition (Lean source)
def fwlCoef reviewed
⚑ flagged
Causalean.Mathlib.FWL
The FWL coefficient. Defined directly as Q_{XX}⁻¹ *ᵥ (fun j => ⟨X̃ j, Y⟩).
Definition (Lean source)
def residualizedObjective reviewed
⚑ flagged
Causalean.Mathlib.FWL
Residualized least-squares objective.
Definition (Lean source)
noncomputable def residualizedObjective (Y : V) (β : Fin K → ℝ) : ℝ :=
inner ℝ
(residualize H Y - fittedValue (fun j => residualize H (X j)) β)
(residualize H Y - fittedValue (fun j => residualize H (X j)) β)
def originalObjective reviewed
⚑ flagged
Causalean.Mathlib.FWL
Original least-squares objective with an explicit nuisance term h ∈ H.
Definition (Lean source)
noncomputable def originalObjective (Y : V) (β : Fin K → ℝ) (h : V) : ℝ :=
inner ℝ (Y - fittedValue X β - h) (Y - fittedValue X β - h)
theorem fwlCoef_original_minimizes reviewed
⚑ flagged
Causalean.Mathlib.FWL
Standard finite-dimensional Frisch–Waugh–Lovell theorem. On a real inner-product space with a nuisance subspace H admitting an orthogonal projection, and a finite tuple of regressors X, if the residualized Gram matrix of X has nonzero determinant, i.e. is invertible and a candidate nuisance vector h lies in H, then the original least-squares objective — evaluated at the FWL coefficient together with the orthogonal-projection nuisance term of its raw residual — is at most the original objective at any other coefficient vector β and nuisance term h.
Formal statement
hypotheses
conclusion
originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)))
≤ originalObjective X Y β h
Proof (Lean source)
theorem fwlCoef_original_minimizes
(Y : V) (hQ : IsUnit (gramResid H X).det)
(β : Fin K → ℝ) {h : V} (hh : h ∈ H) :
originalObjective X Y (fwlCoef H X Y)
(H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))) ≤
originalObjective X Y β h := by
calc
originalObjective X Y (fwlCoef H X Y)
(H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)))
= residualizedObjective H X Y (fwlCoef H X Y) := by
rw [originalObjective_projection_eq_residualizedObjective]
_ ≤ residualizedObjective H X Y β :=
fwlCoef_residualized_minimizes H X Y hQ β
_ ≤ originalObjective X Y β h :=
residualizedObjective_le_originalObjective H X Y β hh
theorem original_minimizer_eq_fwlCoef_projection reviewed
⚑ flagged
Causalean.Mathlib.FWL
Uniqueness of the original least-squares minimizer. If the residualized Gram matrix of X is invertible, a candidate nuisance vector h lies in H, and the pair (β, h) minimizes the original least-squares objective over all coefficient vectors and nuisance terms in H, then β equals the FWL coefficient and h equals the orthogonal-projection nuisance term of the FWL coefficient's raw residual.
Formal statement
hypotheses
Y :
V
β :
Fin K → ℝ
h :
V
hh :
h ∈ H
hmin :
∀ (γ : Fin K → ℝ) {g : V}
if
g ∈ H
then
originalObjective X Y β h ≤ originalObjective X Y γ g
Proof (Lean source)
theorem original_minimizer_eq_fwlCoef_projection
(Y : V) (hQ : IsUnit (gramResid H X).det)
(β : Fin K → ℝ) {h : V} (hh : h ∈ H)
(hmin : ∀ (γ : Fin K → ℝ) {g : V}, g ∈ H →
originalObjective X Y β h ≤ originalObjective X Y γ g) :
β = fwlCoef H X Y ∧
h = H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)) := by
have hβ : β = fwlCoef H X Y :=
fwlCoef_eq_of_original_minimizer H X Y hQ β hh hmin
have hp : h = H.orthogonalProjectionFn (Y - fittedValue X β) := by
let p : V := H.orthogonalProjectionFn (Y - fittedValue X β)
have hp_mem : p ∈ H := by
dsimp [p]
exact Submodule.starProjection_apply_mem H (Y - fittedValue X β)
have hle : originalObjective X Y β h ≤ originalObjective X Y β p :=
hmin β hp_mem
have hsplit := originalObjective_eq_residualizedObjective_add_projectionError H X Y β hh
have hproj : originalObjective X Y β p = residualizedObjective H X Y β := by
simpa [p] using originalObjective_projection_eq_residualizedObjective H X Y β
rw [hsplit, hproj] at hle
have hnonneg :
0 ≤ inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h)
(H.orthogonalProjectionFn (Y - fittedValue X β) - h) := by
simp
have hz :
inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h)
(H.orthogonalProjectionFn (Y - fittedValue X β) - h) = 0 := by
linarith
have hzero : H.orthogonalProjectionFn (Y - fittedValue X β) - h = 0 :=
inner_self_eq_zero.mp hz
rw [sub_eq_zero] at hzero
exact hzero.symm
constructor
· exact hβ
· rw [hp, hβ]
18 supporting declarations (lemmas, instances)
-
residualize_deflemma — Residualization is the original vector minus its orthogonal projection onto the nuisance subspace.hypothesesv :Vconclusionresidualize H v = v - H.orthogonalProjectionFn vProof (Lean source)
@[simp] lemma residualize_def (v : V) : residualize H v = v - H.orthogonalProjectionFn v := rfl -
residualizeL_applylemma — Applying the residual-maker linear map gives the residualized vector.Proof (Lean source)
@[simp] lemma residualizeL_apply (v : V) : residualizeL H v = residualize H v := by simp [residualizeL, residualize] -
inner_residualize_of_memlemma — Residual is orthogonal to every element of H. This is the defining property of the orthogonal residual.Proof (Lean source)
lemma inner_residualize_of_mem (v : V) {w : V} (hw : w ∈ H) : inner ℝ (residualize H v) w = 0 := by simpa [residualize] using Submodule.orthogonalProjectionFn_inner_eq_zero (K := H) v w hw -
residualize_inner_swap_rightlemma — Symmetric residualization in the right slot. Since M_H is self-adjoint and idempotent, ⟨X̃, Y⟩ = ⟨X̃, Ỹ⟩.hypothesesv w :VProof (Lean source)
lemma residualize_inner_swap_right (v w : V) : inner ℝ (residualize H v) w = inner ℝ (residualize H v) (residualize H w) := by -- `w = residualize H w + P_H w` and `P_H w ∈ H`, which is orthogonal -- to `residualize H v`. have hPw : H.orthogonalProjectionFn w ∈ H := Submodule.starProjection_apply_mem H w have horth : inner ℝ (residualize H v) (H.orthogonalProjectionFn w) = 0 := inner_residualize_of_mem H v hPw have hsplit : w = residualize H w + H.orthogonalProjectionFn w := by simp [residualize, sub_add_cancel] calc inner ℝ (residualize H v) w = inner ℝ (residualize H v) (residualize H w + H.orthogonalProjectionFn w) := by rw [← hsplit] _ = inner ℝ (residualize H v) (residualize H w) + inner ℝ (residualize H v) (H.orthogonalProjectionFn w) := by rw [inner_add_right] _ = inner ℝ (residualize H v) (residualize H w) := by rw [horth, add_zero] -
fittedValue_sublemma — Fitted values are linear in the coefficient vector.hypothesesβ γ :Fin K → ℝconclusionfittedValue X (fun j => β j - γ j) = fittedValue X β - fittedValue X γProof (Lean source)
lemma fittedValue_sub (β γ : Fin K → ℝ) : fittedValue X (fun j => β j - γ j) = fittedValue X β - fittedValue X γ := by simp [fittedValue, sub_smul, Finset.sum_sub_distrib] -
residualize_fittedValuelemma — Residualization commutes with forming a fitted value.hypothesesβ :Fin K → ℝconclusionresidualize H (fittedValue X β) = fittedValue (fun j => residualize H (X j)) βProof (Lean source)
lemma residualize_fittedValue (β : Fin K → ℝ) : residualize H (fittedValue X β) = fittedValue (fun j => residualize H (X j)) β := by rw [← residualizeL_apply] change residualizeL H (fittedValue X β) = fittedValue (fun j => residualizeL H (X j)) β simp [fittedValue] -
residualize_regressionResiduallemma — Residualization of the raw regression residual is the residualized outcome minus the fitted value of the residualized regressors.hypothesesY :Vβ :Fin K → ℝconclusionresidualize H (Y - fittedValue X β)= residualize H Y - fittedValue (fun j => residualize H (X j)) βProof (Lean source)
lemma residualize_regressionResidual (Y : V) (β : Fin K → ℝ) : residualize H (Y - fittedValue X β) = residualize H Y - fittedValue (fun j => residualize H (X j)) β := by rw [← residualizeL_apply] change residualizeL H (Y - fittedValue X β) = residualizeL H Y - fittedValue (fun j => residualizeL H (X j)) β rw [map_sub] rw [show residualizeL H (fittedValue X β) = fittedValue (fun j => residualizeL H (X j)) β by simpa [residualizeL_apply] using residualize_fittedValue H X β] -
residInnerVec_applylemma — Each entry of the residualized right-hand side is the inner product of a residualized regressor with the outcome.Proof (Lean source)
@[simp] lemma residInnerVec_apply (Y : V) (j : Fin K) : residInnerVec H X Y j = inner ℝ (residualize H (X j)) Y := rfl -
gramResid_mulVec_fwlCoeflemma — Residualized normal equations (FWL coefficient form). If Q_{XX} = gramResid H X is invertible (equivalently, the residualized regressors are linearly independent), the FWL coefficient fwlCoef H X Y = Q_{XX}⁻¹ *ᵥ (fun j => ⟨X̃ j, Y⟩) satisfies the residualized normal equations Q_{XX} *ᵥ fwlCoef H X Y = (fun j => ⟨X̃ j, Y⟩).hypothesesconclusionProof (Lean source)
lemma gramResid_mulVec_fwlCoef (Y : V) (hQ : IsUnit (gramResid H X).det) : (gramResid H X).mulVec (fwlCoef H X Y) = residInnerVec H X Y := by -- Pure matrix algebra: `A *ᵥ (A⁻¹ *ᵥ b) = b` when `A.det` is a unit. unfold fwlCoef rw [Matrix.mulVec_mulVec, Matrix.mul_nonsing_inv _ hQ, Matrix.one_mulVec] -
residInnerVec_eq_residualize_rightlemma — Symmetric residualization for the FWL right-hand side. The residualized inner products ⟨X̃ j, Y⟩ agree with ⟨X̃ j, Ỹ⟩, so the FWL coefficient depends only on the residualized response.Proof (Lean source)
lemma residInnerVec_eq_residualize_right (Y : V) : residInnerVec H X Y = residInnerVec H X (residualize H Y) := by funext j simpa [residInnerVec] using residualize_inner_swap_right H (X j) Y -
inner_residualizedRegressor_fwlResiduallemma — The residual left by fwlCoef is orthogonal to every residualized regressor. This is the normal-equation form used in the completing-square argument.hypothesesProof (Lean source)
lemma inner_residualizedRegressor_fwlResidual (Y : V) (hQ : IsUnit (gramResid H X).det) (j : Fin K) : inner ℝ (residualize H (X j)) (residualize H Y - fittedValue (fun k => residualize H (X k)) (fwlCoef H X Y)) = 0 := by have hne := congrFun (gramResid_mulVec_fwlCoef H X Y hQ) j rw [← sub_eq_zero] rw [inner_sub_right] rw [fittedValue] simp_rw [inner_sum, inner_smul_right] rw [← residualize_inner_swap_right H (X j) Y] have hsum : (∑ x, fwlCoef H X Y x * inner ℝ (residualize H (X j)) (residualize H (X x))) = ∑ x, inner ℝ (residualize H (X j)) (residualize H (X x)) * fwlCoef H X Y x := by apply Finset.sum_congr rfl intro x _hx ring rw [hsum] simpa [mulVec, dotProduct, gramResid, residInnerVec] using sub_eq_zero.mpr hne.symm -
residualizedObjective_eq_fwlCoef_add_errortheorem — Completing-square identity for the residualized objective around the FWL coefficient.hypothesesconclusionresidualizedObjective H X Y β= residualizedObjective H X Y (fwlCoef H X Y)Proof (Lean source)
theorem residualizedObjective_eq_fwlCoef_add_error (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) : residualizedObjective H X Y β = residualizedObjective H X Y (fwlCoef H X Y) + inner ℝ (fittedValue (fun j => residualize H (X j)) (fun j => fwlCoef H X Y j - β j)) (fittedValue (fun j => residualize H (X j)) (fun j => fwlCoef H X Y j - β j)) := by let Xtilde : Fin K → V := fun j => residualize H (X j) let b : Fin K → ℝ := fwlCoef H X Y let e : V := residualize H Y - fittedValue Xtilde b let z : V := fittedValue Xtilde (fun j => b j - β j) have hz_eq : z = fittedValue Xtilde b - fittedValue Xtilde β := by dsimp [z, b] rw [fittedValue_sub] have hdecomp : residualize H Y - fittedValue Xtilde β = e + z := by dsimp [e] rw [hz_eq] abel have hcross' : inner ℝ z e = 0 := by dsimp [z, e, Xtilde, b] rw [fittedValue] simp_rw [sum_inner, inner_smul_left] apply Finset.sum_eq_zero intro j _hj have hjzero : inner ℝ (X j - H.starProjection (X j)) (Y - H.starProjection Y - fittedValue (fun j => X j - H.starProjection (X j)) (fwlCoef H X Y)) = 0 := by simpa [residualize] using inner_residualizedRegressor_fwlResidual H X Y hQ j rw [hjzero] simp have hcross : inner ℝ e z = 0 := by rw [real_inner_comm, hcross'] have hpyth : residualizedObjective H X Y β = residualizedObjective H X Y b + inner ℝ z z := by change inner ℝ (residualize H Y - fittedValue Xtilde β) (residualize H Y - fittedValue Xtilde β) = inner ℝ e e + inner ℝ z z rw [hdecomp] rw [inner_add_left, inner_add_right, inner_add_right, hcross, hcross'] ring simpa [z, Xtilde, b] using hpyth -
fwlCoef_residualized_minimizestheorem — The FWL coefficient minimizes the residualized least-squares objective.hypothesesconclusionProof (Lean source)
theorem fwlCoef_residualized_minimizes (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) : residualizedObjective H X Y (fwlCoef H X Y) ≤ residualizedObjective H X Y β := by rw [residualizedObjective_eq_fwlCoef_add_error H X Y hQ β] exact le_add_of_nonneg_right (by simp) -
originalObjective_eq_residualizedObjective_add_projectionErrortheorem — Pythagorean split of the original objective into the residualized objective plus the squared distance from h to the projection of the raw regression residual onto H.hypothesesconclusionoriginalObjective X Y β h= residualizedObjective H X Y β+ inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h) (H.orthogonalProjectionFn (Y - fittedValue X β) - h)Proof (Lean source)
theorem originalObjective_eq_residualizedObjective_add_projectionError (Y : V) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) : originalObjective X Y β h = residualizedObjective H X Y β + inner ℝ (H.orthogonalProjectionFn (Y - fittedValue X β) - h) (H.orthogonalProjectionFn (Y - fittedValue X β) - h) := by let v : V := Y - fittedValue X β let r : V := residualize H v let p : V := H.orthogonalProjectionFn v - h have hp_mem : p ∈ H := by exact Submodule.sub_mem H (Submodule.starProjection_apply_mem H v) hh have horth : inner ℝ r p = 0 := by exact inner_residualize_of_mem H v hp_mem have horth' : inner ℝ p r = 0 := by rw [real_inner_comm, horth] have hvh : v - h = r + p := by dsimp [r, p, v] simp have hres_vec : residualize H Y - fittedValue (fun j => residualize H (X j)) β = r := by dsimp [r, v] exact (residualize_regressionResidual H X Y β).symm have hres : residualizedObjective H X Y β = inner ℝ r r := by change inner ℝ (residualize H Y - fittedValue (fun j => residualize H (X j)) β) (residualize H Y - fittedValue (fun j => residualize H (X j)) β) = inner ℝ r r rw [hres_vec] dsimp [originalObjective] change inner ℝ (v - h) (v - h) = residualizedObjective H X Y β + inner ℝ p p rw [hvh, hres] rw [inner_add_left, inner_add_right, inner_add_right, horth, horth'] ring -
residualizedObjective_le_originalObjectivetheorem — For fixed β, the residualized objective is the minimum of the original objective over the nuisance subspace H.hypothesesconclusionresidualizedObjective H X Y β ≤ originalObjective X Y β hProof (Lean source)
theorem residualizedObjective_le_originalObjective (Y : V) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) : residualizedObjective H X Y β ≤ originalObjective X Y β h := by rw [originalObjective_eq_residualizedObjective_add_projectionError H X Y β hh] exact le_add_of_nonneg_right (by simp) -
originalObjective_projection_eq_residualizedObjectivetheorem — At the nuisance projection, the original objective equals the residualized objective.hypothesesY :Vβ :Fin K → ℝconclusionoriginalObjective X Y β (H.orthogonalProjectionFn (Y - fittedValue X β))= residualizedObjective H X Y βProof (Lean source)
theorem originalObjective_projection_eq_residualizedObjective (Y : V) (β : Fin K → ℝ) : originalObjective X Y β (H.orthogonalProjectionFn (Y - fittedValue X β)) = residualizedObjective H X Y β := by have hmem : H.orthogonalProjectionFn (Y - fittedValue X β) ∈ H := Submodule.starProjection_apply_mem H (Y - fittedValue X β) rw [originalObjective_eq_residualizedObjective_add_projectionError H X Y β hmem] simp -
fwlCoef_eq_of_original_minimizertheorem — Any minimizer of the original least-squares problem has coefficient block equal to the FWL coefficient. This is the uniqueness part of the standard FWL statement for the X-block.hypothesesY :Vβ :Fin K → ℝh :Vhh :h ∈ Hhmin :∀ (γ : Fin K → ℝ) {g : V}ifg ∈ HthenoriginalObjective X Y β h ≤ originalObjective X Y γ gconclusionβ = fwlCoef H X YProof (Lean source)
theorem fwlCoef_eq_of_original_minimizer (Y : V) (hQ : IsUnit (gramResid H X).det) (β : Fin K → ℝ) {h : V} (hh : h ∈ H) (hmin : ∀ (γ : Fin K → ℝ) {g : V}, g ∈ H → originalObjective X Y β h ≤ originalObjective X Y γ g) : β = fwlCoef H X Y := by let Xtilde : Fin K → V := fun j => residualize H (X j) let b : Fin K → ℝ := fwlCoef H X Y let z : V := fittedValue Xtilde (fun j => b j - β j) let hp : V := H.orthogonalProjectionFn (Y - fittedValue X b) have hp_mem : hp ∈ H := by dsimp [hp] exact Submodule.starProjection_apply_mem H (Y - fittedValue X b) have hle₁ : residualizedObjective H X Y β ≤ residualizedObjective H X Y b := by calc residualizedObjective H X Y β ≤ originalObjective X Y β h := residualizedObjective_le_originalObjective H X Y β hh _ ≤ originalObjective X Y b hp := hmin b hp_mem _ = residualizedObjective H X Y b := by simpa [hp] using originalObjective_projection_eq_residualizedObjective H X Y b have hle₂ : residualizedObjective H X Y b ≤ residualizedObjective H X Y β := fwlCoef_residualized_minimizes H X Y hQ β have hres_eq : residualizedObjective H X Y β = residualizedObjective H X Y b := le_antisymm hle₁ hle₂ have hpyth := residualizedObjective_eq_fwlCoef_add_error H X Y hQ β have hz_inner : inner ℝ z z = 0 := by rw [hres_eq] at hpyth have hpyth_z : residualizedObjective H X Y b = residualizedObjective H X Y b + inner ℝ z z := by simpa [z, Xtilde, b] using hpyth linarith have hz0 : z = 0 := inner_self_eq_zero.mp hz_inner let δ : Fin K → ℝ := fun j => b j - β j have hmul : (gramResid H X).mulVec δ = 0 := by funext j have hinner : inner ℝ (residualize H (X j)) z = 0 := by rw [hz0, inner_zero_right] dsimp [z, Xtilde, δ] at hinner ⊢ rw [fittedValue] at hinner simp_rw [inner_sum, inner_smul_right] at hinner simpa [mulVec, dotProduct, gramResid, mul_comm] using hinner have hδ0 : δ = 0 := Matrix.eq_zero_of_mulVec_eq_zero hQ.ne_zero hmul funext j have hj := congrFun hδ0 j dsimp [δ, b] at hj linarith
IIDCenteredSum 1 core · 7 supporting This file proves a conditional second-moment bound for normalized centered sums of a finite independent identically distributed sample. ★ iid_centered_sum_sq_lintegral_le
Centered Sums of Independent Identically Distributed Samples
This file proves a conditional second-moment bound for normalized centered sums
of a finite independent identically distributed sample. The sample coordinates
W i : Ω → X are jointly distributed as a product law P^s and jointly
independent of a sub-σ-algebra m_A; the integrand g : Ω → X → ℝ is
m_A-measurable in its parameter and square-integrable in the sample
coordinate.
The headline theorem is iid_centered_sum_sq_lintegral_le: for nonempty s,
∫⁻ ω, ofReal (((sqrt |s|)⁻¹ * ∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ
is bounded by
∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ.
The supporting lemmas isolate the deterministic normalization step, the
product-space variance estimate using variance_sum_pi, and the measure-law
bridge indep_trim_prod_map_eq that turns independence of m_A from the sample
tuple into a joined product law. The result is reusable outside cross-fitting:
it is a general finite-product probability estimate stated in lintegral form
with ENNReal.ofReal.
theorem iid_centered_sum_sq_lintegral_le reviewed
⚑ flagged
Causalean.Mathlib
Conditional second-moment bound for a centered i.i.d. sum. For a nonempty finite index set s, a sub-σ-algebra m_A with m_A coarser than the ambient σ-algebra, and a finite family of measurable sample coordinates W i that is jointly independent of m_A and jointly distributed as the i.i.d. product law P^s, if the parametric integrand g is jointly measurable with respect to m_A and the σ-algebra on the sample space and g ω lies in L²(P) for every ω, then the second moment of the normalized centered sum (1/√|s|)·Σᵢ(g ω (W i ω) − ∫ g ω dP) is at most the integrated squared L²(P)-norm of g ω, stated in lintegral form via ENNReal.ofReal.
Formal statement
hypotheses
Ω X :
ι :
Type*
s :
Finset ι
hs_pos :
0 < s.card
W :
ι → Ω → X
hW_meas :
∀ i ∈ s, Measurable (W i)
m_A :
hm_A_le :
m_A ≤ mΩ
hW_indep_A :
hW_iid_pi :
(@Measure.map Ω _ mΩ _ (fun ω (i : s) => W i.val ω) μ) = Measure.pi (fun _ : s => P)
g :
Ω → X → ℝ
hg_uncurry_meas :
Measurable[m_A.prod mX] (uncurry g)
hg_memLp :
∀ ω, MemLp (g ω) 2 P
Proof (Lean source)
theorem iid_centered_sum_sq_lintegral_le
{Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X]
{μ : Measure Ω} {P : Measure X}
[IsFiniteMeasure μ] [IsProbabilityMeasure P]
{ι : Type*} (s : Finset ι) (hs_pos : 0 < s.card)
(W : ι → Ω → X)
(hW_meas : ∀ i ∈ s, Measurable (W i))
(m_A : MeasurableSpace Ω) (hm_A_le : m_A ≤ mΩ)
(hW_indep_A :
Indep m_A
(comap
(fun ω (i : s) => W i.val ω) (inferInstance : MeasurableSpace _)) μ)
(hW_iid_pi :
(@Measure.map Ω _ mΩ _ (fun ω (i : s) => W i.val ω) μ) =
Measure.pi (fun _ : s => P))
(g : Ω → X → ℝ)
(hg_uncurry_meas :
Measurable[m_A.prod mX]
(uncurry g))
(hg_memLp : ∀ ω, MemLp (g ω) 2 P) :
∫⁻ ω, ofReal
(((sqrt (s.card : ℝ))⁻¹ *
∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ
≤ ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ := by
let Y : ι → Ω → ℝ :=
fun i ω => g ω (W i ω) - ∫ x, g ω x ∂P
let B : Ω → ENNReal :=
fun ω => ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2)
change
∫⁻ ω, ofReal
(((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, Y i ω) ^ 2) ∂μ
≤ ∫⁻ ω, B ω ∂μ
exact @lintegral_ofReal_inv_sqrt_smul_sum_sq_le Ω mΩ μ ι
s hs_pos Y B
(by
simpa [Y, B] using
iid_centered_sum_sq_lintegral_unscaled_le
(Ω := Ω) (X := X) (mΩ := mΩ) (mX := mX) (μ := μ) (P := P)
(s := s) (W := W) hW_meas m_A hm_A_le hW_indep_A hW_iid_pi
g hg_uncurry_meas hg_memLp)
7 supporting declarations (lemmas, instances)
-
lintegral_ofReal_inv_sqrt_smul_sum_sq_lelemma — A finite sum whose squared integral is at most its number of terms times a nonnegative benchmark remains bounded by that benchmark after division by the square root of the number of terms.Proof (Lean source)
lemma lintegral_ofReal_inv_sqrt_smul_sum_sq_le {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {ι : Type*} (s : Finset ι) (hs_pos : 0 < s.card) (Y : ι → Ω → ℝ) (B : Ω → ENNReal) (h_sum : ∫⁻ ω, ofReal ((∑ i ∈ s, Y i ω) ^ 2) ∂μ ≤ (s.card : ENNReal) * ∫⁻ ω, B ω ∂μ) : ∫⁻ ω, ofReal (((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, Y i ω) ^ 2) ∂μ ≤ ∫⁻ ω, B ω ∂μ := by let nE : ENNReal := s.card have hnE_ne_zero : nE ≠ 0 := by simp [nE, Nat.ne_of_gt hs_pos] have hnE_ne_top : nE ≠ ⊤ := by simp [nE] have hnE_inv_ne_top : nE⁻¹ ≠ ⊤ := ENNReal.Finiteness.inv_ne_top hnE_ne_zero have hpoint : ∀ ω, ofReal (((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, Y i ω) ^ 2) ≤ nE⁻¹ * ofReal ((∑ i ∈ s, Y i ω) ^ 2) := by intro ω let z : ℝ := ∑ i ∈ s, Y i ω have hnR_pos : 0 < (s.card : ℝ) := Nat.cast_pos.mpr hs_pos have hreal : ((sqrt (s.card : ℝ))⁻¹ * z) ^ 2 = ((s.card : ℝ)⁻¹) * z ^ 2 := by have hc : ((sqrt (s.card : ℝ))⁻¹) ^ 2 = ((s.card : ℝ)⁻¹) := by rw [inv_pow] rw [Real.sq_sqrt (le_of_lt hnR_pos)] rw [mul_pow, hc] rw [show ((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, Y i ω) ^ 2 = ((s.card : ℝ)⁻¹) * (∑ i ∈ s, Y i ω) ^ 2 by simpa [z] using hreal] rw [ENNReal.ofReal_mul (inv_nonneg.mpr (le_of_lt hnR_pos))] rw [ENNReal.ofReal_inv_of_pos hnR_pos] norm_num [nE] calc ∫⁻ ω, ofReal (((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, Y i ω) ^ 2) ∂μ ≤ ∫⁻ ω, nE⁻¹ * ofReal ((∑ i ∈ s, Y i ω) ^ 2) ∂μ := lintegral_mono hpoint _ = nE⁻¹ * ∫⁻ ω, ofReal ((∑ i ∈ s, Y i ω) ^ 2) ∂μ := by rw [lintegral_const_mul' _ _ hnE_inv_ne_top] _ ≤ nE⁻¹ * (nE * ∫⁻ ω, B ω ∂μ) := by exact mul_le_mul_right (by simpa [nE] using h_sum) nE⁻¹ _ = ∫⁻ ω, B ω ∂μ := by rw [← mul_assoc, ENNReal.inv_mul_cancel hnE_ne_zero hnE_ne_top, one_mul] -
eLpNorm_two_sq_toReal_eq_integral_sqlemma — The square of a square-integrable variable's L2 norm equals the integral of its squared norm, for any measure.hypothesesProof (Lean source)
lemma eLpNorm_two_sq_toReal_eq_integral_sq {X : Type*} [MeasurableSpace X] {P : Measure X} {E : Type*} [NormedAddCommGroup E] {f : X → E} (hf : MemLp f 2 P) : ofReal ((eLpNorm f 2 P).toReal ^ 2) = ofReal (∫ x, ‖f x‖ ^ 2 ∂P) := by have h_eLp := hf.eLpNorm_eq_integral_rpow_norm (by norm_num : (2 : ENNReal) ≠ 0) (by norm_num : (2 : ENNReal) ≠ ⊤) rw [h_eLp] simp only [ENNReal.toReal_ofNat] have hroot_nonneg : 0 ≤ (∫ a, ‖f a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹ := by exact Real.rpow_nonneg (integral_nonneg fun x => by positivity) _ rw [ENNReal.toReal_ofReal hroot_nonneg] have hsq : ((∫ a, ‖f a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹) ^ 2 = ∫ x, ‖f x‖ ^ 2 ∂P := by rw [show ((∫ x, ‖f x‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹) ^ 2 = ((∫ x, ‖f x‖ ^ (2 : ℝ) ∂P) ^ (1 / 2 : ℝ)) ^ 2 by norm_num] rw [show ((∫ x, ‖f x‖ ^ (2 : ℝ) ∂P) ^ (1 / 2 : ℝ)) ^ 2 = ((∫ x, ‖f x‖ ^ (2 : ℝ) ∂P) ^ (1 / 2 : ℝ)) ^ (2 : ℝ) by norm_num [Real.rpow_two]] rw [← Real.rpow_mul] · norm_num · exact integral_nonneg fun x => Real.rpow_nonneg (norm_nonneg _) _ rw [hsq] -
centered_sq_lintegral_le_eLpNorm_two_sqlemma — Centering a square-integrable real variable cannot increase its second moment beyond its uncentered L2 energy under a probability distribution.hypothesesProof (Lean source)
lemma centered_sq_lintegral_le_eLpNorm_two_sq {X : Type*} [MeasurableSpace X] {P : Measure X} [IsProbabilityMeasure P] {f : X → ℝ} (hf : MemLp f 2 P) : ∫⁻ x, ofReal ((f x - ∫ y, f y ∂P) ^ 2) ∂P ≤ ofReal ((eLpNorm f 2 P).toReal ^ 2) := by have hcenter_int : Integrable (fun x => (f x - ∫ y, f y ∂P) ^ 2) P := by have hcenter : MemLp (fun x => f x - ∫ y, f y ∂P) 2 P := by exact hf.sub (memLp_const (∫ y, f y ∂P)) exact hcenter.integrable_sq have hcenter_nn : 0 ≤ᵐ[P] fun x => (f x - ∫ y, f y ∂P) ^ 2 := Filter.Eventually.of_forall fun x => sq_nonneg _ rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal hcenter_int hcenter_nn] have hvar_eq : ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P = variance f P := by rw [(variance_eq_integral hf.aemeasurable).symm] rw [hvar_eq] have hvar_le : variance f P ≤ ∫ x, ‖f x‖ ^ 2 ∂P := by simpa [Real.norm_eq_abs, sq_abs] using variance_le_expectation_sq hf.aestronglyMeasurable rw [eLpNorm_two_sq_toReal_eq_integral_sq hf] exact ENNReal.ofReal_le_ofReal hvar_le -
pi_centered_sum_sq_lintegral_lelemma — Finitely many independent coordinates, each with its own square-integrable real-valued law, have a centered sum whose second moment is bounded by the sum of their individual squared L² norms.hypothesesι :∀ i, MeasurableSpace (X i)P :∀ i, Measure (X i)∀ i, IsProbabilityMeasure (P i)f :∀ iifX ithenℝhf :∀ i, MemLp (f i) 2 (P i)Proof (Lean source)
lemma pi_centered_sum_sq_lintegral_le {ι : Type*} [Fintype ι] {X : ι → Type*} [∀ i, MeasurableSpace (X i)] {P : ∀ i, Measure (X i)} [∀ i, IsProbabilityMeasure (P i)] {f : ∀ i, X i → ℝ} (hf : ∀ i, MemLp (f i) 2 (P i)) : ∫⁻ v : ∀ i, X i, ofReal ((∑ i, (f i (v i) - ∫ x, f i x ∂P i)) ^ 2) ∂Measure.pi P ≤ ∑ i, ofReal ((eLpNorm (f i) 2 (P i)).toReal ^ 2) := by classical let ν : Measure (∀ i, X i) := Measure.pi P let c : ∀ i, ℝ := fun i => ∫ x, f i x ∂P i let Y : ∀ i, (∀ i, X i) → ℝ := fun i v => f i (v i) - c i have hcenterP : ∀ i, MemLp (fun x => f i x - c i) 2 (P i) := by intro i exact (hf i).sub (memLp_const (∫ x, f i x ∂P i)) have hYmem : ∀ i, MemLp (Y i) 2 ν := by intro i have hcomp := (hcenterP i).comp_measurePreserving (measurePreserving_eval P i) simpa [Y, c, Function.comp_def, ν] using hcomp have hsum_mem : MemLp (fun v => ∑ i, Y i v) 2 ν := by simpa using (memLp_finset_sum univ (fun i _ => hYmem i)) have hsum_int : Integrable (fun v => (∑ i, Y i v) ^ 2) ν := hsum_mem.integrable_sq have hsum_nn : 0 ≤ᵐ[ν] fun v => (∑ i, Y i v) ^ 2 := Filter.Eventually.of_forall fun v => sq_nonneg _ rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal hsum_int hsum_nn] have hYint_zero : ∀ i, ∫ v, Y i v ∂ν = 0 := by intro i have hmp := measurePreserving_eval P i have hcenter_map : AEStronglyMeasurable (fun x => f i x - c i) (Measure.map (Function.eval i) ν) := by rw [hmp.map_eq] exact (hcenterP i).aestronglyMeasurable have hmap0 := integral_map hmp.aemeasurable hcenter_map rw [hmp.map_eq] at hmap0 have hmap : ∫ x, f i x - c i ∂P i = ∫ v, f i (v i) - c i ∂ν := hmap0 have hcenter_int_zero : ∫ x, f i x - c i ∂P i = 0 := by have hf_int : Integrable (f i) (P i) := (hf i).integrable (by norm_num : (1 : ENNReal) ≤ 2) rw [integral_sub hf_int (integrable_const (c i))] simp [c] simpa [Y, c, ν] using hmap ▸ hcenter_int_zero have hsum_int_zero : ∫ v, (∑ i, Y i v) ∂ν = 0 := by rw [integral_finset_sum univ] · simp [hYint_zero] · intro i _hi exact (hYmem i).integrable (by norm_num : (1 : ENNReal) ≤ 2) have hvar_eq_int : variance (fun v => ∑ i, Y i v) ν = ∫ v, (∑ i, Y i v) ^ 2 ∂ν := by rw [variance_of_integral_eq_zero hsum_mem.aemeasurable hsum_int_zero] have hvar_sum : variance (fun v => ∑ i, Y i v) ν = ∑ i, variance (fun x => f i x - c i) (P i) := by rw [show (fun v => ∑ i, Y i v) = (∑ i, Y i) by funext v simp] have h := variance_sum_pi (μ := P) (X := fun i x => f i x - c i) hcenterP simpa [Y, ν] using h rw [← hvar_eq_int, hvar_sum] calc ofReal (∑ i, variance (fun x => f i x - c i) (P i)) ≤ ofReal (∑ i, ∫ x, ‖f i x‖ ^ 2 ∂P i) := by exact ENNReal.ofReal_le_ofReal (Finset.sum_le_sum fun _i _hi => by rw [variance_sub_const (hf _).aestronglyMeasurable (c _)] simpa [Real.norm_eq_abs, sq_abs] using variance_le_expectation_sq (hf _).aestronglyMeasurable) _ = ∑ i, ofReal (∫ x, ‖f i x‖ ^ 2 ∂P i) := by rw [ENNReal.ofReal_sum_of_nonneg] intro i _ exact integral_nonneg fun x => sq_nonneg _ _ = ∑ i, ofReal ((eLpNorm (f i) 2 (P i)).toReal ^ 2) := by apply Finset.sum_congr rfl intro i _ rw [eLpNorm_two_sq_toReal_eq_integral_sq (hf i)] -
indep_trim_prod_map_eqlemma — Convert independence of a sub-σ-algebra and a random element into the product law of the joined map, with the first marginal trimmed to the sub-σ-algebra.hypothesesconclusion@Measure.map Ω (Ω × β) mΩ (@instMeasurableSpace Ω β m_A mβ) (fun ω => (ω, Z ω)) μ= @Measure.prod Ω β m_A mβ (μ.trim hm_A_le) (@Measure.map Ω β mΩ mβ Z μ)Proof (Lean source)
lemma indep_trim_prod_map_eq {Ω β : Type*} [mΩ : MeasurableSpace Ω] [mβ : MeasurableSpace β] {μ : Measure Ω} [IsFiniteMeasure μ] (m_A : MeasurableSpace Ω) (hm_A_le : m_A ≤ mΩ) {Z : Ω → β} (hZ : @AEMeasurable Ω β mβ mΩ Z μ) (hInd : @Indep Ω m_A (comap Z mβ) mΩ μ) : @Measure.map Ω (Ω × β) mΩ (@instMeasurableSpace Ω β m_A mβ) (fun ω => (ω, Z ω)) μ = @Measure.prod Ω β m_A mβ (μ.trim hm_A_le) (@Measure.map Ω β mΩ mβ Z μ) := by have hIF : @IndepFun Ω Ω β mΩ m_A mβ id Z μ := by rw [IndepFun_iff_Indep] simpa using hInd have hid_map : @Measure.map Ω Ω mΩ m_A id μ = μ.trim hm_A_le := by apply Measure.ext intro t ht rw [Measure.map_apply (measurable_id'' hm_A_le) ht] exact (trim_measurableSet_eq hm_A_le ht).symm have hprod := (indepFun_iff_map_prod_eq_prod_map_map ((measurable_id'' hm_A_le).aemeasurable) hZ).mp hIF simpa [hid_map, Function.comp_def] using hprod -
iid_centered_sum_sq_lintegral_unscaled_le_of_joined_lawlemma — When a finite family jointly has the product law of a base population measure and independent identically distributed draws, the integrated squared centered sum is bounded by the number of draws times the integrated squared L² norm.hypothesesΩ X :ι :Type*s :Finset ιW :ι → Ω → XhW_meas :∀ i ∈ s, Measurable (W i)m_A :hm_A_le :m_A ≤ mΩhW_join :@Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) (fun ω => (ω, fun i : s => W i.val ω)) μ= @Measure.prod Ω ((i : s) → X) m_A inferInstance (μ.trim hm_A_le) (Measure.pi (fun _ : s => P))g :Ω → X → ℝhg_uncurry_meas :Measurable[m_A.prod mX] (uncurry g)hg_memLp :∀ ω, MemLp (g ω) 2 PProof (Lean source)
lemma iid_centered_sum_sq_lintegral_unscaled_le_of_joined_law {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X] {μ : Measure Ω} {P : Measure X} [IsFiniteMeasure μ] [IsProbabilityMeasure P] {ι : Type*} (s : Finset ι) (W : ι → Ω → X) (hW_meas : ∀ i ∈ s, Measurable (W i)) (m_A : MeasurableSpace Ω) (hm_A_le : m_A ≤ mΩ) (hW_join : @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) (fun ω => (ω, fun i : s => W i.val ω)) μ = @Measure.prod Ω ((i : s) → X) m_A inferInstance (μ.trim hm_A_le) (Measure.pi (fun _ : s => P))) (g : Ω → X → ℝ) (hg_uncurry_meas : Measurable[m_A.prod mX] (uncurry g)) (hg_memLp : ∀ ω, MemLp (g ω) 2 P) : ∫⁻ ω, ofReal ((∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ ≤ (s.card : ENNReal) * ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ := by classical let νA : Measure Ω := μ.trim hm_A_le let νX : Measure ((i : s) → X) := Measure.pi (fun _ : s => P) let J : Ω → Ω × ((i : s) → X) := fun ω => (ω, fun i : s => W i.val ω) let F : Ω × ((i : s) → X) → ENNReal := fun p => ofReal ((∑ i : s, (g p.1 (p.2 i) - ∫ x, g p.1 x ∂P)) ^ 2) let B : Ω → ENNReal := fun ω => ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) have hJ_meas : @Measurable Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) J := by apply Measurable.prod · exact measurable_id'' hm_A_le · exact @measurable_pi_lambda Ω s (fun _ : s => X) mΩ (fun _ : s => mX) (fun ω (i : s) => W i.val ω) (fun i => hW_meas i.val i.property) have hc_meas : @Measurable Ω ℝ m_A inferInstance (fun ω => ∫ x, g ω x ∂P) := hg_uncurry_meas.stronglyMeasurable.integral_prod_right.measurable have hF_meas : @Measurable (Ω × ((i : s) → X)) ENNReal (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) inferInstance F := by have hterm : ∀ i : s, Measurable fun p : Ω × ((i : s) → X) => g p.1 (p.2 i) - ∫ x, g p.1 x ∂P := by intro i have hpair : Measurable fun p : Ω × ((i : s) → X) => (p.1, p.2 i) := by apply Measurable.prod · exact measurable_fst · exact (measurable_pi_apply i).comp measurable_snd exact (hg_uncurry_meas.comp hpair).sub (hc_meas.comp measurable_fst) exact ENNReal.measurable_ofReal.comp ((measurable_sum _ fun i _ => hterm i).pow_const 2) have hB_meas : @Measurable Ω ENNReal m_A inferInstance B := by have hnorm : @Measurable Ω ℝ m_A inferInstance (fun ω => (eLpNorm (g ω) 2 P).toReal) := measurable_eLpNorm_two_toReal_of_uncurry (Ω := Ω) (P := P) (g := g) (by norm_num) (by norm_num) hg_uncurry_meas exact ENNReal.measurable_ofReal.comp (hnorm.pow_const 2) have hleft_eq : ∫⁻ ω, ofReal ((∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ = ∫⁻ p, F p ∂ @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) J μ := by rw [@lintegral_map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) μ F J hF_meas hJ_meas] apply lintegral_congr_ae refine Filter.Eventually.of_forall fun ω => ?_ simp only [F, J] congr 2 exact (show (∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) = ∑ i : s, (g ω (W i.val ω) - ∫ x, g ω x ∂P) by symm simpa using (Finset.sum_attach s (fun i : ι => g ω (W i ω) - ∫ x, g ω x ∂P))) have hprod_eq : ∫⁻ p, F p ∂ @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) J μ = ∫⁻ p, F p ∂νA.prod νX := by rw [show @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) J μ = νA.prod νX by simpa [νA, νX, J] using hW_join] have hprod_tonelli : ∫⁻ p, F p ∂νA.prod νX = ∫⁻ ω, ∫⁻ v, F (ω, v) ∂νX ∂νA := by exact lintegral_prod F hF_meas.aemeasurable have hinner_le : ∀ ω, ∫⁻ v, F (ω, v) ∂νX ≤ (s.card : ENNReal) * B ω := by intro ω simpa [F, B, νX] using (pi_centered_sum_sq_lintegral_le (ι := s) (X := fun _ : s => X) (P := fun _ : s => P) (f := fun _ : s => g ω) (fun _ => hg_memLp ω)) calc ∫⁻ ω, ofReal ((∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ = ∫⁻ p, F p ∂ @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) J μ := hleft_eq _ = ∫⁻ p, F p ∂νA.prod νX := hprod_eq _ = ∫⁻ ω, ∫⁻ v, F (ω, v) ∂νX ∂νA := hprod_tonelli _ ≤ ∫⁻ ω, (s.card : ENNReal) * B ω ∂νA := lintegral_mono hinner_le _ = (s.card : ENNReal) * ∫⁻ ω, B ω ∂νA := by rw [lintegral_const_mul' _ _ (by simp)] _ = (s.card : ENNReal) * ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ := by rw [lintegral_trim hm_A_le hB_meas] -
iid_centered_sum_sq_lintegral_unscaled_lelemma — A finite conditionally independent identically distributed family has integrated squared centered sum bounded by its size times the integrated squared L² norm.hypothesesΩ X :ι :Type*s :Finset ιW :ι → Ω → XhW_meas :∀ i ∈ s, Measurable (W i)m_A :hm_A_le :m_A ≤ mΩhW_indep_A :hW_iid_pi :(@Measure.map Ω _ mΩ _ (fun ω (i : s) => W i.val ω) μ) = Measure.pi (fun _ : s => P)g :Ω → X → ℝhg_uncurry_meas :Measurable[m_A.prod mX] (uncurry g)hg_memLp :∀ ω, MemLp (g ω) 2 PProof (Lean source)
lemma iid_centered_sum_sq_lintegral_unscaled_le {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X] {μ : Measure Ω} {P : Measure X} [IsFiniteMeasure μ] [IsProbabilityMeasure P] {ι : Type*} (s : Finset ι) (W : ι → Ω → X) (hW_meas : ∀ i ∈ s, Measurable (W i)) (m_A : MeasurableSpace Ω) (hm_A_le : m_A ≤ mΩ) (hW_indep_A : Indep m_A (comap (fun ω (i : s) => W i.val ω) (inferInstance : MeasurableSpace _)) μ) (hW_iid_pi : (@Measure.map Ω _ mΩ _ (fun ω (i : s) => W i.val ω) μ) = Measure.pi (fun _ : s => P)) (g : Ω → X → ℝ) (hg_uncurry_meas : Measurable[m_A.prod mX] (uncurry g)) (hg_memLp : ∀ ω, MemLp (g ω) 2 P) : ∫⁻ ω, ofReal ((∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ ≤ (s.card : ENNReal) * ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ := by have hZ_meas : @Measurable Ω ((i : s) → X) mΩ inferInstance (fun ω (i : s) => W i.val ω) := by exact @measurable_pi_lambda Ω s (fun _ : s => X) mΩ (fun _ : s => mX) (fun ω (i : s) => W i.val ω) (fun i => hW_meas i.val i.property) have hW_join : @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) (fun ω => (ω, fun i : s => W i.val ω)) μ = @Measure.prod Ω ((i : s) → X) m_A inferInstance (μ.trim hm_A_le) (Measure.pi (fun _ : s => P)) := by have hW_join_raw : @Measure.map Ω (Ω × ((i : s) → X)) mΩ (@instMeasurableSpace Ω ((i : s) → X) m_A inferInstance) (fun ω => (ω, fun i : s => W i.val ω)) μ = @Measure.prod Ω ((i : s) → X) m_A inferInstance (μ.trim hm_A_le) (@Measure.map Ω ((i : s) → X) mΩ inferInstance (fun ω (i : s) => W i.val ω) μ) := indep_trim_prod_map_eq (Ω := Ω) (β := ((i : s) → X)) (mΩ := mΩ) (μ := μ) m_A hm_A_le hZ_meas.aemeasurable hW_indep_A simpa [hW_iid_pi] using hW_join_raw exact iid_centered_sum_sq_lintegral_unscaled_le_of_joined_law (Ω := Ω) (X := X) (mΩ := mΩ) (mX := mX) (μ := μ) (P := P) (s := s) (W := W) hW_meas m_A hm_A_le hW_join g hg_uncurry_meas hg_memLp
Indep 5 core · 10 supporting This file develops generic independence and conditional-independence facts for finite coordinate projections under product measures. ★ condIndepFun_pi_cond_residual_of_disjoint★ condIndepFun_pi_of_inter_subset
Independence Helpers for Product Coordinates
This file develops generic independence and conditional-independence facts for finite coordinate projections under product measures. The results are Mathlib-adjacent and do not depend on any causal-model definitions; downstream local-Markov arguments use them as product-measure plumbing.
Main coordinate maps:
* finsetCoordProj S projects a dependent product to the coordinates indexed by
a finite set S.
* finsetCoordProjFromCondResidual S U reassembles the coordinates on S from
the conditioning block U and the residual block S \ U.
* finsetCoordProjPairFromUnion A B extracts the A and B sub-blocks from
their union.
Main results:
* indepFun_pi_of_disjoint proves independence of disjoint coordinate blocks
under a finite product measure.
* condIndepFun_bot_of_indepFun lifts ordinary independence to conditional
independence given the trivial σ-algebra.
* condIndepFun_pi_cond_residual_of_disjoint gives conditional independence of
two residual coordinate blocks after conditioning on a common block.
* condIndepFun_pi_of_inter_subset is the public finite-product criterion:
coordinate blocks on S and T are conditionally independent given U when
S ∩ T ⊆ U.
* comap_eq_bot_of_subsingleton, indepFun_of_map, and
condIndepFun_of_indepFun_indep provide small σ-algebra and pushforward
bridges used around the product-coordinate statements.
def finsetCoordProj reviewed
⚑ flagged
Causalean
Tuple projection to a finite coordinate block of a dependent product.
Definition (Lean source)
def finsetCoordProj
{ι : Type*}
{Ω : ι → Type*} (S : Finset ι) :
(∀ i, Ω i) → ((i : {i // i ∈ S}) → Ω i.val) :=
fun x i => x i.val
def finsetCoordProjFromCondResidual reviewed
⚑ flagged
Causalean
Reassemble coordinates on S from coordinates on U and on the residual block S \ U.
Definition (Lean source)
def finsetCoordProjFromCondResidual
{ι : Type*} [DecidableEq ι]
{Ω : ι → Type*} (S U : Finset ι) :
(((i : {i // i ∈ U}) → Ω i.val) ×
((i : {i // i ∈ S \ U}) → Ω i.val)) →
((i : {i // i ∈ S}) → Ω i.val) :=
fun x i =>
if hiU : i.val ∈ U then
x.1 ⟨i.val, hiU⟩
else
x.2 ⟨i.val, Finset.mem_sdiff.mpr ⟨i.property, hiU⟩⟩
def finsetCoordProjPairFromUnion reviewed
⚑ flagged
Causalean
Extract two sub-blocks from the tuple on their union.
Definition (Lean source)
def finsetCoordProjPairFromUnion
{ι : Type*} [DecidableEq ι]
{Ω : ι → Type*} (A B : Finset ι) :
(((i : {i // i ∈ A ∪ B}) → Ω i.val) →
((i : {i // i ∈ A}) → Ω i.val) × ((i : {i // i ∈ B}) → Ω i.val)) :=
fun x =>
(fun i => x ⟨i.val, Finset.mem_union.mpr (inl i.property)⟩,
fun i => x ⟨i.val, Finset.mem_union.mpr (inr i.property)⟩)
theorem condIndepFun_pi_cond_residual_of_disjoint reviewed
⚑ flagged
Causalean
For a finite index set, a family of standard Borel probability spaces indexed by it, and finite subsets S0, T0, U of the index set, if S0 and T0 are disjoint from each other and S0 is disjoint from U, then under the product probability measure, the pair consisting of the U-coordinates and the S0-coordinates is conditionally independent of the pair consisting of the U-coordinates and the T0-coordinates, given the σ-algebra generated by the U-coordinates.
Formal statement
hypotheses
ι :
Type*
Finite ι
ι → Type*
∀ i, MeasurableSpace (Ω i)
∀ i, StandardBorelSpace (Ω i)
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
S0 T0 U :
Finset ι
hS0T0 :
Disjoint S0 T0
hS0U :
Disjoint S0 U
conclusion
letI : Fintype ι
Proof (Lean source)
theorem condIndepFun_pi_cond_residual_of_disjoint
{ι : Type*} [Finite ι]
{Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] [∀ i, StandardBorelSpace (Ω i)]
(μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)]
{S0 T0 U : Finset ι} (hS0T0 : Disjoint S0 T0)
(hS0U : Disjoint S0 U) :
letI : Fintype ι := Fintype.ofFinite ι
CondIndepFun
(comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) S0 x))
(fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) T0 x))
(Measure.pi μ) := by
classical
letI : Fintype ι := Fintype.ofFinite ι
have hS0T0U : Disjoint S0 (T0 ∪ U) := by
rw [Finset.disjoint_left]
intro i hiS0 hiT0U
rcases Finset.mem_union.mp hiT0U with hiT0 | hiU
· exact (Finset.disjoint_left.mp hS0T0) hiS0 hiT0
· exact (Finset.disjoint_left.mp hS0U) hiS0 hiU
have hindep :
IndepFun
(finsetCoordProj (Ω := Ω) S0)
(finsetCoordProj (Ω := Ω) (T0 ∪ U))
(Measure.pi μ) :=
indepFun_pi_of_disjoint (Ω := Ω) μ hS0T0U
have hindep_pair :
IndepFun
(finsetCoordProj (Ω := Ω) S0)
(fun x => (finsetCoordProj (Ω := Ω) T0 x,
finsetCoordProj (Ω := Ω) U x))
(Measure.pi μ) := by
simpa [finsetCoordProjPairFromUnion_comp] using
hindep.comp measurable_id
(measurable_finsetCoordProjPairFromUnion (Ω := Ω) T0 U)
have hbot :
CondIndepFun ⊥ bot_le
(finsetCoordProj (Ω := Ω) S0)
(fun x => (finsetCoordProj (Ω := Ω) T0 x,
finsetCoordProj (Ω := Ω) U x))
(Measure.pi μ) :=
condIndepFun_bot_of_indepFun
(measurable_finsetCoordProj (Ω := Ω) S0)
((measurable_finsetCoordProj (Ω := Ω) T0).prod
(measurable_finsetCoordProj (Ω := Ω) U))
hindep_pair
have hbase :
CondIndepFun
(comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(finsetCoordProj (Ω := Ω) S0)
(finsetCoordProj (Ω := Ω) T0)
(Measure.pi μ) := by
simpa [sup_bot_eq] using
(condIndepFun_weak_union_of_prodMk
(Ω := (i : ι) → Ω i)
(m := ⊥)
(mΩ := inferInstance)
(μ := Measure.pi μ)
bot_le
(W := finsetCoordProj (Ω := Ω) S0)
(V := finsetCoordProj (Ω := Ω) T0)
(A := finsetCoordProj (Ω := Ω) U)
(measurable_finsetCoordProj (Ω := Ω) S0)
(measurable_finsetCoordProj (Ω := Ω) T0)
(measurable_finsetCoordProj (Ω := Ω) U)
hbot)
have hleft :
CondIndepFun
(comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(fun x => (finsetCoordProj (Ω := Ω) S0 x,
finsetCoordProj (Ω := Ω) U x))
(finsetCoordProj (Ω := Ω) T0)
(Measure.pi μ) :=
condIndepFun_prodMk_of_measurable_left
(m := comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(mΩ := inferInstance)
(μ := Measure.pi μ)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(measurable_finsetCoordProj (Ω := Ω) S0)
(measurable_finsetCoordProj (Ω := Ω) T0)
(comap_measurable (finsetCoordProj (Ω := Ω) U))
hbase
have hright :
CondIndepFun
(comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(fun x => (finsetCoordProj (Ω := Ω) T0 x,
finsetCoordProj (Ω := Ω) U x))
(fun x => (finsetCoordProj (Ω := Ω) S0 x,
finsetCoordProj (Ω := Ω) U x))
(Measure.pi μ) :=
condIndepFun_prodMk_of_measurable_left
(m := comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(mΩ := inferInstance)
(μ := Measure.pi μ)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(measurable_finsetCoordProj (Ω := Ω) T0)
((measurable_finsetCoordProj (Ω := Ω) S0).prod
(measurable_finsetCoordProj (Ω := Ω) U))
(comap_measurable (finsetCoordProj (Ω := Ω) U))
hleft.symm
have hswapS :
Measurable
(fun p : (((i : {i // i ∈ S0}) → Ω i.val) ×
((i : {i // i ∈ U}) → Ω i.val)) => (p.2, p.1)) :=
measurable_snd.prod measurable_fst
have hswapT :
Measurable
(fun p : (((i : {i // i ∈ T0}) → Ω i.val) ×
((i : {i // i ∈ U}) → Ω i.val)) => (p.2, p.1)) :=
measurable_snd.prod measurable_fst
exact hright.symm.comp hswapS hswapT
theorem condIndepFun_pi_of_inter_subset reviewed
⚑ flagged
Causalean
Under a finite product probability measure, if the overlap S ∩ T is contained in the conditioning block U, then the coordinate tuple on S is conditionally independent of the coordinate tuple on T, given the coordinate tuple on U.
Formal statement
hypotheses
ι :
∀ i, MeasurableSpace (Ω i)
∀ i, StandardBorelSpace (Ω i)
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
S T U :
Finset ι
hSTU :
S ∩ T ⊆ U
conclusion
letI : Fintype ι
Proof (Lean source)
theorem condIndepFun_pi_of_inter_subset
{ι : Type*} [DecidableEq ι] [Finite ι]
{Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] [∀ i, StandardBorelSpace (Ω i)]
(μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)]
{S T U : Finset ι} (hSTU : S ∩ T ⊆ U) :
letI : Fintype ι := Fintype.ofFinite ι
CondIndepFun
(comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(finsetCoordProj (Ω := Ω) S)
(finsetCoordProj (Ω := Ω) T)
(Measure.pi μ) := by
classical
letI : Fintype ι := Fintype.ofFinite ι
let S0 : Finset ι := S \ U
let T0 : Finset ι := T \ U
have hS0T0 : Disjoint S0 T0 := by
rw [Finset.disjoint_left]
intro i hiS0 hiT0
change i ∈ S \ U at hiS0
change i ∈ T \ U at hiT0
rw [mem_sdiff] at hiS0
rw [mem_sdiff] at hiT0
exact hiT0.2 (hSTU (Finset.mem_inter.mpr ⟨hiS0.1, hiT0.1⟩))
have hS0U : Disjoint S0 U := by
rw [Finset.disjoint_left]
intro i hiS0 hiU
change i ∈ S \ U at hiS0
rw [mem_sdiff] at hiS0
exact hiS0.2 hiU
have hT0U : Disjoint T0 U := by
rw [Finset.disjoint_left]
intro i hiT0 hiU
change i ∈ T \ U at hiT0
rw [mem_sdiff] at hiT0
exact hiT0.2 hiU
have hbase :
CondIndepFun
(comap (finsetCoordProj (Ω := Ω) U) inferInstance)
(comap_le (measurable_finsetCoordProj (Ω := Ω) U))
(fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) S0 x))
(fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) T0 x))
(Measure.pi μ) :=
condIndepFun_pi_cond_residual_of_disjoint (Ω := Ω) μ hS0T0 hS0U
have h := hbase.comp
(measurable_finsetCoordProjFromCondResidual (Ω := Ω) S U)
(measurable_finsetCoordProjFromCondResidual (Ω := Ω) T U)
simpa [S0, T0, finsetCoordProjFromCondResidual_comp] using h
10 supporting declarations (lemmas, instances)
-
indepFun_pi_of_disjointtheorem — Coordinate-tuple projections at disjoint Finsets are IndepFun under Measure.pi of a family of probability measures. This is the binary aggregation of iIndepFun_pi via iIndepFun.indepFun_finset.hypothesesι :Type*Finite ιι → Type*∀ i, MeasurableSpace (Ω i)μ :(i : ι) → Measure (Ω i)∀ i, IsProbabilityMeasure (μ i)S T :Finset ιhST :Disjoint S TconclusionletI : Fintype ιProof (Lean source)
theorem indepFun_pi_of_disjoint {ι : Type*} [Finite ι] {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] {S T : Finset ι} (hST : Disjoint S T) : letI : Fintype ι := Fintype.ofFinite ι IndepFun (fun (x : ∀ i, Ω i) (i : {i // i ∈ S}) => x i.val) (fun (x : ∀ i, Ω i) (i : {i // i ∈ T}) => x i.val) (Measure.pi μ) := by letI : Fintype ι := Fintype.ofFinite ι have hiindep : iIndepFun (fun (i : ι) (ω : ∀ j, Ω j) => ω i) (Measure.pi μ) := iIndepFun_pi (X := fun _ (ω : Ω _) => ω) (fun _ => aemeasurable_id) exact hiindep.indepFun_finset S T hST (fun i => measurable_pi_apply i) -
measurable_finsetCoordProjtheorem — finsetCoordProj is measurable.hypothesesconclusionMeasurable (finsetCoordProj (Ω := Ω) S)Proof (Lean source)
theorem measurable_finsetCoordProj {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] (S : Finset ι) : Measurable (finsetCoordProj (Ω := Ω) S) := by refine measurable_pi_lambda _ ?_ intro i exact measurable_pi_apply i.val -
measurable_finsetCoordProjFromCondResidualtheorem — The residual reassembly map is measurable.hypothesesconclusionMeasurable (finsetCoordProjFromCondResidual (Ω := Ω) S U)Proof (Lean source)
theorem measurable_finsetCoordProjFromCondResidual {ι : Type*} [DecidableEq ι] {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] (S U : Finset ι) : Measurable (finsetCoordProjFromCondResidual (Ω := Ω) S U) := by refine measurable_pi_lambda _ ?_ intro i dsimp [finsetCoordProjFromCondResidual] by_cases hiU : i.val ∈ U · let j : {j // j ∈ U} := ⟨i.val, hiU⟩ simpa [hiU, j, Function.comp_def] using (measurable_pi_apply j).comp measurable_fst · let j : {j // j ∈ S \ U} := ⟨i.val, Finset.mem_sdiff.mpr ⟨i.property, hiU⟩⟩ simpa [hiU, j, Function.comp_def] using (measurable_pi_apply j).comp measurable_snd -
finsetCoordProjFromCondResidual_comptheorem — Reassembling π_U with the residual projection π_{S \ U} gives π_S.hypothesesι :S U :Finset ιconclusionfinsetCoordProjFromCondResidual (Ω := Ω) S U ∘ (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) (S \ U) x))= finsetCoordProj (Ω := Ω) SProof (Lean source)
theorem finsetCoordProjFromCondResidual_comp {ι : Type*} [DecidableEq ι] {Ω : ι → Type*} (S U : Finset ι) : finsetCoordProjFromCondResidual (Ω := Ω) S U ∘ (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) (S \ U) x)) = finsetCoordProj (Ω := Ω) S := by funext x i dsimp [finsetCoordProjFromCondResidual, finsetCoordProj] by_cases hiU : i.val ∈ U <;> simp [hiU] -
measurable_finsetCoordProjPairFromUniontheorem — The union sub-block extraction map is measurable.hypothesesconclusionMeasurable (finsetCoordProjPairFromUnion (Ω := Ω) A B)Proof (Lean source)
theorem measurable_finsetCoordProjPairFromUnion {ι : Type*} [DecidableEq ι] {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] (A B : Finset ι) : Measurable (finsetCoordProjPairFromUnion (Ω := Ω) A B) := by refine (measurable_pi_lambda _ ?_).prod (measurable_pi_lambda _ ?_) · intro i exact measurable_pi_apply (⟨i.val, Finset.mem_union.mpr (inl i.property)⟩ : {j // j ∈ A ∪ B}) · intro i exact measurable_pi_apply (⟨i.val, Finset.mem_union.mpr (inr i.property)⟩ : {j // j ∈ A ∪ B}) -
finsetCoordProjPairFromUnion_comptheorem — Projecting to A ∪ B and then extracting the two sub-blocks gives the pair of direct projections to A and B.hypothesesι :A B :Finset ιconclusionfinsetCoordProjPairFromUnion (Ω := Ω) A B ∘ finsetCoordProj (Ω := Ω) (A ∪ B)= fun x => (finsetCoordProj (Ω := Ω) A x, finsetCoordProj (Ω := Ω) B x)Proof (Lean source)
theorem finsetCoordProjPairFromUnion_comp {ι : Type*} [DecidableEq ι] {Ω : ι → Type*} (A B : Finset ι) : finsetCoordProjPairFromUnion (Ω := Ω) A B ∘ finsetCoordProj (Ω := Ω) (A ∪ B) = fun x => (finsetCoordProj (Ω := Ω) A x, finsetCoordProj (Ω := Ω) B x) := by funext x ext i <;> rfl -
condIndepFun_bot_of_indepFuntheorem — Bridge: if μ is a probability measure on a standard Borel space Ω, then unconditional IndepFun f g μ lifts to CondIndepFun ⊥ bot_le f g μ — conditional independence given the trivial σ-algebra.Proof (Lean source)
theorem condIndepFun_bot_of_indepFun {Ω : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] {β γ : Type*} [MeasurableSpace β] [MeasurableSpace γ] {f : Ω → β} {g : Ω → γ} (hf : Measurable f) (hg : Measurable g) {μ : Measure Ω} [IsProbabilityMeasure μ] (h : IndepFun f g μ) : CondIndepFun ⊥ bot_le f g μ := by rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hf hg] intro s t hs ht have hfs : MeasurableSet (f ⁻¹' s) := hf hs have hgt : MeasurableSet (g ⁻¹' t) := hg ht have hfgst : MeasurableSet (f ⁻¹' s ∩ g ⁻¹' t) := hfs.inter hgt have hmst : μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t) := h.measure_inter_preimage_eq_mul s t hs ht change condExp ⊥ μ (indicator (f ⁻¹' s ∩ g ⁻¹' t) (1 : Ω → ℝ)) =ᵐ[μ] fun ω => condExp ⊥ μ (indicator (f ⁻¹' s) (1 : Ω → ℝ)) ω * condExp ⊥ μ (indicator (g ⁻¹' t) (1 : Ω → ℝ)) ω rw [condExp_bot (μ := μ) _, condExp_bot (μ := μ) _, condExp_bot (μ := μ) _] refine Filter.Eventually.of_forall fun _ => ?_ simp only [integral_indicator_one hfgst, integral_indicator_one hfs, integral_indicator_one hgt, measureReal_def] rw [hmst, ENNReal.toReal_mul] -
comap_eq_bot_of_subsingletontheorem — The comap σ-algebra of a function into a Subsingleton codomain is the trivial σ-algebra ⊥. Every measurable set in the codomain is either empty or the full space, so every preimage is either ∅ or univ.hypothesesα β :f :α → βconclusionProof (Lean source)
theorem comap_eq_bot_of_subsingleton {α β : Type*} [MeasurableSpace β] [Subsingleton β] (f : α → β) : comap f inferInstance = (⊥ : MeasurableSpace α) := by refine le_antisymm ?_ bot_le rintro s ⟨t, _, rfl⟩ rcases t.eq_empty_or_nonempty with ht | ⟨x, hx⟩ · rw [ht, Set.preimage_empty] exact (MeasurableSpace.measurableSet_bot_iff).mpr (inl rfl) · have hpre : f ⁻¹' t = univ := by ext ω refine ⟨fun _ => trivial, fun _ => ?_⟩ have : f ω = x := Subsingleton.elim _ _ simp only [Set.mem_preimage, this, hx] rw [hpre] exact (MeasurableSpace.measurableSet_bot_iff).mpr (inr rfl) -
indepFun_of_maptheorem — Pushforward bridge for IndepFun: if X ∘ φ ⟂ᵢ Y ∘ φ under ν, then X ⟂ᵢ Y under ν.map φ. Analogue of LocalMarkov.condIndepFun_of_map at the IndepFun level.hypothesesconclusionIndepFun X Y (ν.map φ)Proof (Lean source)
theorem indepFun_of_map {α β γ δ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] {ν : Measure α} {φ : α → β} (hφ : AEMeasurable φ ν) {X : β → γ} (hX : Measurable X) {Y : β → δ} (hY : Measurable Y) (h : IndepFun (X ∘ φ) (Y ∘ φ) ν) : IndepFun X Y (ν.map φ) := by rw [indepFun_iff_measure_inter_preimage_eq_mul] at h ⊢ intro s t hs ht rw [Measure.map_apply_of_aemeasurable hφ ((hX hs).inter (hY ht)), Measure.map_apply_of_aemeasurable hφ (hX hs), Measure.map_apply_of_aemeasurable hφ (hY ht)] have := h s t hs ht simp only [Set.preimage_comp] at this exact this -
condIndepFun_of_indepFun_indeptheorem — If X and Y are independent, and the joint (X, Y) is independent of the conditioning variable Z, then X and Y are conditionally independent given the σ-algebra generated by Z.hypothesesconclusionProof (Lean source)
theorem condIndepFun_of_indepFun_indep {Ω β γ δ : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] {μ : Measure Ω} [IsProbabilityMeasure μ] {X : Ω → β} {Y : Ω → γ} {Z : Ω → δ} (hX : Measurable X) (hY : Measurable Y) (_hZ : Measurable Z) (hXY : IndepFun X Y μ) (hindep : Indep (comap (fun ω => (X ω, Y ω)) inferInstance) (comap Z inferInstance) μ) : CondIndepFun (comap Z inferInstance) _hZ.comap_le X Y μ := by have hle₂ : comap Z inferInstance ≤ (inferInstance : MeasurableSpace Ω) := _hZ.comap_le have hXYmeas : Measurable (fun ω => (X ω, Y ω)) := hX.prod hY have hle₁ : comap (fun ω => (X ω, Y ω)) inferInstance ≤ (inferInstance : MeasurableSpace Ω) := hXYmeas.comap_le rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hX hY] intro s t hs ht have hAs : MeasurableSet[comap (fun ω => (X ω, Y ω)) inferInstance] (X ⁻¹' s) := by refine ⟨(s ×ˢ Set.univ : Set (β × γ)), hs.prod MeasurableSet.univ, ?_⟩ ext ω; simp have hAt : MeasurableSet[comap (fun ω => (X ω, Y ω)) inferInstance] (Y ⁻¹' t) := by refine ⟨(Set.univ ×ˢ t : Set (β × γ)), MeasurableSet.univ.prod ht, ?_⟩ ext ω; simp have hAst := hAs.inter hAt have hconst : ∀ {A : Set Ω}, MeasurableSet[comap (fun ω => (X ω, Y ω)) inferInstance] A → (μ⟦A | comap Z inferInstance⟧) =ᵐ[μ] fun _ => (μ A).toReal := by intro A hA have hsm : StronglyMeasurable[comap (fun ω => (X ω, Y ω)) inferInstance] (A.indicator (fun _ : Ω => (1 : ℝ))) := stronglyMeasurable_const.indicator hA have hmain := condExp_indep_eq hle₁ hle₂ hsm hindep refine hmain.trans ?_ refine Filter.Eventually.of_forall fun ω => ?_ have hAmeas : MeasurableSet A := hle₁ _ hA simp only [] rw [show (A.indicator (fun _ : Ω => (1 : ℝ))) = A.indicator 1 from rfl, integral_indicator_one hAmeas, measureReal_def] have h1 := hconst hAst have h2 := hconst hAs have h3 := hconst hAt have hmul := hXY.measure_inter_preimage_eq_mul s t hs ht filter_upwards [h1, h2, h3] with ω e1 e2 e3 rw [e1, e2, e3, hmul, ENNReal.toReal_mul]
IndepIntegral 1 core · 0 supporting This file proves a drop-of-conditioning identity for independent random variables: integrating a function of one variable over an event determined by an independent variable factors into the event probability times the f ★ integral_restrict_preimage_eq_mul
Integrals Under Independent Variables
This file proves a drop-of-conditioning identity for independent random variables: integrating a function of one variable over an event determined by an independent variable factors into the event probability times the full integral. The helper supports instrumental-variable identification arguments while remaining a general measure-theoretic result.
theorem integral_restrict_preimage_eq_mul reviewed
⚑ flagged
ProbabilityTheory.IndepFun
Drop of conditioning. For random elements f and g that are independent, with f almost-everywhere measurable and g almost-everywhere measurable, given a measurable set E whose preimage f ⁻¹' E is measurable, and a function h that is almost-everywhere strongly measurable with respect to the pushforward measure of g, then restricting the integral of h ∘ g to the event f ⁻¹' E equals the probability of that event times the unrestricted integral of h ∘ g.
Formal statement
hypotheses
Ω α β :
hfg :
IndepFun f g μ
hf_ae :
AEMeasurable f μ
hg :
AEMeasurable g μ
E :
Set α
hE :
hpre :
MeasurableSet (f ⁻¹' E)
h :
β → ℝ
hh :
AEStronglyMeasurable h (μ.map g)
conclusion
∫ ω in f ⁻¹' E, h (g ω) ∂μ = (μ (f ⁻¹' E)).toReal * ∫ ω, h (g ω) ∂μ
Proof (Lean source)
theorem IndepFun.integral_restrict_preimage_eq_mul
{Ω α β : Type*} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β]
{μ : Measure Ω}
{f : Ω → α} {g : Ω → β} (hfg : IndepFun f g μ)
(hf_ae : AEMeasurable f μ) (hg : AEMeasurable g μ)
{E : Set α} (hE : MeasurableSet E)
(hpre : MeasurableSet (f ⁻¹' E))
{h : β → ℝ} (hh : AEStronglyMeasurable h (μ.map g)) :
∫ ω in f ⁻¹' E, h (g ω) ∂μ
= (μ (f ⁻¹' E)).toReal * ∫ ω, h (g ω) ∂μ := by
classical
-- `φ : α → ℝ` is the indicator of `E` as a plain function.
set φ : α → ℝ := fun a => if a ∈ E then (1 : ℝ) else 0 with hφ_def
have hφ_meas : Measurable φ :=
Measurable.ite hE measurable_const measurable_const
-- Pointwise: `φ (f ω) = (f ⁻¹' E).indicator 1 ω`.
have hφ_indicator : ∀ ω,
φ (f ω) = (f ⁻¹' E).indicator (fun _ => (1 : ℝ)) ω := by
intro ω
by_cases hω : ω ∈ f ⁻¹' E
· have hfE : f ω ∈ E := hω
simp [hφ_def, hfE]
· have hfE : f ω ∉ E := hω
simp [hφ_def, hfE]
-- Rewrite `∫ in f ⁻¹' E, ...` as `∫ φ(f) * h(g) dμ`.
have heq_int : ∫ ω in f ⁻¹' E, h (g ω) ∂μ
= ∫ ω, φ (f ω) * h (g ω) ∂μ := by
rw [← MeasureTheory.integral_indicator hpre]
refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall ?_)
intro ω
by_cases hω : ω ∈ f ⁻¹' E
· have hfE : f ω ∈ E := hω
simp [hφ_def, hfE]
· have hfE : f ω ∉ E := hω
simp [hφ_def, hfE]
-- Apply independence to factor the product integral.
have hfAE : AEMeasurable f μ := hf_ae
have hgAE : AEMeasurable g μ := hg
have hφAEStr : AEStronglyMeasurable φ (μ.map f) :=
hφ_meas.aestronglyMeasurable
have hmul : ∫ ω, φ (f ω) * h (g ω) ∂μ
= (∫ ω, φ (f ω) ∂μ) * ∫ ω, h (g ω) ∂μ :=
hfg.integral_fun_comp_mul_comp hfAE hgAE hφAEStr hh
-- `∫ φ(f) dμ = μ(f ⁻¹' E).toReal`.
have hφint : ∫ ω, φ (f ω) ∂μ = (μ (f ⁻¹' E)).toReal := by
rw [MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall hφ_indicator)]
rw [MeasureTheory.integral_indicator_const (1 : ℝ) hpre]
simp [MeasureTheory.measureReal_def]
rw [heq_int, hmul, hφint]
LikelihoodRatioSwap 1 core · 0 supporting This file proves setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap, an abstract change-of-measure identity for replacing an integral over one treatment arm by an integral over another arm with a likelihood-ratio wei ★ setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap
Likelihood-Ratio Arm Swap
This file proves setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap, an abstract
change-of-measure identity for replacing an integral over one treatment arm by an
integral over another arm with a likelihood-ratio weight. The result is used by proximal
partial-identification arguments and is formulated as a general measure-theoretic helper
independent of causal model structure.
lemma setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap reviewed
⚑ flagged
Causalean
Arm-swap via likelihood ratio. For a sub-σ-algebra m of the ambient σ-algebra on Ω, a finite measure μ, and measurable sets s and t, suppose the product f · L is almost-everywhere strongly measurable relative to m, the integrand f itself is almost-everywhere strongly measurable relative to m, f restricted to the source set t is integrable, the product f · L restricted to the target set s is integrable, and the likelihood ratio L satisfies the change-of-measure relation: the conditional probability of s given m, times L, agrees μ-almost everywhere with the conditional probability of t given m. Then the integral of f over t equals the integral of f · L over s: ∫ₜ f dμ = ∫ₛ f · L dμ.
Formal statement
hypotheses
Ω :
Type*
hm :
m ≤ mΩ
μ :
s t :
Set Ω
hs_meas :
ht_meas :
L f :
Ω → ℝ
hprod_m :
AEStronglyMeasurable[m] (fun ω => f ω * L ω) μ
hf_m :
AEStronglyMeasurable[m] f μ
hint :
IntegrableOn f t μ
hint' :
IntegrableOn (fun ω => f ω * L ω) s μ
conclusion
∫ ω in t, f ω ∂μ = ∫ ω in s, f ω * L ω ∂μ
Proof (Lean source)
lemma setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap
{Ω : Type*} {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ)
{μ : Measure Ω} [IsFiniteMeasure μ]
(s t : Set Ω) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t)
{L f : Ω → ℝ}
(hprod_m : AEStronglyMeasurable[m] (fun ω => f ω * L ω) μ)
(hf_m : AEStronglyMeasurable[m] f μ)
(hint : IntegrableOn f t μ)
(hint' : IntegrableOn (fun ω => f ω * L ω) s μ)
(hSpec :
(fun ω =>
(μ[indicator s (fun _ => (1 : ℝ)) | m]) ω * L ω)
=ᵐ[μ]
(μ[indicator t (fun _ => (1 : ℝ)) | m])) :
∫ ω in t, f ω ∂μ = ∫ ω in s, f ω * L ω ∂μ := by
-- Set up the indicator notations (as functions, not via `set`, to avoid
-- definitional unfolding issues with `condExp_mul_of_aestronglyMeasurable_left`).
let Ia : Ω → ℝ := indicator s (fun _ => (1 : ℝ))
let Ia' : Ω → ℝ := indicator t (fun _ => (1 : ℝ))
have hIa_meas : Measurable Ia :=
(measurable_const).indicator hs_meas
have hIa'_meas : Measurable Ia' :=
(measurable_const).indicator ht_meas
have hIa_le : ∀ ω, ‖Ia ω‖ ≤ 1 := by
intro ω; by_cases h : ω ∈ s
· simp [Ia, Set.indicator_of_mem h]
· simp [Ia, Set.indicator_of_notMem h]
have hIa'_le : ∀ ω, ‖Ia' ω‖ ≤ 1 := by
intro ω; by_cases h : ω ∈ t
· simp [Ia', Set.indicator_of_mem h]
· simp [Ia', Set.indicator_of_notMem h]
-- σ-finiteness of the trim, needed for `integral_condExp`.
haveI : IsFiniteMeasure (μ.trim hm) := isFiniteMeasure_trim hm
haveI : SigmaFinite (μ.trim hm) := inferInstance
-- Integrability of indicators (against μ).
have hIa_int : Integrable Ia μ := by
refine (integrable_const (1 : ℝ)).mono' hIa_meas.aestronglyMeasurable ?_
exact Filter.Eventually.of_forall (by intro ω; simpa using hIa_le ω)
have hIa'_int : Integrable Ia' μ := by
refine (integrable_const (1 : ℝ)).mono' hIa'_meas.aestronglyMeasurable ?_
exact Filter.Eventually.of_forall (by intro ω; simpa using hIa'_le ω)
-- Step A: `∫ₜ f dμ = ∫ f · Ia' dμ`.
have hStepA : ∫ ω in t, f ω ∂μ
= ∫ ω, f ω * Ia' ω ∂μ := by
rw [← integral_indicator (μ := μ) ht_meas]
refine integral_congr_ae (Filter.Eventually.of_forall ?_)
intro ω; by_cases h : ω ∈ t
· simp [Ia', Set.indicator_of_mem h]
· simp [Ia', Set.indicator_of_notMem h]
-- Step B (symmetric): `∫ₛ f · L dμ = ∫ (f · L) · Ia dμ`.
have hStepB : ∫ ω in s, f ω * L ω ∂μ
= ∫ ω, (f ω * L ω) * Ia ω ∂μ := by
rw [← integral_indicator (μ := μ) hs_meas]
refine integral_congr_ae (Filter.Eventually.of_forall ?_)
intro ω; by_cases h : ω ∈ s
· simp [Ia, Set.indicator_of_mem h]
· simp [Ia, Set.indicator_of_notMem h]
-- Integrability of pointwise products (f * Ia') and ((f*L) * Ia).
-- These equal the indicator-times-f and indicator-times-(f·L) functions, so
-- IntegrableOn-on-t (resp. s) gives global integrability.
have hint_f_Ia' : Integrable (fun ω => f ω * Ia' ω) μ := by
have h_eq : (fun ω => f ω * Ia' ω) = t.indicator f := by
funext ω
by_cases h : ω ∈ t
· simp [Ia', Set.indicator_of_mem h]
· simp [Ia', Set.indicator_of_notMem h]
rw [h_eq]
exact hint.integrable_indicator ht_meas
have hint_fL_Ia : Integrable (fun ω => (f ω * L ω) * Ia ω) μ := by
have h_eq : (fun ω => (f ω * L ω) * Ia ω)
= s.indicator (fun ω => f ω * L ω) := by
funext ω
by_cases h : ω ∈ s
· simp [Ia, Set.indicator_of_mem h]
· simp [Ia, Set.indicator_of_notMem h]
rw [h_eq]
exact hint'.integrable_indicator hs_meas
-- Pull-out: `μ[f * Ia' | m] =ᵐ f · μ[Ia' | m]`.
have hpull' : (μ[fun ω => f ω * Ia' ω | m]) =ᵐ[μ]
(fun ω => f ω * (μ[Ia' | m]) ω) := by
have h := condExp_mul_of_aestronglyMeasurable_left (μ := μ) (m := m)
(f := f) (g := Ia') hf_m hint_f_Ia' hIa'_int
-- h : μ[f * Ia' | m] =ᵐ f * μ[Ia' | m] (Pi product)
exact h
-- Pull-out: `μ[(f*L) * Ia | m] =ᵐ (f·L) · μ[Ia | m]`.
have hpull : (μ[fun ω => (f ω * L ω) * Ia ω | m]) =ᵐ[μ]
(fun ω => (f ω * L ω) * (μ[Ia | m]) ω) := by
have h := condExp_mul_of_aestronglyMeasurable_left (μ := μ) (m := m)
(f := fun ω => f ω * L ω) (g := Ia) hprod_m
hint_fL_Ia hIa_int
exact h
-- Compute LHS: lift indicator integral, then condExp tower, then pull-out.
have hLHS : ∫ ω in t, f ω ∂μ
= ∫ ω, f ω * (μ[Ia' | m]) ω ∂μ := by
rw [hStepA, ← integral_condExp hm (f := fun ω => f ω * Ia' ω)]
exact integral_congr_ae hpull'
-- Compute RHS.
have hRHS : ∫ ω in s, f ω * L ω ∂μ
= ∫ ω, (f ω * L ω) * (μ[Ia | m]) ω ∂μ := by
rw [hStepB, ← integral_condExp hm (f := fun ω => (f ω * L ω) * Ia ω)]
exact integral_congr_ae hpull
-- Identify the two integrands via `hSpec`.
rw [hLHS, hRHS]
refine integral_congr_ae ?_
filter_upwards [hSpec] with ω hω
-- hω : (μ[Ia | m]) ω * L ω = (μ[Ia' | m]) ω
-- Goal: f ω * (μ[Ia' | m]) ω = (f ω * L ω) * (μ[Ia | m]) ω
rw [← hω]; ring
MeasurableEmbeddingExtras 1 core · 0 supporting This file collects general measure-theoretic facts about measurable embeddings that are independent of the library's structural causal model and SWIG infrastructure. ★ restrict_range_eq_of_forall_image
Measurable Embedding Extras
This file collects general measure-theoretic facts about measurable embeddings that are
independent of the library's structural causal model and SWIG infrastructure. Its main
result, restrict_range_eq_of_forall_image, shows that agreement on all embedded
measurable images implies agreement after restricting both measures to the embedding
range.
theorem restrict_range_eq_of_forall_image reviewed
⚑ flagged
MeasureTheory
If F is a measurable embedding of one measurable space into another and two measures μ and ν on the codomain assign the same mass to the image F '' A of every measurable set A in the domain, then restricting μ and ν to the range of F yields identical measures.
Formal statement
hypotheses
Proof (Lean source)
theorem restrict_range_eq_of_forall_image (hF : MeasurableEmbedding F)
(μ ν : Measure β)
(h : ∀ A, MeasurableSet A → μ (F '' A) = ν (F '' A)) :
μ.restrict (range F) = ν.restrict (range F) := by
-- Step 1: μ.comap F = ν.comap F on α (both interpret each measurable
-- A ⊆ α as μ (F '' A), resp. ν (F '' A)).
have h_comap : μ.comap F = ν.comap F := by
refine Measure.ext (fun A hA => ?_)
rw [hF.comap_apply, hF.comap_apply]
exact h A hA
-- Step 2: push forward via F, using map_comap.
calc μ.restrict (range F)
= (μ.comap F).map F := (hF.map_comap μ).symm
_ = (ν.comap F).map F := by rw [h_comap]
_ = ν.restrict (range F) := hF.map_comap ν
OperatorSqrt 2 core · 9 supporting This file constructs the positive square root of a positive operator on a finite-dimensional real inner-product space by diagonalizing the operator in an orthonormal eigenbasis. ★ posSqrt_mul_self★ posSqrtCLM_comp_self
Positive square roots of finite-dimensional positive operators
This file constructs the positive square root of a positive operator on a
finite-dimensional real inner-product space by diagonalizing the operator in an
orthonormal eigenbasis. The main linear-map construction is posSqrt, with
posSqrt_mul_self, posSqrt_isSymmetric, and posSqrt_isPositive proving that it
is the positive square root. The file also packages the same map as a continuous
linear map posSqrtCLM, proves it is self-adjoint, and proves the corresponding
continuous square law posSqrtCLM_comp_self.
theorem posSqrt_mul_self reviewed
⚑ flagged
LinearMap.IsPositive
Composing the positive square root of T with itself recovers T.
Formal statement
conclusion
hT.posSqrt ∘ₗ hT.posSqrt = T
Proof (Lean source)
theorem posSqrt_mul_self : hT.posSqrt ∘ₗ hT.posSqrt = T := by
refine (hT.eigBasis).toBasis.ext fun i => ?_
simp only [OrthonormalBasis.coe_toBasis, coe_comp, Function.comp_apply,
hT.posSqrt_apply_eigBasis i, map_smul, smul_smul,
Real.mul_self_sqrt (hT.eigVals_nonneg i), hT.apply_eigBasis i]
theorem posSqrtCLM_comp_self reviewed
⚑ flagged
LinearMap.IsPositive
Composing the continuous positive square root of T with itself recovers T, packaged as a continuous linear map.
Formal statement
conclusion
hT.posSqrtCLM ∘L hT.posSqrtCLM = T.toContinuousLinearMap
Proof (Lean source)
theorem posSqrtCLM_comp_self :
hT.posSqrtCLM ∘L hT.posSqrtCLM = T.toContinuousLinearMap := by
ext x
change hT.posSqrt (hT.posSqrt x) = T x
rw [← LinearMap.comp_apply, hT.posSqrt_mul_self]
9 supporting declarations (lemmas, instances)
-
apply_eigBasistheorem — Applying the operator to an eigenbasis vector scales that vector by its indexed eigenvalue.Proof (Lean source)
theorem apply_eigBasis (i : Fin (finrank ℝ E)) : T (hT.eigBasis i) = (hT.eigVals i) • hT.eigBasis i := by simp only [eigBasis, eigVals] exact hT.isSymmetric.apply_eigenvectorBasis rfl i -
eigVals_nonnegtheorem — Eigenvalues of a positive operator are nonnegative.Proof (Lean source)
theorem eigVals_nonneg (i : Fin (finrank ℝ E)) : 0 ≤ hT.eigVals i := by have hb : ⟪hT.eigBasis i, hT.eigBasis i⟫ = 1 := by have := (hT.eigBasis).orthonormal.1 i rw [real_inner_self_eq_norm_sq, this]; norm_num have hpos := hT.2 (hT.eigBasis i) rw [hT.apply_eigBasis i, inner_smul_left] at hpos -- `hpos : 0 ≤ ⟪T (b i), b i⟫` becomes `0 ≤ μ i` simpa only [conj_trivial, hb, mul_one, RCLike.re_to_real] using hpos -
posSqrt_apply_eigBasistheorem — The positive square root sends each eigenbasis vector to the same vector scaled by the square root of its eigenvalue.hypothesesconclusionhT.posSqrt (hT.eigBasis i) = sqrt (hT.eigVals i) • hT.eigBasis iProof (Lean source)
theorem posSqrt_apply_eigBasis (i : Fin (finrank ℝ E)) : hT.posSqrt (hT.eigBasis i) = sqrt (hT.eigVals i) • hT.eigBasis i := by rw [posSqrt, ← OrthonormalBasis.coe_toBasis, Basis.constr_basis] -
posSqrt_innertheorem — Inner-product form of posSqrt: a symmetric weighted sum over the eigenbasis.hypothesesx y :Econclusion⟪hT.posSqrt x, y⟫= ∑ i, sqrt (hT.eigVals i) * ⟪hT.eigBasis i, x⟫ * ⟪hT.eigBasis i, y⟫Proof (Lean source)
theorem posSqrt_inner (x y : E) : ⟪hT.posSqrt x, y⟫ = ∑ i, sqrt (hT.eigVals i) * ⟪hT.eigBasis i, x⟫ * ⟪hT.eigBasis i, y⟫ := by have hx : hT.posSqrt x = ∑ i, (⟪hT.eigBasis i, x⟫ * sqrt (hT.eigVals i)) • hT.eigBasis i := by conv_lhs => rw [← (hT.eigBasis).sum_repr x] rw [map_sum] refine Finset.sum_congr rfl fun i _ => ?_ rw [map_smul, hT.posSqrt_apply_eigBasis i, smul_smul, OrthonormalBasis.repr_apply_apply] rw [hx, sum_inner] refine Finset.sum_congr rfl fun i _ => ?_ rw [inner_smul_left, conj_trivial] ring -
posSqrt_isSymmetrictheorem — posSqrt is symmetric.conclusionhT.posSqrt.IsSymmetricProof (Lean source)
theorem posSqrt_isSymmetric : hT.posSqrt.IsSymmetric := fun x y => by rw [hT.posSqrt_inner x y, show ⟪x, hT.posSqrt y⟫ = ⟪hT.posSqrt y, x⟫ from real_inner_comm _ _, hT.posSqrt_inner y x] exact Finset.sum_congr rfl fun i _ => by ring -
posSqrt_isPositivetheorem — posSqrt is itself a positive operator.conclusionhT.posSqrt.IsPositiveProof (Lean source)
theorem posSqrt_isPositive : hT.posSqrt.IsPositive := by refine (LinearMap.isPositive_iff _).mpr ⟨hT.posSqrt_isSymmetric, fun x => ?_⟩ rw [hT.posSqrt_inner x x] refine sum_nonneg fun i _ => ?_ nlinarith [Real.sqrt_nonneg (hT.eigVals i), mul_self_nonneg ⟪hT.eigBasis i, x⟫] -
posSqrtCLM_applytheorem — The continuous-linear-map packaging of the positive square root has the same pointwise action as the linear-map square root.hypothesesx :EconclusionhT.posSqrtCLM x = hT.posSqrt xProof (Lean source)
@[simp] theorem posSqrtCLM_apply (x : E) : hT.posSqrtCLM x = hT.posSqrt x := rfl -
posSqrtCLM_isSelfAdjointtheorem — The continuous square root is self-adjoint.conclusionIsSelfAdjoint hT.posSqrtCLMProof (Lean source)
theorem posSqrtCLM_isSelfAdjoint : IsSelfAdjoint hT.posSqrtCLM := (LinearMap.isSelfAdjoint_toContinuousLinearMap_iff _).mpr ((LinearMap.isSymmetric_iff_isSelfAdjoint _).mp hT.posSqrt_isSymmetric)
SemiInnerProjection 1 core · 0 supporting This file proves exists_orthogonalProjection_of_posSemidef: every finite-dimensional subspace of a vector space over a linearly ordered field admits a linear map into that subspace whose residual is orthogonal, with resp ★ exists_orthogonalProjection_of_posSemidef
Semidefinite Normal-Equation Maps
This file proves exists_orthogonalProjection_of_posSemidef: every finite-dimensional
subspace of a vector space over a linearly ordered field admits a linear map into that
subspace whose residual is orthogonal, with respect to a symmetric positive-semidefinite
bilinear form, to every vector in the subspace. The result supplies the
linear-algebra substrate for weighted normal-equation arguments where the inner
product may be degenerate.
lemma exists_orthogonalProjection_of_posSemidef reviewed
⚑ flagged
Causalean.Mathlib
In a vector space over a linearly ordered field equipped with a bilinear form B that is symmetric and positive-semidefinite, every finite-dimensional linear subspace H admits a linear self-map P of the ambient space, valued in H, whose residual X - P X is B-orthogonal to every vector of H, for every X.
Formal statement
Proof (Lean source)
lemma exists_orthogonalProjection_of_posSemidef
(B : BilinForm K V)
(hsymm : ∀ x y, B x y = B y x)
(hpos : ∀ x, 0 ≤ B x x)
(H : Submodule K V) [FiniteDimensional K H] :
∃ P : V →ₗ[K] V,
(∀ X, P X ∈ H) ∧ (∀ X, ∀ h ∈ H, B (X - P X) h = 0) := by
classical
let A : H →ₗ[K] Module.Dual K H :=
LinearMap.mk₂ K (fun x y : H => B x.1 y.1)
(by
intro x y z
simp)
(by
intro a x z
simp)
(by
intro x y z
simp)
(by
intro a x z
simp)
let L : V →ₗ[K] Module.Dual K H :=
LinearMap.mk₂ K (fun (x : V) (y : H) => B x y.1)
(by
intro x y z
simp)
(by
intro a x z
simp)
(by
intro x y z
simp)
(by
intro a x z
simp)
have hBsymm : B.IsSymm := ⟨fun x y => hsymm x y⟩
have hAflip : A.flip = A := by
ext x y
simpa [A] using (hsymm x.1 y.1).symm
have hL_mem_range : ∀ X, L X ∈ range A := by
intro X
have hL_ann : L X ∈ (ker A).dualAnnihilator := by
rw [Submodule.mem_dualAnnihilator]
intro x hx
have hxself : B x.1 x.1 = 0 := by
have hAx : A x = 0 := by
simpa [LinearMap.mem_ker] using hx
have := congrArg (fun f : Module.Dual K H => f x) hAx
simpa [A] using this
have hxker : x.1 ∈ ker B := by
exact (B.apply_apply_same_eq_zero_iff hpos hBsymm).mp hxself
have hxX : B x.1 X = 0 := by
have hBx : B x.1 = 0 := by
simpa [LinearMap.mem_ker] using hxker
have := congrArg (fun f : Module.Dual K V => f X) hBx
simpa using this
simpa [L, hsymm X x.1] using hxX
rwa [LinearMap.dualAnnihilator_ker_eq_range_flip, hAflip] at hL_ann
let Lrange : V →ₗ[K] range A :=
L.codRestrict (range A) hL_mem_range
letI : Module.Free K (range A) :=
Module.Free.of_divisionRing K (range A)
obtain ⟨S, hS⟩ :=
A.rangeRestrict.exists_rightInverse_of_surjective
(LinearMap.range_rangeRestrict A)
let PH : V →ₗ[K] H := S.comp Lrange
refine ⟨H.subtype.comp PH, ?_, ?_⟩
· intro X
exact (PH X).2
· intro X h hH
let hh : H := ⟨h, hH⟩
have hEq : A (PH X) hh = L X hh := by
have hRangeEq : A.rangeRestrict (S (Lrange X)) = Lrange X := by
exact congrArg (fun f : range A →ₗ[K] range A =>
f (Lrange X)) hS
have hValEq : (A.rangeRestrict (S (Lrange X)) : Module.Dual K H) =
(Lrange X : Module.Dual K H) :=
congrArg (fun y : range A => (y : Module.Dual K H)) hRangeEq
exact congrArg (fun f : Module.Dual K H => f hh) hValEq
have hB_eq : B (PH X).1 h = B X h := by
simpa [A, L, PH, hh] using hEq
simp [hB_eq]
StandardGaussian 3 core · 9 supporting This file constructs the standard Gaussian probability measure on an arbitrary finite-dimensional real inner-product space and proves its mean, Gaussianity, and covariance form. ★ stdGaussian_map_normSq_eq_pi
Standard Gaussian Measures
This file constructs the standard Gaussian probability measure on an arbitrary finite-dimensional real inner-product space and proves its mean, Gaussianity, and covariance form. It also identifies the law of the squared norm with the sum of squared independent one-dimensional standard Gaussians. The construction gives downstream statistical modules a basis-independent Gaussian law with covariance equal to the inner product.
def piGaussian reviewed
⚑ flagged
Causalean.Mathlib
The product measure of independent standard normal laws, with one real-valued coordinate for each dimension of a finite-dimensional real inner-product space.
def stdGaussian reviewed
⚑ flagged
Causalean.Mathlib
The standard Gaussian measure on a finite-dimensional real inner-product space E: covariance equal to the identity (inner product), mean zero.
theorem stdGaussian_map_normSq_eq_pi reviewed
⚑ flagged
Causalean.Mathlib
Product-of-1-D-Gaussians model for the squared norm. The law of the squared norm under the standard Gaussian measure on E equals the law of the sum of squared coordinates under a product of finrank ℝ E independent standard real Gaussians.
Formal statement
conclusion
(stdGaussian E).map (fun x => ‖x‖ ^ 2)
Proof (Lean source)
theorem stdGaussian_map_normSq_eq_pi :
(stdGaussian E).map (fun x => ‖x‖ ^ 2)
= (Measure.pi (fun _ : Fin (finrank ℝ E) => gaussianReal 0 1)).map
(fun w => ∑ i, (w i) ^ 2) := by
-- `stdGaussian = euclideanStdGaussian.map repr.symm`, and `repr.symm` is an isometry
rw [stdGaussian, Measure.map_map (by fun_prop) (by fun_prop)]
have h1 : (fun x => ‖x‖ ^ 2) ∘ ⇑(onb E).repr.symm.toContinuousLinearEquiv
= fun y => ‖y‖ ^ 2 := by
funext y
simp only [Function.comp_apply]
rw [show (onb E).repr.symm.toContinuousLinearEquiv y = (onb E).repr.symm y from rfl,
(onb E).repr.symm.norm_map]
rw [h1, euclideanStdGaussian, Measure.map_map (by fun_prop) (by fun_prop)]
refine Measure.map_congr (ae_of_all _ fun w => ?_)
simp only [Function.comp_apply]
rw [EuclideanSpace.norm_eq, Real.sq_sqrt (sum_nonneg fun i _ => by positivity)]
refine Finset.sum_congr rfl fun i _ => ?_
rw [Real.norm_eq_abs, sq_abs]
congr 1
9 supporting declarations (lemmas, instances)
-
isProbabilityMeasure_piGaussianinstance — The product of independent one-dimensional standard Gaussian laws is a probability measure.instance isProbabilityMeasure_piGaussian : IsProbabilityMeasure (piGaussian E) := by unfold piGaussian; infer_instance -
isGaussian_piGaussianinstance — The product standard Gaussian on Fin n → ℝ is Gaussian.instance isGaussian_piGaussian : IsGaussian (piGaussian E) := by have hIndep : iIndepFun (fun (i : Fin (finrank ℝ E)) (ω : Fin (finrank ℝ E) → ℝ) => ω i) (piGaussian E) := iIndepFun_pi (X := fun _ => (id : ℝ → ℝ)) (fun _ => aemeasurable_id) have hLaw : ∀ i, HasGaussianLaw (fun ω : Fin (finrank ℝ E) → ℝ => ω i) (piGaussian E) := by intro i classical have hmap : (piGaussian E).map (fun ω => ω i) = gaussianReal 0 1 := by unfold piGaussian rw [show (fun ω : Fin (finrank ℝ E) → ℝ => ω i) = Function.eval i from rfl, Measure.pi_map_eval] simp refine ⟨?_⟩ rw [hmap]; infer_instance have hJoint : IsGaussian ((piGaussian E).map (fun ω => (fun i => ω i : Fin (finrank ℝ E) → ℝ))) := (hIndep.hasGaussianLaw hLaw).isGaussian_map simpa using hJoint -
isProbabilityMeasure_euclideanStdGaussianinstance — The transported product standard Gaussian on Euclidean space is a probability measure.instance isProbabilityMeasure_euclideanStdGaussian : IsProbabilityMeasure (euclideanStdGaussian E) := by unfold euclideanStdGaussian exact Measure.isProbabilityMeasure_map (by fun_prop) -
isProbabilityMeasure_stdGaussianinstance — The standard Gaussian measure on the inner-product space is a probability measure.instance isProbabilityMeasure_stdGaussian : IsProbabilityMeasure (stdGaussian E) := by unfold stdGaussian exact Measure.isProbabilityMeasure_map (by fun_prop) -
isGaussian_euclideanStdGaussianinstance — The product standard Gaussian on EuclideanSpace ℝ (Fin n) is Gaussian.instance isGaussian_euclideanStdGaussian : IsGaussian (euclideanStdGaussian E) := by unfold euclideanStdGaussian exact isGaussian_map_equiv _ -
isGaussian_stdGaussianinstance — The standard Gaussian measure on the inner-product space is a Gaussian law.instance isGaussian_stdGaussian : IsGaussian (stdGaussian E) := by unfold stdGaussian exact isGaussian_map_equiv _ -
integral_id_map_equivlemma — Transporting a measure through a continuous linear equivalence transports its vector integral through the same equivalence.hypothesesF G :L :F ≃L[ℝ] Gconclusion∫ x, x ∂(μ.map L) = L (∫ x, x ∂μ)Proof (Lean source)
lemma integral_id_map_equiv {F G : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {μ : Measure F} (L : F ≃L[ℝ] G) : ∫ x, x ∂(μ.map L) = L (∫ x, x ∂μ) := by rw [integral_map (φ := L) (f := fun x => x) (by fun_prop) (aestronglyMeasurable_id.congr (by rfl))] exact L.integral_comp_comm (fun x => x) -
stdGaussian_meantheorem — The standard Gaussian measure on a finite-dimensional real inner-product space has mean zero.conclusion∫ x, x ∂(stdGaussian E) = 0Proof (Lean source)
theorem stdGaussian_mean : ∫ x, x ∂(stdGaussian E) = 0 := by unfold stdGaussian rw [integral_id_map_equiv, integral_euclideanStdGaussian] simp -
covarianceBilin_stdGaussiantheorem — The covariance bilinear form of the standard Gaussian measure is the ambient inner product.Proof (Lean source)
theorem covarianceBilin_stdGaussian (u v : E) : covarianceBilin (stdGaussian E) u v = (inner ℝ u v : ℝ) := by have hmemLp : MemLp id 2 (euclideanStdGaussian E) := (isGaussian_euclideanStdGaussian (E := E)).memLp_two_id set L : EuclideanSpace ℝ (Fin (finrank ℝ E)) →L[ℝ] E := (onb E).repr.symm.toContinuousLinearEquiv.toContinuousLinearMap with hL have hmeas : stdGaussian E = (euclideanStdGaussian E).map L := rfl rw [hmeas, covarianceBilin_map hmemLp] have hadj : L.adjoint = ((onb E).repr : E →L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) := by rw [hL] have h := (onb E).repr.symm.adjoint_eq_symm simp only [LinearIsometryEquiv.symm_symm] at h convert h using 2 rw [hadj, covarianceBilin_euclideanStdGaussian] exact (onb E).repr.inner_map_map u v
TwoStateMarkov 4 core · 2 supporting This file develops transitionMatrix, stationaryProjection, transitionMatrix_pow_eq_spectral, the pointwise and compact-uniform spectral gap bounds, and transitionMatrix_pow_tendsto_stationary_uniform for a two-state Mark ★ transitionMatrix_pow_eq_spectral★ transitionMatrix_pow_tendsto_stationary_uniform
Two-State Markov Chains
This file develops transitionMatrix, stationaryProjection,
transitionMatrix_pow_eq_spectral, the pointwise and compact-uniform spectral
gap bounds, and transitionMatrix_pow_tendsto_stationary_uniform for a
two-state Markov chain with transition probabilities in the open unit square.
def transitionMatrix reviewed
⚑ flagged
Causalean.Mathlib.TwoStateMarkov
Transition matrix with rows (1 - a, a) and (b, 1 - b).
def stationaryProjection reviewed
⚑ flagged
Causalean.Mathlib.TwoStateMarkov
Stationary projection with both rows equal to (b/(a+b), a/(a+b)).
theorem transitionMatrix_pow_eq_spectral reviewed
⚑ flagged
Causalean.Mathlib.TwoStateMarkov
For parameters a, b in a field with a + b nonzero, the k-th power of the two-state transition matrix transitionMatrix a b decomposes as the stationary projection stationaryProjection a b plus (1 - a - b)^k times its complement, for every k.
Formal statement
hypotheses
conclusion
∀ k : ℕ,
(transitionMatrix a b) ^ k
= stationaryProjection a b + ((1 - a - b) ^ k) • (1 - stationaryProjection a b)
Proof (Lean source)
theorem transitionMatrix_pow_eq_spectral
{K : Type*} [Field K] (a b : K) (hs : a + b ≠ 0) :
∀ k : ℕ,
(transitionMatrix a b) ^ k =
stationaryProjection a b +
((1 - a - b) ^ k) • (1 - stationaryProjection a b) := by
let P := stationaryProjection a b
let Q : Matrix (Fin 2) (Fin 2) K := 1 - P
let lam := 1 - a - b
have hM : transitionMatrix a b = P + lam • Q := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, lam, transitionMatrix, stationaryProjection, Matrix.smul_apply,
Matrix.sub_apply, Matrix.add_apply] <;>
field_simp [hs] <;> ring
have hP2 : P * P = P := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, stationaryProjection, Matrix.mul_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
have hPQ : P * Q = 0 := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, stationaryProjection, Matrix.mul_apply, Matrix.sub_apply,
Matrix.one_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
have hQP : Q * P = 0 := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, stationaryProjection, Matrix.mul_apply, Matrix.sub_apply,
Matrix.one_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
have hQ2 : Q * Q = Q := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, stationaryProjection, Matrix.mul_apply, Matrix.sub_apply,
Matrix.one_apply, Fin.sum_univ_two] <;>
field_simp [hs] <;> ring
intro k
induction k with
| zero =>
ext i j
fin_cases i <;> fin_cases j <;>
simp [stationaryProjection, Matrix.add_apply, Matrix.sub_apply]
| succ k ih =>
calc
transitionMatrix a b ^ (k + 1)
= (P + (lam ^ k) • Q) * (P + lam • Q) := by rw [pow_succ, ih, hM]
_ = P + (lam ^ (k + 1)) • Q := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [P, Q, lam, stationaryProjection, Matrix.mul_apply, Matrix.add_apply,
Matrix.sub_apply, Matrix.smul_apply, Matrix.one_apply, Fin.sum_univ_two,
pow_succ] <;>
field_simp [hs] <;> ring
theorem transitionMatrix_pow_tendsto_stationary_uniform reviewed
⚑ flagged
Causalean.Mathlib.TwoStateMarkov
For a set K of transition-parameter pairs (a,b) that is compact and contained in the open unit square, the k-th power of the transition matrix converges to the stationary projection entrywise, uniformly over K: for every ε > 0 there is a threshold N such that every entry of (transitionMatrix a b)^k - stationaryProjection a b has absolute value at most ε once k ≥ N, for every (a,b) in K.
Formal statement
hypotheses
conclusion
∀ ε > (0 : ℝ),
∃ N : ℕ,
∀ k : ℕ,
N
≤ k → ∀ p ∈ K, ∀ i j : Fin 2, |((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j| ≤ ε
Proof (Lean source)
theorem transitionMatrix_pow_tendsto_stationary_uniform
(K : Set (ℝ × ℝ)) (hK_compact : IsCompact K)
(hK_open : K ⊆ {p : ℝ × ℝ | 0 < p.1 ∧ p.1 < 1 ∧ 0 < p.2 ∧ p.2 < 1}) :
∀ ε > (0 : ℝ), ∃ N : ℕ, ∀ k : ℕ, N ≤ k →
∀ p ∈ K, ∀ i j : Fin 2,
|((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j| ≤ ε := by
intro ε hε
classical
by_cases hne : K.Nonempty
· obtain ⟨ρ, hρ_lt, hρ_bound⟩ :=
one_minus_a_b_uniform_gap_on_compact K hK_compact (fun p hp => by
have hopen := hK_open hp
exact ⟨by linarith [hopen.1, hopen.2.2.1], by linarith [hopen.2.1, hopen.2.2.2]⟩)
rcases hne with ⟨p0, hp0⟩
have hρ_nonneg : 0 ≤ ρ :=
(abs_nonneg (1 - p0.1 - p0.2)).trans (hρ_bound p0 hp0)
have htend := tendsto_pow_atTop_nhds_zero_of_lt_one hρ_nonneg hρ_lt
have hevent : ∀ᶠ k in atTop, ρ ^ k < ε := htend.eventually_lt_const hε
rw [Filter.eventually_atTop] at hevent
rcases hevent with ⟨N, hN⟩
refine ⟨N, ?_⟩
intro k hk p hp i j
have hopen := hK_open hp
have ha_pos : 0 < p.1 := hopen.1
have hb_pos : 0 < p.2 := hopen.2.2.1
have hs_pos : 0 < p.1 + p.2 := by linarith
have hs : p.1 + p.2 ≠ 0 := ne_of_gt hs_pos
have hqa : |p.1 / (p.1 + p.2)| ≤ 1 := by
rw [abs_of_nonneg (div_nonneg ha_pos.le hs_pos.le)]
rw [div_le_one hs_pos]
linarith
have hqb : |p.2 / (p.1 + p.2)| ≤ 1 := by
rw [abs_of_nonneg (div_nonneg hb_pos.le hs_pos.le)]
rw [div_le_one hs_pos]
linarith
have hQ_le : |(1 - stationaryProjection p.1 p.2) i j| ≤ 1 := by
fin_cases i <;> fin_cases j
· have h : 1 - p.2 / (p.1 + p.2) = p.1 / (p.1 + p.2) := by
field_simp [hs]
ring
simpa [stationaryProjection, Matrix.sub_apply, h] using hqa
· simpa [stationaryProjection, Matrix.sub_apply, abs_neg] using hqa
· simpa [stationaryProjection, Matrix.sub_apply, abs_neg] using hqb
· have h : 1 - p.1 / (p.1 + p.2) = p.2 / (p.1 + p.2) := by
field_simp [hs]
ring
simpa [stationaryProjection, Matrix.sub_apply, h] using hqb
have hentry :
((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j =
(1 - p.1 - p.2) ^ k * (1 - stationaryProjection p.1 p.2) i j := by
have hspec :=
transitionMatrix_pow_eq_spectral p.1 p.2 hs k
calc
((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j
=
(stationaryProjection p.1 p.2 +
(1 - p.1 - p.2) ^ k • (1 - stationaryProjection p.1 p.2) -
stationaryProjection p.1 p.2) i j := by
rw [hspec]
_ = (1 - p.1 - p.2) ^ k * (1 - stationaryProjection p.1 p.2) i j := by
simp [Matrix.sub_apply, Matrix.add_apply, Matrix.smul_apply]
have hgap_pow : |(1 - p.1 - p.2) ^ k| ≤ ρ ^ k := by
rw [abs_pow]
exact pow_le_pow_left₀ (abs_nonneg (1 - p.1 - p.2)) (hρ_bound p hp) k
have hbound :
|((transitionMatrix p.1 p.2) ^ k - stationaryProjection p.1 p.2) i j| ≤ ρ ^ k := by
rw [hentry, abs_mul]
calc
|(1 - p.1 - p.2) ^ k| * |(1 - stationaryProjection p.1 p.2) i j|
≤ ρ ^ k * 1 :=
mul_le_mul hgap_pow hQ_le (abs_nonneg _) (pow_nonneg hρ_nonneg k)
_ = ρ ^ k := by ring
exact hbound.trans (le_of_lt (hN k hk))
· refine ⟨0, ?_⟩
intro k hk p hp i j
exact elim (hne ⟨p, hp⟩)
2 supporting declarations (lemmas, instances)
-
one_minus_a_b_abs_lt_onetheorem — Pointwise spectral gap: |1 - a - b| < 1 when a + b lies strictly between zero and two.hypothesesconclusion|1 - a - b| < 1Proof (Lean source)
theorem one_minus_a_b_abs_lt_one {K : Type*} [CommRing K] [LinearOrder K] [IsStrictOrderedRing K] {a b : K} (hs_pos : 0 < a + b) (hs_lt_two : a + b < 2) : |1 - a - b| < 1 := by by_cases hle : a + b ≤ 1 · rw [abs_of_nonneg (by linarith)] linarith · have hgt : 1 < a + b := lt_of_not_ge hle rw [abs_of_neg (by linarith)] linarith -
one_minus_a_b_uniform_gap_on_compacttheorem — Uniform spectral gap on compact subsets of the open strip: the continuous function (a,b) ↦ |1 - a - b| attains its supremum when 0 < a + b < 2 at some point of K, and that supremum is strictly less than 1 by the pointwise bound.hypothesesconclusion∃ ρ : ℝ, ρ < 1 ∧ ∀ p ∈ K, |1 - p.1 - p.2| ≤ ρProof (Lean source)
theorem one_minus_a_b_uniform_gap_on_compact (K : Set (ℝ × ℝ)) (hK_compact : IsCompact K) (hK_open : K ⊆ {p : ℝ × ℝ | 0 < p.1 + p.2 ∧ p.1 + p.2 < 2}) : ∃ ρ : ℝ, ρ < 1 ∧ ∀ p ∈ K, |1 - p.1 - p.2| ≤ ρ := by by_cases hne : K.Nonempty · let f : ℝ × ℝ → ℝ := fun p => |1 - p.1 - p.2| have hf : ContinuousOn f K := by dsimp [f] fun_prop rcases hK_compact.exists_isMaxOn hne hf with ⟨pstar, hpstar, hpmax⟩ have hopen := hK_open hpstar have hmax_lt : f pstar < 1 := by dsimp [f] exact one_minus_a_b_abs_lt_one hopen.1 hopen.2 refine ⟨(f pstar + 1) / 2, ?_, ?_⟩ · linarith · intro p hp have hle : f p ≤ f pstar := isMaxOn_iff.mp hpmax p hp dsimp [f] at hle ⊢ linarith · refine ⟨0, by norm_num, ?_⟩ intro p hp exact elim (hne ⟨p, hp⟩)