Mathlib

conclusion

= (μ.map snd).bind (fun c : γ => (condDistrib fst snd μ c).map (fun b : β => (b, c)))

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)

Causalean.measure_eq_bind_marginal_condDistrib · Causalean/Mathlib/CondDistrib.lean:169

theorem condDistrib_map_comp reviewed

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*

MeasurableSpace Ω'

MeasurableSpace 𝒳

MeasurableSpace 𝒴

StandardBorelSpace 𝒴

Nonempty 𝒴

μ :

φ :

Ω → Ω'

g :

Ω' → 𝒴

f :

Ω' → 𝒳

hφ :

Measurable φ

hg :

Measurable g

hf :

Measurable f

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

Causalean.condDistrib_map_comp · Causalean/Mathlib/CondDistrib.lean:262

1 supporting declaration (lemmas, instances)

condDistrib_comp_right_measurableEquiv theorem — Push-forward invariance of condDistrib under a measurable equivalence of the conditioning variable.

hypotheses

α β Ω γ :

Type*
MeasurableSpace α
MeasurableSpace β
MeasurableSpace Ω
StandardBorelSpace Ω
Nonempty Ω
MeasurableSpace γ

μ :

Measure γ
IsFiniteMeasure μ

Y :

γ → Ω

X :

γ → α

e :

α ≃ᵐ β

hY :

Measurable Y

hX :

Measurable X

conclusion

∀ᵐ x ∂(μ.map X), condDistrib Y (e ∘ X) μ (e x)
= condDistrib Y X μ x

Proof (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]

Causalean.condDistrib_comp_right_measurableEquiv · Causalean/Mathlib/CondDistrib.lean:93

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

ProbabilityTheory

Given a sample space equipped with a σ-algebra, a treatment space equipped with a σ-algebra, a covariate space equipped with a σ-algebra, a nonempty standard Borel residual-coordinate space, and an outcome space equipped with a σ-algebra, let the sampling measure be finite, the covariate map and the residual-coordinate map map sample points to their respective spaces, and let the structural response map map a treatment, covariate, and residual coordinate to an outcome. If this structural response is jointly measurable, then the witness kernel assigns to each treatment--covariate pair the distribution of the structural response after drawing the residual coordinate from its conditional distribution given the covariate.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

𝒳 :

Type u_2

shared

𝒵 :

Type u_3

shared

𝒞 :

Type u_4

shared

𝒴 :

Type u_5

shared

μ :

Z :

Ω → 𝒵

C :

Ω → 𝒞

h :

𝒳 → 𝒵 → 𝒞 → 𝒴

hh :

Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)

def

witnessKernel μ hh :

Kernel (𝒳 × 𝒵) 𝒴

given by

clause 1

toFun p := (condDistrib C Z μ p.2).map (h p.1 p.2)

clause 2

measurable' := by 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 => ?_) 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] 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 ?_ exact (measurable_const.indicator hB).comp hh

ProbabilityTheory.witnessKernel · Causalean/Mathlib/CondDistribWitness.lean:45

theorem condDistrib_map_of_condDistrib_fst_eq reviewed

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

Ω :

Type u_1

shared

𝒳 :

Type u_2

shared

𝒵 :

Type u_3

shared

𝒞 :

Type u_4

shared

𝒴 :

Type u_5

shared

μ :

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)

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 := by fun_prop 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

ProbabilityTheory.condDistrib_map_of_condDistrib_fst_eq · Causalean/Mathlib/CondDistribWitness.lean:112

theorem condDistrib_map_of_funext reviewed

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

Ω :

Type u_1

shared

𝒵 :

Type u_3

shared

𝒞 :

Type u_4

shared

𝒴 :

Type u_5

shared

μ :

Z :

Ω → 𝒵

C :

Ω → 𝒞

H :

𝒵 → 𝒞 → 𝒴

hZ :

Measurable Z

hC :

Measurable C

hH :

Measurable (fun p : 𝒵 × 𝒞 => H p.1 p.2)

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

ProbabilityTheory.condDistrib_map_of_funext · Causalean/Mathlib/CondDistribWitness.lean:189

2 supporting declarations (lemmas, instances)

witnessKernel_apply lemma — Evaluating the witness kernel at a conditioning pair gives the residual conditional law pushed through the corresponding structural slice.

hypotheses

Ω :

Type u_1
shared

𝒳 :

Type u_2
shared

𝒵 :

Type u_3
shared

𝒞 :

Type u_4
shared

𝒴 :

Type u_5
shared

μ :

Measure Ω
IsFiniteMeasure μ

Z :

Ω → 𝒵

C :

Ω → 𝒞

h :

𝒳 → 𝒵 → 𝒞 → 𝒴

hh :

Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)

p :

𝒳 × 𝒵

conclusion

witnessKernel μ (Z := Z) (C := C) hh p = (condDistrib C Z μ p.2).map (h p.1 p.2)

Proof (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

ProbabilityTheory.witnessKernel_apply · Causalean/Mathlib/CondDistribWitness.lean:92
instIsMarkovKernel_witnessKernel instance — For every sample space, treatment space, covariate space, nonempty standard Borel residual-coordinate space, and outcome space, each equipped with the stated measurable structure, finite sampling measure, covariate map, residual-coordinate map, structural response map, and joint measurability of that response map, the witness kernel is a Markov kernel.

parameters

Ω :

Type u_1
shared

𝒳 :

Type u_2
shared

𝒵 :

Type u_3
shared

𝒞 :

Type u_4
shared

𝒴 :

Type u_5
shared

μ :

Measure Ω
IsFiniteMeasure μ

Z :

Ω → 𝒵

C :

Ω → 𝒞

h :

𝒳 → 𝒵 → 𝒞 → 𝒴

hh :

Measurable (fun p : (𝒳 × 𝒵) × 𝒞 => h p.1.1 p.1.2 p.2)

instance

instIsMarkovKernel_witnessKernel μ hh :
IsMarkovKernel (witnessKernel μ (Z := Z) (C := C) hh)

given by

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

ProbabilityTheory.instIsMarkovKernel_witnessKernel · Causalean/Mathlib/CondDistribWitness.lean:100

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

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

Ω :

Type u_1

shared

ι :

Type u_2

shared

μ :

shared

l :

Filter ι

shared

IsProbabilityMeasure μ

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)

MeasureTheory.TendstoInDistribution.const_mul_of_tendsto_const · Causalean/Mathlib/ConvergenceInDistribution.lean:62

theorem tendsto_map_mul_of_tendsto reviewed

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

ι :

Type*

Filter ι

ι → ProbabilityMeasure ℝ

ν :

ProbabilityMeasure ℝ

a :

ι → ℝ

a₀ :

ℝ

hν :

Tendsto νs l (𝓝 ν)

ha :

Tendsto a l (𝓝 a₀)

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

MeasureTheory.ProbabilityMeasure.tendsto_map_mul_of_tendsto · Causalean/Mathlib/ConvergenceInDistribution.lean:102

3 supporting declarations (lemmas, instances)

tendstoInMeasure_const_of_tendsto_real lemma — 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.

hypotheses

Ω :

Type u_1
shared

ι :

Type u_2
shared

μ :

Measure Ω
shared

l :

Filter ι
shared

E :

Type*
SeminormedAddCommGroup E
ι → E
E

ha :

Tendsto a l (𝓝 a₀)

conclusion

TendstoInMeasure μ (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

MeasureTheory.tendstoInMeasure_const_of_tendsto_real · Causalean/Mathlib/ConvergenceInDistribution.lean:33
tendstoInMeasure_const_of_tendsto lemma — Alias for tendstoInMeasure_const_of_tendsto_real whose name reflects that the result holds in any seminormed additive commutative group.

hypotheses

Ω :

Type u_1
shared

ι :

Type u_2
shared

μ :

Measure Ω
shared

l :

Filter ι
shared

E :

Type*
SeminormedAddCommGroup E
ι → E
E

ha :

Tendsto a l (𝓝 a₀)

conclusion

TendstoInMeasure μ (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

MeasureTheory.tendstoInMeasure_const_of_tendsto · Causalean/Mathlib/ConvergenceInDistribution.lean:54
map_mul_eq_map_prod_dirac lemma — Multiplying a deterministic real value and a random draw has the same distribution as scaling that random draw by the deterministic value.

hypotheses

c :

ℝ

ν :

ProbabilityMeasure ℝ

conclusion

((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 ℝ))

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

MeasureTheory.ProbabilityMeasure.map_mul_eq_map_prod_dirac · Causalean/Mathlib/ConvergenceInDistribution.lean:84

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_toReal_of_uncurry★ measurable_eLpNorm_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_toReal_of_uncurry; the sub-σ-algebra version, where joint measurability factors through mΩ × MeasurableSpace X, is measurable_eLpNorm_toReal_of_uncurry_of_factor.

lemma measurable_eLpNorm_toReal_of_uncurry reviewed

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

Ω :

Type u_1

shared

X :

Type u_2

shared

P :

Measure X

SFinite P

E :

Type*

MeasurableSpace E

TopologicalSpace E

ContinuousENorm E

OpensMeasurableSpace E

Ω → X → E

p :

ℝ≥0∞

hp_zero :

p ≠ 0

hp_top :

p ≠ ⊤

hg :

Measurable (uncurry g)

conclusion

Measurable (fun ω => (eLpNorm (g ω) p P).toReal)

Proof (Lean source)

@[fun_prop] 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) := 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

Causalean.Mathlib.measurable_eLpNorm_toReal_of_uncurry · Causalean/Mathlib/ELpNormMeasurable.lean:50

lemma measurable_eLpNorm_toReal_of_uncurry_of_factor reviewed

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

Ω :

Type u_1

shared

X :

Type u_2

shared

mΩ :

P :

Measure X

SFinite P

E :

Type*

MeasurableSpace E

TopologicalSpace E

ContinuousENorm E

OpensMeasurableSpace E

Ω → X → E

p :

ℝ≥0∞

hp_zero :

p ≠ 0

hp_top :

p ≠ ⊤

hg_uncurry :

@Measurable (Ω × X) E (@instMeasurableSpace Ω X mΩ inferInstance) inferInstance (uncurry g)

conclusion

Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal)

Proof (Lean source)

@[fun_prop] 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) := 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

Causalean.Mathlib.measurable_eLpNorm_toReal_of_uncurry_of_factor · Causalean/Mathlib/ELpNormMeasurable.lean:90

2 supporting declarations (lemmas, instances)

measurable_eLpNorm_two_toReal_of_uncurry lemma — Vestigial _two_ spelling of measurable_eLpNorm_toReal_of_uncurry; the exponent p was never fixed to 2.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

MeasurableSpace Ω

P :

Measure X
SFinite P

E :

Type*
MeasurableSpace E
TopologicalSpace E
ContinuousENorm E
OpensMeasurableSpace E
Ω → X → E

p :

ℝ≥0∞

hp_zero :

p ≠ 0

hp_top :

p ≠ ⊤

hg :

Measurable (uncurry g)

conclusion

Measurable (fun ω => (eLpNorm (g ω) p P).toReal)

Proof (Lean source)

@[deprecated measurable_eLpNorm_toReal_of_uncurry (since := "2026-08-29")] 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) := measurable_eLpNorm_toReal_of_uncurry hp_zero hp_top hg

Causalean.Mathlib.measurable_eLpNorm_two_toReal_of_uncurry · Causalean/Mathlib/ELpNormMeasurable.lean:78
measurable_eLpNorm_two_toReal_of_uncurry_of_factor lemma — Vestigial _two_ spelling of measurable_eLpNorm_toReal_of_uncurry_of_factor; the exponent p was never fixed to 2.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

mΩ :

MeasurableSpace Ω

P :

Measure X
SFinite P

E :

Type*
MeasurableSpace E
TopologicalSpace E
ContinuousENorm E
OpensMeasurableSpace E
Ω → X → E

p :

ℝ≥0∞

hp_zero :

p ≠ 0

hp_top :

p ≠ ⊤

hg_uncurry :

@Measurable (Ω × X) E (@instMeasurableSpace Ω X mΩ inferInstance) inferInstance (uncurry g)

conclusion

Measurable[mΩ] (fun ω => (eLpNorm (g ω) p P).toReal)

Proof (Lean source)

@[deprecated measurable_eLpNorm_toReal_of_uncurry_of_factor (since := "2026-08-29")] 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) := measurable_eLpNorm_toReal_of_uncurry_of_factor hp_zero hp_top hg_uncurry

Causalean.Mathlib.measurable_eLpNorm_two_toReal_of_uncurry_of_factor · Causalean/Mathlib/ELpNormMeasurable.lean:120

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

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, and a vector, the orthogonal residual is the vector minus its orthogonal projection onto that subspace.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

v :

def

residualize H v :

given by

v - H.orthogonalProjectionFn v

Causalean.Mathlib.FWL.residualize · Causalean/Mathlib/FWL.lean:93

def residualizeL reviewed

Causalean.Mathlib.FWL

For a real inner-product space and a subspace that admits an orthogonal projection, the residual-maker linear map sends each vector to its orthogonal residual after removal of its projection onto that subspace.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

def

residualizeL H :

V →L[ℝ] V

given by

id ℝ V - H.starProjection

Causalean.Mathlib.FWL.residualizeL · Causalean/Mathlib/FWL.lean:106

def fittedValue reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a finite number of regressors, a tuple of regressor vectors, and a vector of real coefficients, the fitted value is the sum of each regressor multiplied by its corresponding coefficient.

Definition (Lean source)

parameters

V :

Type u_1

shared

K :

ℕ

shared

X :

Fin K → V

shared

β :

Fin K → ℝ

def

fittedValue X β :

given by

∑ j, β j • X j

Causalean.Mathlib.FWL.fittedValue · Causalean/Mathlib/FWL.lean:153

def gramResid reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, and a tuple of regressor vectors, the residualized Gram matrix has as its $(j,k)$ entry the inner product of the orthogonal residuals of the $j$ th and $k$ th regressors.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

def

gramResid H X :

Matrix (Fin K) (Fin K) ℝ

given by

fun j k => inner ℝ (residualize H (X j)) (residualize H (X k))

Causalean.Mathlib.FWL.gramResid · Causalean/Mathlib/FWL.lean:187

def residInnerVec reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, a tuple of regressor vectors, and an outcome vector, the residualized inner-product vector assigns to each regressor index the inner product of that regressor's orthogonal residual with the outcome.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

def

residInnerVec H X Y :

Fin K → ℝ

given by

fun j => inner ℝ (residualize H (X j)) Y

Causalean.Mathlib.FWL.residInnerVec · Causalean/Mathlib/FWL.lean:200

def fwlCoef reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, a tuple of regressor vectors, and an outcome vector, the Frisch–Waugh–Lovell coefficient vector is the inverse residualized Gram matrix multiplied by the vector of inner products between residualized regressors and the outcome.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

def

fwlCoef H X Y :

Fin K → ℝ

given by

(gramResid H X)⁻¹.mulVec (residInnerVec H X Y)

Causalean.Mathlib.FWL.fwlCoef · Causalean/Mathlib/FWL.lean:212

def residualizedObjective reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a subspace that admits an orthogonal projection, a finite number of regressors, a tuple of regressor vectors, an outcome vector, and a vector of real coefficients, the residualized least-squares objective is the squared norm of the orthogonal residual of the outcome minus the fitted value formed from the orthogonal residuals of the regressors.

Definition (Lean source)

parameters

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

β :

Fin K → ℝ

def

residualizedObjective H X Y β :

ℝ

given by

inner ℝ (residualize H Y - fittedValue (fun j => residualize H (X j)) β) (residualize H Y - fittedValue (fun j => residualize H (X j)) β)

Causalean.Mathlib.FWL.residualizedObjective · Causalean/Mathlib/FWL.lean:242

def originalObjective reviewed

Causalean.Mathlib.FWL

For a real inner-product space, a finite number of regressors, a tuple of regressor vectors, an outcome vector, a vector of real coefficients, and a nuisance vector, the original least-squares objective is the squared norm of the outcome minus its fitted value and minus the nuisance vector.

Definition (Lean source)

parameters

V :

Type u_1

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

β :

Fin K → ℝ

h :

def

originalObjective X Y β h :

ℝ

given by

inner ℝ (Y - fittedValue X β - h) (Y - fittedValue X β - h)

Causalean.Mathlib.FWL.originalObjective · Causalean/Mathlib/FWL.lean:252

theorem fwlCoef_original_minimizes reviewed

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

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

hh :

h ∈ H

conclusion

originalObjective X Y (fwlCoef H X Y) (H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y)))

≤ originalObjective X Y β h

Proof (Lean source)

theorem fwlCoef_original_minimizes (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

Causalean.Mathlib.FWL.fwlCoef_original_minimizes · Causalean/Mathlib/FWL.lean:400 · uses fittedValue , fwlCoef , gramResid , originalObjective

theorem original_minimizer_eq_fwlCoef_projection reviewed

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

V :

Type u_1

shared

H :

Submodule ℝ V

shared

K :

ℕ

shared

X :

Fin K → V

shared

Y :

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

hh :

h ∈ H

hmin :

∀ (γ : Fin K → ℝ) {g : V}

g ∈ H

then

originalObjective X Y β h ≤ originalObjective X Y γ g

conclusion

conclusion 1

β = fwlCoef H X Y

conclusion 2

h = H.orthogonalProjectionFn (Y - fittedValue X (fwlCoef H X Y))

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β]

Causalean.Mathlib.FWL.original_minimizer_eq_fwlCoef_projection · Causalean/Mathlib/FWL.lean:474 · uses fittedValue , fwlCoef , gramResid , originalObjective

18 supporting declarations (lemmas, instances)

residualize_def lemma — Residualization is the original vector minus its orthogonal projection onto the nuisance subspace.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v :

V

conclusion

residualize H v = v - H.orthogonalProjectionFn v

Proof (Lean source)

@[simp] lemma residualize_def (v : V) : residualize H v = v - H.orthogonalProjectionFn v := rfl

Causalean.Mathlib.FWL.residualize_def · Causalean/Mathlib/FWL.lean:101
residualizeL_apply lemma — Applying the residual-maker linear map gives the residualized vector.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v :

V

conclusion

residualizeL H v = residualize H v

Proof (Lean source)

@[simp] lemma residualizeL_apply (v : V) : residualizeL H v = residualize H v := by simp [residualizeL, residualize]

Causalean.Mathlib.FWL.residualizeL_apply · Causalean/Mathlib/FWL.lean:114
inner_residualize_of_mem lemma — Residual is orthogonal to every element of H. This is the defining property of the orthogonal residual.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v :

V

w :

V

hw :

w ∈ H

conclusion

inner ℝ (residualize H v) w = 0

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

Causalean.Mathlib.FWL.inner_residualize_of_mem · Causalean/Mathlib/FWL.lean:119
residualize_inner_swap_right lemma — Symmetric residualization in the right slot. Since M_H is self-adjoint and idempotent, ⟨X̃, Y⟩ = ⟨X̃, Ỹ⟩.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

v w :

V

conclusion

inner ℝ (residualize H v) w = inner ℝ (residualize H v) (residualize H w)

Proof (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]

Causalean.Mathlib.FWL.residualize_inner_swap_right · Causalean/Mathlib/FWL.lean:127
fittedValue_sub lemma — Fitted values are linear in the coefficient vector.

hypotheses

V :

Type u_1
shared

K :

ℕ
shared

X :

Fin K → V
shared

β γ :

Fin K → ℝ

conclusion

fittedValue 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]

Causalean.Mathlib.FWL.fittedValue_sub · Causalean/Mathlib/FWL.lean:159
residualize_fittedValue lemma — Residualization commutes with forming a fitted value.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

β :

Fin K → ℝ

conclusion

residualize 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]

Causalean.Mathlib.FWL.residualize_fittedValue · Causalean/Mathlib/FWL.lean:165
residualize_regressionResidual lemma — Residualization of the raw regression residual is the residualized outcome minus the fitted value of the residualized regressors.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

conclusion

residualize 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 β]

Causalean.Mathlib.FWL.residualize_regressionResidual · Causalean/Mathlib/FWL.lean:174
gramResid_apply lemma — Each entry of the residualized Gram matrix is the inner product of two residualized regressors.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

j k :

Fin K

conclusion

gramResid H X j k = inner ℝ (residualize H (X j)) (residualize H (X k))

Proof (Lean source)

@[simp] lemma gramResid_apply (j k : Fin K) : gramResid H X j k = inner ℝ (residualize H (X j)) (residualize H (X k)) := rfl

Causalean.Mathlib.FWL.gramResid_apply · Causalean/Mathlib/FWL.lean:194
residInnerVec_apply lemma — Each entry of the residualized right-hand side is the inner product of a residualized regressor with the outcome.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

j :

Fin K

conclusion

residInnerVec H X Y j = inner ℝ (residualize H (X j)) Y

Proof (Lean source)

@[simp] lemma residInnerVec_apply (Y : V) (j : Fin K) : residInnerVec H X Y j = inner ℝ (residualize H (X j)) Y := rfl

Causalean.Mathlib.FWL.residInnerVec_apply · Causalean/Mathlib/FWL.lean:207
gramResid_mulVec_fwlCoef lemma — 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⟩).

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

conclusion

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

Proof (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]

Causalean.Mathlib.FWL.gramResid_mulVec_fwlCoef · Causalean/Mathlib/FWL.lean:220
residInnerVec_eq_residualize_right lemma — 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.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

conclusion

residInnerVec H X Y = residInnerVec H X (residualize H Y)

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

Causalean.Mathlib.FWL.residInnerVec_eq_residualize_right · Causalean/Mathlib/FWL.lean:234
inner_residualizedRegressor_fwlResidual lemma — The residual left by fwlCoef is orthogonal to every residualized regressor. This is the normal-equation form used in the completing-square argument.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

j :

Fin K

conclusion

inner ℝ (residualize H (X j)) (residualize H Y - fittedValue (fun k => residualize H (X k)) (fwlCoef H X Y))
= 0

Proof (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

Causalean.Mathlib.FWL.inner_residualizedRegressor_fwlResidual · Causalean/Mathlib/FWL.lean:259
residualizedObjective_eq_fwlCoef_add_error theorem — Completing-square identity for the residualized objective around the FWL coefficient.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

conclusion

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))

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

Causalean.Mathlib.FWL.residualizedObjective_eq_fwlCoef_add_error · Causalean/Mathlib/FWL.lean:285
fwlCoef_residualized_minimizes theorem — The FWL coefficient minimizes the residualized least-squares objective.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

conclusion

residualizedObjective H X Y (fwlCoef H X Y) ≤ residualizedObjective H X Y β

Proof (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)

Causalean.Mathlib.FWL.fwlCoef_residualized_minimizes · Causalean/Mathlib/FWL.lean:334
originalObjective_eq_residualizedObjective_add_projectionError theorem — 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.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

h :

V

hh :

h ∈ H

conclusion

originalObjective 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

Causalean.Mathlib.FWL.originalObjective_eq_residualizedObjective_add_projectionError · Causalean/Mathlib/FWL.lean:342
residualizedObjective_le_originalObjective theorem — For fixed β, the residualized objective is the minimum of the original objective over the nuisance subspace H.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

h :

V

hh :

h ∈ H

conclusion

residualizedObjective H X Y β ≤ originalObjective X Y β h

Proof (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)

Causalean.Mathlib.FWL.residualizedObjective_le_originalObjective · Causalean/Mathlib/FWL.lean:380
originalObjective_projection_eq_residualizedObjective theorem — At the nuisance projection, the original objective equals the residualized objective.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

β :

Fin K → ℝ

conclusion

originalObjective 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

Causalean.Mathlib.FWL.originalObjective_projection_eq_residualizedObjective · Causalean/Mathlib/FWL.lean:389
fwlCoef_eq_of_original_minimizer theorem — 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.

hypotheses

V :

Type u_1
shared

H :

Submodule ℝ V
shared

K :

ℕ
shared

X :

Fin K → V
shared

Y :

V

hQ :

IsUnit (gramResid H X).det

β :

Fin K → ℝ

h :

V

hh :

h ∈ H

hmin :

∀ (γ : Fin K → ℝ) {g : V}
if
g ∈ H
then
originalObjective X Y β h ≤ originalObjective X Y γ g

conclusion

β = fwlCoef H X Y

Proof (Lean source)

theorem fwlCoef_eq_of_original_minimizer (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

Causalean.Mathlib.FWL.fwlCoef_eq_of_original_minimizer · Causalean/Mathlib/FWL.lean:423

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

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*

MeasurableSpace X

Measure X

IsProbabilityMeasure P

ι :

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 :

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

conclusion

∫⁻ ω, ofReal (((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ

≤ ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ

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)

Causalean.Mathlib.iid_centered_sum_sq_lintegral_le · Causalean/Mathlib/IIDCenteredSum.lean:465

7 supporting declarations (lemmas, instances)

lintegral_ofReal_inv_sqrt_smul_sum_sq_le lemma — 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.

hypotheses

Ω :

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 ω ∂μ

conclusion

∫⁻ ω, ofReal (((sqrt (s.card : ℝ))⁻¹ * ∑ i ∈ s, Y i ω) ^ 2) ∂μ ≤ ∫⁻ ω, B ω ∂μ

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]

Causalean.Mathlib.lintegral_ofReal_inv_sqrt_smul_sum_sq_le · Causalean/Mathlib/IIDCenteredSum.lean:65
eLpNorm_two_sq_toReal_eq_integral_sq lemma — The square of a square-integrable variable's L2 norm equals the integral of its squared norm, for any measure.

hypotheses

X :

Type*
MeasurableSpace X
Measure X

E :

Type*
NormedAddCommGroup E
X → E

hf :

MemLp f 2 P

conclusion

ofReal ((eLpNorm f 2 P).toReal ^ 2) = ofReal (∫ x, ‖f x‖ ^ 2 ∂P)

Proof (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]

Causalean.Mathlib.eLpNorm_two_sq_toReal_eq_integral_sq · Causalean/Mathlib/IIDCenteredSum.lean:123
centered_sq_lintegral_le_eLpNorm_two_sq lemma — Centering a square-integrable real variable cannot increase its second moment beyond its uncentered L2 energy under a probability distribution.

hypotheses

X :

Type*
MeasurableSpace X
Measure X

IsProbabilityMeasure P

f :

X → ℝ

hf :

MemLp f 2 P

conclusion

∫⁻ x, ofReal ((f x - ∫ y, f y ∂P) ^ 2) ∂P
≤ ofReal ((eLpNorm f 2 P).toReal ^ 2)

Proof (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

Causalean.Mathlib.centered_sq_lintegral_le_eLpNorm_two_sq · Causalean/Mathlib/IIDCenteredSum.lean:153
pi_centered_sum_sq_lintegral_le lemma — 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

ι :

Type*
Fintype ι
ι → Type*

∀ i, MeasurableSpace (X i)

P :

∀ i, Measure (X i)
∀ i, IsProbabilityMeasure (P i)

f :

∀ i
if
X i
then
ℝ

hf :

∀ i, MemLp (f i) 2 (P i)

conclusion

∫⁻ 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)

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)]

Causalean.Mathlib.pi_centered_sum_sq_lintegral_le · Causalean/Mathlib/IIDCenteredSum.lean:179
indep_trim_prod_map_eq lemma — 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.

hypotheses

Ω β :

Type*
MeasurableSpace Ω
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Ω μ

conclusion

@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

Causalean.Mathlib.indep_trim_prod_map_eq · Causalean/Mathlib/IIDCenteredSum.lean:259
iid_centered_sum_sq_lintegral_unscaled_le_of_joined_law lemma — 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*
MeasurableSpace Ω
MeasurableSpace X
Measure Ω
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

conclusion

∫⁻ ω, ofReal ((∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ
≤ (s.card : ENNReal) * ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ

Proof (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 fun_prop 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_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]

Causalean.Mathlib.iid_centered_sum_sq_lintegral_unscaled_le_of_joined_law · Causalean/Mathlib/IIDCenteredSum.lean:284
iid_centered_sum_sq_lintegral_unscaled_le lemma — 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*
MeasurableSpace Ω
MeasurableSpace X
Measure Ω
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

conclusion

∫⁻ ω, ofReal ((∑ i ∈ s, (g ω (W i ω) - ∫ x, g ω x ∂P)) ^ 2) ∂μ
≤ (s.card : ENNReal) * ∫⁻ ω, ofReal ((eLpNorm (g ω) 2 P).toReal ^ 2) ∂μ

Proof (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

Causalean.Mathlib.iid_centered_sum_sq_lintegral_unscaled_le · Causalean/Mathlib/IIDCenteredSum.lean:406

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

Causalean

Given an index collection, a family of coordinate value spaces, and a finite coordinate block, the coordinate-block projection maps a full coordinate assignment to the assignment obtained by retaining exactly the coordinates in that block.

Definition (Lean source)

parameters

ι :

Type*

ι → Type*

S :

Finset ι

def

finsetCoordProj S :

(∀ i, Ω i) → ((i : {i // i ∈ S}) → Ω i.val)

given by

fun x i => x i.val

Causalean.finsetCoordProj · Causalean/Mathlib/Indep.lean:88

def finsetCoordProjFromCondResidual reviewed

Causalean

Given an index collection whose equality is decidable, a family of coordinate value spaces, a target coordinate block and a conditioning block, the residual-reassembly map reconstructs an assignment on the target block from an assignment on the conditioning block and an assignment on those target coordinates outside that block.

Definition (Lean source)

parameters

ι :

Type*

DecidableEq ι

ι → Type*

S U :

Finset ι

def

finsetCoordProjFromCondResidual S U :

(((i : {i // i ∈ U}) → Ω i.val) × ((i : {i // i ∈ S \ U}) → Ω i.val)) → ((i : {i // i ∈ S}) → Ω i.val)

given by

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⟩⟩

Causalean.finsetCoordProjFromCondResidual · Causalean/Mathlib/Indep.lean:107

def finsetCoordProjPairFromUnion reviewed

Causalean

Given an index collection whose equality is decidable, a family of coordinate value spaces, and finite coordinate blocks, the union-sub-block extraction map maps an assignment on their union to the pair of its restrictions to the first and second blocks.

Definition (Lean source)

parameters

ι :

Type*

DecidableEq ι

ι → Type*

A B :

Finset ι

def

finsetCoordProjPairFromUnion A B :

(((i : {i // i ∈ A ∪ B}) → Ω i.val) → ((i : {i // i ∈ A}) → Ω i.val) × ((i : {i // i ∈ B}) → Ω i.val))

given by

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)⟩)

Causalean.finsetCoordProjPairFromUnion · Causalean/Mathlib/Indep.lean:149

theorem condIndepFun_pi_cond_residual_of_disjoint reviewed

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

Causalean.condIndepFun_pi_cond_residual_of_disjoint · Causalean/Mathlib/Indep.lean:222 · uses finsetCoordProj , measurable_finsetCoordProj

theorem condIndepFun_pi_of_inter_subset reviewed

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

ι :

Type*

DecidableEq ι

Finite ι

ι → Type*

∀ 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

Causalean.condIndepFun_pi_of_inter_subset · Causalean/Mathlib/Indep.lean:349 · uses finsetCoordProj , measurable_finsetCoordProj

10 supporting declarations (lemmas, instances)

indepFun_pi_of_disjoint theorem — 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 T

conclusion

letI : 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)

Causalean.indepFun_pi_of_disjoint · Causalean/Mathlib/Indep.lean:71
measurable_finsetCoordProj theorem — finsetCoordProj is measurable.

hypotheses

ι :

Type*
ι → Type*

∀ i, MeasurableSpace (Ω i)

S :

Finset ι

conclusion

Measurable (finsetCoordProj (Ω := Ω) S)

Proof (Lean source)

@[fun_prop] 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

Causalean.measurable_finsetCoordProj · Causalean/Mathlib/Indep.lean:97
measurable_finsetCoordProjFromCondResidual theorem — The residual reassembly map is measurable.

hypotheses

ι :

Type*
DecidableEq ι
ι → Type*

∀ i, MeasurableSpace (Ω i)

S U :

Finset ι

conclusion

Measurable (finsetCoordProjFromCondResidual (Ω := Ω) S U)

Proof (Lean source)

@[fun_prop] 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

Causalean.measurable_finsetCoordProjFromCondResidual · Causalean/Mathlib/Indep.lean:123
finsetCoordProjFromCondResidual_comp theorem — Reassembling π_U with the residual projection π_{S \ U} gives π_S.

hypotheses

ι :

Type*
DecidableEq ι
ι → Type*

S U :

Finset ι

conclusion

finsetCoordProjFromCondResidual (Ω := Ω) S U ∘ (fun x => (finsetCoordProj (Ω := Ω) U x, finsetCoordProj (Ω := Ω) (S \ U) x))
= finsetCoordProj (Ω := Ω) S

Proof (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]

Causalean.finsetCoordProjFromCondResidual_comp · Causalean/Mathlib/Indep.lean:138
measurable_finsetCoordProjPairFromUnion theorem — The union sub-block extraction map is measurable.

hypotheses

ι :

Type*
DecidableEq ι
ι → Type*

∀ i, MeasurableSpace (Ω i)

A B :

Finset ι

conclusion

Measurable (finsetCoordProjPairFromUnion (Ω := Ω) A B)

Proof (Lean source)

@[fun_prop] 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})

Causalean.measurable_finsetCoordProjPairFromUnion · Causalean/Mathlib/Indep.lean:162
finsetCoordProjPairFromUnion_comp theorem — Projecting to A ∪ B and then extracting the two sub-blocks gives the pair of direct projections to A and B.

hypotheses

ι :

Type*
DecidableEq ι
ι → Type*

A B :

Finset ι

conclusion

finsetCoordProjPairFromUnion (Ω := Ω) 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

Causalean.finsetCoordProjPairFromUnion_comp · Causalean/Mathlib/Indep.lean:178
condIndepFun_bot_of_indepFun theorem — 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.

hypotheses

Ω :

Type*
MeasurableSpace Ω
StandardBorelSpace Ω

β γ :

Type*
MeasurableSpace β
MeasurableSpace γ
Ω → β
Ω → γ

hf :

Measurable f

hg :

Measurable g

μ :

Measure Ω
IsProbabilityMeasure μ

h :

IndepFun f g μ

conclusion

CondIndepFun ⊥ bot_le f g μ

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]

Causalean.condIndepFun_bot_of_indepFun · Causalean/Mathlib/Indep.lean:190
comap_eq_bot_of_subsingleton theorem — 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

α β :

Type*
MeasurableSpace β
Subsingleton β

f :

α → β

conclusion

comap f inferInstance = (⊥ : MeasurableSpace α)

Proof (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)

Causalean.comap_eq_bot_of_subsingleton · Causalean/Mathlib/Indep.lean:412
indepFun_of_map theorem — Pushforward bridge for IndepFun: if X ∘ φ ⟂ᵢ Y ∘ φ under ν, then X ⟂ᵢ Y under ν.map φ. Analogue of LocalMarkov.condIndepFun_of_map at the IndepFun level.

hypotheses

α β γ δ :

Type*
MeasurableSpace α
MeasurableSpace β
MeasurableSpace γ
MeasurableSpace δ
Measure α
α → β

hφ :

AEMeasurable φ ν

X :

β → γ

hX :

Measurable X

Y :

β → δ

hY :

Measurable Y

h :

IndepFun (X ∘ φ) (Y ∘ φ) ν

conclusion

IndepFun 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

Causalean.indepFun_of_map · Causalean/Mathlib/Indep.lean:435
condIndepFun_of_indepFun_indep theorem — 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.

hypotheses

Ω β γ δ :

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) μ

conclusion

CondIndepFun (comap Z inferInstance) _hZ.comap_le X Y μ

Proof (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 ω)) := by fun_prop 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]

Causalean.condIndepFun_of_indepFun_indep · Causalean/Mathlib/Indep.lean:458

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

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

Ω α β :

Type*

MeasurableSpace α

MeasurableSpace β

Ω → α

Ω → β

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)

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]

ProbabilityTheory.IndepFun.integral_restrict_preimage_eq_mul · Causalean/Mathlib/IndepIntegral.lean:23

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

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Ω

μ :