Mathlib.Probability.Independence.Conditional.ThreeBlockShiftedProduct
Held-out scores are shifted by measurable training-block functions.
ThreeBlockShiftedProduct 2 core · 2 supporting Held-out scores are shifted by measurable training-block functions. ★ condCov_shiftedThreeBlockProduct
Shifted three-block moments and covariance
Held-out scores are shifted by measurable training-block functions. The results give their conditional first moments, cross moment, and covariance under a finite product probability law.
def shiftedThreeBlockProduct reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
The training block, three evaluation blocks, one held-out score for each block, and one training-block shift for each score define the shifted three-block product, by multiplying the three held-out scores after subtracting their respective shifts.
theorem condCov_shiftedThreeBlockProduct reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
A finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness and pairwise evaluation disjointness, two held-out-score families, two training-shift families, measurability, integrability of base scores and shifts, integrable local cross products, square-integrable shifted scores, integrable first shifted pairs, an integrable first shifted cross pair, and square-integrable shifted three-block products imply that the conditional covariance of the two shifted three-block products given the training block almost surely equals the product over the three blocks of the blockwise covariance plus the product of the two shifted held-out means, minus the product over all blocks of both families' shifted held-out means, where a shifted held-out mean is the unconditional mean of a held-out score minus its training shift.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
B0 :
Finset ι
htrain :
∀ t, Disjoint B0 (B t)
f g :
(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ
a b :
(t : Fin 3) → ((i : {i // i ∈ B0}) → Ω i.val) → ℝ
hfmeas :
∀ t, Measurable (f t)
hgmeas :
∀ t, Measurable (g t)
hameas :
∀ t, Measurable (a t)
hbmeas :
∀ t, Measurable (b t)
hf :
∀ t, Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x)) (Measure.pi μ)
hg :
∀ t, Integrable (fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x)) (Measure.pi μ)
ha :
∀ t, Integrable (fun x : ∀ i, Ω i => a t (finsetCoordProj B0 x)) (Measure.pi μ)
hb :
∀ t, Integrable (fun x : ∀ i, Ω i => b t (finsetCoordProj B0 x)) (Measure.pi μ)
hfg :
∀ t,
Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) * g t (finsetCoordProj (B t) x)) (Measure.pi μ)
hflp :
∀ t,
MemLp (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) - a t (finsetCoordProj B0 x)) 2 (Measure.pi μ)
hglp :
∀ t,
MemLp (fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x) - b t (finsetCoordProj B0 x)) 2 (Measure.pi μ)
hf01 :
Integrable (fun x : ∀ i, Ω i => (f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) * (f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x))) (Measure.pi μ)
hg01 :
Integrable (fun x : ∀ i, Ω i => (g 0 (finsetCoordProj (B 0) x) - b 0 (finsetCoordProj B0 x)) * (g 1 (finsetCoordProj (B 1) x) - b 1 (finsetCoordProj B0 x))) (Measure.pi μ)
hcross01 :
Integrable (fun x : ∀ i, Ω i => ((f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) * (g 0 (finsetCoordProj (B 0) x) - b 0 (finsetCoordProj B0 x))) * ((f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x)) * (g 1 (finsetCoordProj (B 1) x) - b 1 (finsetCoordProj B0 x)))) (Measure.pi μ)
hflpProd :
MemLp (shiftedThreeBlockProduct B0 B f a) 2 (Measure.pi μ)
hglpProd :
MemLp (shiftedThreeBlockProduct B0 B g b) 2 (Measure.pi μ)
conclusion
(fun x => condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y => shiftedThreeBlockProduct B0 B f a y * shiftedThreeBlockProduct B0 B g b y) x - condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (shiftedThreeBlockProduct B0 B f a) x * condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (shiftedThreeBlockProduct B0 B g b) x)
=ᵐ[Measure.pi μ] (fun x => (∏ t : Fin 3, (covariance (fun y : ∀ i, Ω i => f t (finsetCoordProj (B t) y)) (fun y : ∀ i, Ω i => g t (finsetCoordProj (B t) y)) (Measure.pi μ) + ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)) * ((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) - b t (finsetCoordProj B0 x)))) - (∏ t : Fin 3, ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x))) * (∏ t : Fin 3, ((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) - b t (finsetCoordProj B0 x))))
Proof (Lean source)
theorem condCov_shiftedThreeBlockProduct
(μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)]
(B0 : Finset ι) (B : Fin 3 → Finset ι)
(htrain : ∀ t, Disjoint B0 (B t))
(heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)))
(f g : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ)
(a b : (t : Fin 3) → ((i : {i // i ∈ B0}) → Ω i.val) → ℝ)
(hfmeas : ∀ t, Measurable (f t)) (hgmeas : ∀ t, Measurable (g t))
(hameas : ∀ t, Measurable (a t)) (hbmeas : ∀ t, Measurable (b t))
(hf : ∀ t, Integrable
(fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x)) (Measure.pi μ))
(hg : ∀ t, Integrable
(fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x)) (Measure.pi μ))
(ha : ∀ t, Integrable
(fun x : ∀ i, Ω i => a t (finsetCoordProj B0 x)) (Measure.pi μ))
(hb : ∀ t, Integrable
(fun x : ∀ i, Ω i => b t (finsetCoordProj B0 x)) (Measure.pi μ))
(hfg : ∀ t, Integrable (fun x : ∀ i, Ω i =>
f t (finsetCoordProj (B t) x) * g t (finsetCoordProj (B t) x))
(Measure.pi μ))
(hflp : ∀ t, MemLp
(fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) - a t (finsetCoordProj B0 x))
2 (Measure.pi μ))
(hglp : ∀ t, MemLp
(fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x) - b t (finsetCoordProj B0 x))
2 (Measure.pi μ))
(hf01 : Integrable (fun x : ∀ i, Ω i =>
(f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) *
(f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x)))
(Measure.pi μ))
(hg01 : Integrable (fun x : ∀ i, Ω i =>
(g 0 (finsetCoordProj (B 0) x) - b 0 (finsetCoordProj B0 x)) *
(g 1 (finsetCoordProj (B 1) x) - b 1 (finsetCoordProj B0 x)))
(Measure.pi μ))
(hcross01 : Integrable (fun x : ∀ i, Ω i =>
((f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) *
(g 0 (finsetCoordProj (B 0) x) - b 0 (finsetCoordProj B0 x))) *
((f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x)) *
(g 1 (finsetCoordProj (B 1) x) - b 1 (finsetCoordProj B0 x))))
(Measure.pi μ))
(hflpProd : MemLp (shiftedThreeBlockProduct B0 B f a) 2 (Measure.pi μ))
(hglpProd : MemLp (shiftedThreeBlockProduct B0 B g b) 2 (Measure.pi μ)) :
(fun x =>
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ)
(fun y => shiftedThreeBlockProduct B0 B f a y *
shiftedThreeBlockProduct B0 B g b y) x -
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (shiftedThreeBlockProduct B0 B f a) x *
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (shiftedThreeBlockProduct B0 B g b) x) =ᵐ[Measure.pi μ]
(fun x =>
(∏ t : Fin 3,
(covariance
(fun y : ∀ i, Ω i => f t (finsetCoordProj (B t) y))
(fun y : ∀ i, Ω i => g t (finsetCoordProj (B t) y))
(Measure.pi μ) +
((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) -
a t (finsetCoordProj B0 x)) *
((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) -
b t (finsetCoordProj B0 x)))) -
(∏ t : Fin 3,
((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) -
a t (finsetCoordProj B0 x))) *
(∏ t : Fin 3,
((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) -
b t (finsetCoordProj B0 x)))) := by
have hcross := condExp_shiftedThreeBlockCross μ B0 B htrain heval f g a b
hfmeas hgmeas hameas hbmeas hf hg ha hb hfg hflp hglp hcross01
hflpProd hglpProd
have hleft := condExp_shiftedThreeBlockProduct μ B0 B htrain heval f a
hfmeas hameas hf ha hf01 (hflpProd.integrable (by norm_num))
have hright := condExp_shiftedThreeBlockProduct μ B0 B htrain heval g b
hgmeas hbmeas hg hb hg01 (hglpProd.integrable (by norm_num))
filter_upwards [hcross, hleft, hright] with x hx hy hz
simp only [hx, hy, hz]
2 supporting declarations (lemmas, instances)
-
condExp_shiftedThreeBlockProducttheorem — A finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness and pairwise evaluation disjointness, held-out scores and training shifts with measurability and integrability, an integrable first shifted pair, and an integrable shifted three-block product imply that its conditional mean is the product of held-out means minus the corresponding training shifts.hypothesesι :sharedType u_1ι → Type u_2μ :(i : ι) → Measure (Ω i)∀ i, IsProbabilityMeasure (μ i)B0 :Finset ιhtrain :∀ t, Disjoint B0 (B t)f :(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝa :(t : Fin 3) → ((i : {i // i ∈ B0}) → Ω i.val) → ℝhfmeas :∀ t, Measurable (f t)hameas :∀ t, Measurable (a t)hf :∀ t, Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x)) (Measure.pi μ)ha :∀ t, Integrable (fun x : ∀ i, Ω i => a t (finsetCoordProj B0 x)) (Measure.pi μ)hshift01 :Integrable (fun x : ∀ i, Ω i => (f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) * (f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x))) (Measure.pi μ)hshiftprod :Integrable (shiftedThreeBlockProduct B0 B f a) (Measure.pi μ)conclusioncondExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (shiftedThreeBlockProduct B0 B f a)=ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)))Proof (Lean source)
theorem condExp_shiftedThreeBlockProduct (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] (B0 : Finset ι) (B : Fin 3 → Finset ι) (htrain : ∀ t, Disjoint B0 (B t)) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) (f : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ) (a : (t : Fin 3) → ((i : {i // i ∈ B0}) → Ω i.val) → ℝ) (hfmeas : ∀ t, Measurable (f t)) (hameas : ∀ t, Measurable (a t)) (hf : ∀ t, Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x)) (Measure.pi μ)) (ha : ∀ t, Integrable (fun x : ∀ i, Ω i => a t (finsetCoordProj B0 x)) (Measure.pi μ)) (hshift01 : Integrable (fun x : ∀ i, Ω i => (f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) * (f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x))) (Measure.pi μ)) (hshiftprod : Integrable (shiftedThreeBlockProduct B0 B f a) (Measure.pi μ)) : condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (shiftedThreeBlockProduct B0 B f a) =ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x))) := by classical let η : (t : Fin 3) → ((i : {i // i ∈ B0 ∪ B t}) → Ω i.val) → ℝ := fun t => shiftedJoinedScore B0 (B t) (f t) (a t) have hηmeas : ∀ t, Measurable (η t) := by intro t exact measurable_shiftedJoinedScore B0 (B t) (f t) (a t) (hfmeas t) (hameas t) have hη : ∀ t, Integrable (fun x : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) x)) (Measure.pi μ) := by intro t change Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) - a t (finsetCoordProj B0 x)) (Measure.pi μ) exact (hf t).sub (ha t) have hη01 : Integrable (fun x : ∀ i, Ω i => η 0 (finsetCoordProj (B0 ∪ B 0) x) * η 1 (finsetCoordProj (B0 ∪ B 1) x)) (Measure.pi μ) := by simpa only [η, shiftedJoinedScore_comp_proj] using hshift01 have hfun : joinedBlockProduct B0 B η = shiftedThreeBlockProduct B0 B f a := by funext x simp only [joinedBlockProduct, shiftedThreeBlockProduct, η, shiftedJoinedScore_comp_proj] have hηprod : Integrable (joinedBlockProduct B0 B η) (Measure.pi μ) := by simpa only [hfun] using hshiftprod have hfactor := condExp_joinedBlockProduct_of_integrable μ B0 B htrain heval η hηmeas hη hη01 hηprod have hmean : ∀ t, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) y)) =ᵐ[Measure.pi μ] (fun x => (∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)) := by intro t simpa only [η, shiftedJoinedScore_comp_proj] using (condExp_shiftedBlock_eq_integral_sub μ B0 (B t) (htrain t) (f t) (a t) (hfmeas t) (hameas t) (hf t) (ha t)) have hprod : (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) y)) x) =ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x))) := by filter_upwards [hmean 0, hmean 1, hmean 2] with x h0 h1 h2 simp only [Fin.prod_univ_three, h0, h1, h2] rw [← hfun] exact hfactor.trans hprod -
condExp_shiftedThreeBlockCrosstheorem — A finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness and pairwise evaluation disjointness, two held-out-score families, two training-shift families, measurability, integrability of all base scores and shifts, integrable local cross products, square-integrable shifted scores, an integrable first shifted cross pair, and square-integrable shifted three-block products imply that the conditional cross moment factors into the three shifted blockwise cross moments.hypothesesι :sharedType u_1ι → Type u_2μ :(i : ι) → Measure (Ω i)∀ i, IsProbabilityMeasure (μ i)B0 :Finset ιhtrain :∀ t, Disjoint B0 (B t)f g :(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝa b :(t : Fin 3) → ((i : {i // i ∈ B0}) → Ω i.val) → ℝhfmeas :∀ t, Measurable (f t)hgmeas :∀ t, Measurable (g t)hameas :∀ t, Measurable (a t)hbmeas :∀ t, Measurable (b t)hf :∀ t, Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x)) (Measure.pi μ)hg :∀ t, Integrable (fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x)) (Measure.pi μ)ha :∀ t, Integrable (fun x : ∀ i, Ω i => a t (finsetCoordProj B0 x)) (Measure.pi μ)hb :∀ t, Integrable (fun x : ∀ i, Ω i => b t (finsetCoordProj B0 x)) (Measure.pi μ)hfg :∀ t,Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) * g t (finsetCoordProj (B t) x)) (Measure.pi μ)hflp :∀ t,MemLp (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) - a t (finsetCoordProj B0 x)) 2 (Measure.pi μ)hglp :∀ t,MemLp (fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x) - b t (finsetCoordProj B0 x)) 2 (Measure.pi μ)hcross01 :Integrable (fun x : ∀ i, Ω i => ((f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) * (g 0 (finsetCoordProj (B 0) x) - b 0 (finsetCoordProj B0 x))) * ((f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x)) * (g 1 (finsetCoordProj (B 1) x) - b 1 (finsetCoordProj B0 x)))) (Measure.pi μ)hflpProd :MemLp (shiftedThreeBlockProduct B0 B f a) 2 (Measure.pi μ)hglpProd :MemLp (shiftedThreeBlockProduct B0 B g b) 2 (Measure.pi μ)conclusioncondExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x => shiftedThreeBlockProduct B0 B f a x * shiftedThreeBlockProduct B0 B g b x)=ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, (covariance (fun y : ∀ i, Ω i => f t (finsetCoordProj (B t) y)) (fun y : ∀ i, Ω i => g t (finsetCoordProj (B t) y)) (Measure.pi μ) + ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)) * ((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) - b t (finsetCoordProj B0 x))))Proof (Lean source)
theorem condExp_shiftedThreeBlockCross (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] (B0 : Finset ι) (B : Fin 3 → Finset ι) (htrain : ∀ t, Disjoint B0 (B t)) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) (f g : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ) (a b : (t : Fin 3) → ((i : {i // i ∈ B0}) → Ω i.val) → ℝ) (hfmeas : ∀ t, Measurable (f t)) (hgmeas : ∀ t, Measurable (g t)) (hameas : ∀ t, Measurable (a t)) (hbmeas : ∀ t, Measurable (b t)) (hf : ∀ t, Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x)) (Measure.pi μ)) (hg : ∀ t, Integrable (fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x)) (Measure.pi μ)) (ha : ∀ t, Integrable (fun x : ∀ i, Ω i => a t (finsetCoordProj B0 x)) (Measure.pi μ)) (hb : ∀ t, Integrable (fun x : ∀ i, Ω i => b t (finsetCoordProj B0 x)) (Measure.pi μ)) (hfg : ∀ t, Integrable (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) * g t (finsetCoordProj (B t) x)) (Measure.pi μ)) (hflp : ∀ t, MemLp (fun x : ∀ i, Ω i => f t (finsetCoordProj (B t) x) - a t (finsetCoordProj B0 x)) 2 (Measure.pi μ)) (hglp : ∀ t, MemLp (fun x : ∀ i, Ω i => g t (finsetCoordProj (B t) x) - b t (finsetCoordProj B0 x)) 2 (Measure.pi μ)) (hcross01 : Integrable (fun x : ∀ i, Ω i => ((f 0 (finsetCoordProj (B 0) x) - a 0 (finsetCoordProj B0 x)) * (g 0 (finsetCoordProj (B 0) x) - b 0 (finsetCoordProj B0 x))) * ((f 1 (finsetCoordProj (B 1) x) - a 1 (finsetCoordProj B0 x)) * (g 1 (finsetCoordProj (B 1) x) - b 1 (finsetCoordProj B0 x)))) (Measure.pi μ)) (hflpProd : MemLp (shiftedThreeBlockProduct B0 B f a) 2 (Measure.pi μ)) (hglpProd : MemLp (shiftedThreeBlockProduct B0 B g b) 2 (Measure.pi μ)) : condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x => shiftedThreeBlockProduct B0 B f a x * shiftedThreeBlockProduct B0 B g b x) =ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, (covariance (fun y : ∀ i, Ω i => f t (finsetCoordProj (B t) y)) (fun y : ∀ i, Ω i => g t (finsetCoordProj (B t) y)) (Measure.pi μ) + ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)) * ((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) - b t (finsetCoordProj B0 x)))) := by classical let η : (t : Fin 3) → ((i : {i // i ∈ B0 ∪ B t}) → Ω i.val) → ℝ := fun t y => shiftedJoinedScore B0 (B t) (f t) (a t) y * shiftedJoinedScore B0 (B t) (g t) (b t) y have hηmeas : ∀ t, Measurable (η t) := by intro t exact (measurable_shiftedJoinedScore B0 (B t) (f t) (a t) (hfmeas t) (hameas t)).mul (measurable_shiftedJoinedScore B0 (B t) (g t) (b t) (hgmeas t) (hbmeas t)) have hη : ∀ t, Integrable (fun x : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) x)) (Measure.pi μ) := by intro t change Integrable (fun x : ∀ i, Ω i => (f t (finsetCoordProj (B t) x) - a t (finsetCoordProj B0 x)) * (g t (finsetCoordProj (B t) x) - b t (finsetCoordProj B0 x))) (Measure.pi μ) exact (hflp t).integrable_mul (hglp t) have hη01 : Integrable (fun x : ∀ i, Ω i => η 0 (finsetCoordProj (B0 ∪ B 0) x) * η 1 (finsetCoordProj (B0 ∪ B 1) x)) (Measure.pi μ) := by simpa only [η, shiftedJoinedScore_comp_proj] using hcross01 have hfun : joinedBlockProduct B0 B η = (fun x => shiftedThreeBlockProduct B0 B f a x * shiftedThreeBlockProduct B0 B g b x) := by funext x simp only [joinedBlockProduct, shiftedThreeBlockProduct, η, shiftedJoinedScore_comp_proj, Fin.prod_univ_three] ring have hηprod : Integrable (joinedBlockProduct B0 B η) (Measure.pi μ) := by rw [hfun] exact hflpProd.integrable_mul hglpProd have hfactor := condExp_joinedBlockProduct_of_integrable μ B0 B htrain heval η hηmeas hη hη01 hηprod have hmean : ∀ t, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) y)) =ᵐ[Measure.pi μ] (fun x => covariance (fun y : ∀ i, Ω i => f t (finsetCoordProj (B t) y)) (fun y : ∀ i, Ω i => g t (finsetCoordProj (B t) y)) (Measure.pi μ) + ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)) * ((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) - b t (finsetCoordProj B0 x))) := by intro t simpa only [η, shiftedJoinedScore_comp_proj] using (condExp_shiftedBlockCross_eq_covariance_add μ B0 (B t) (htrain t) (f t) (g t) (a t) (b t) (hfmeas t) (hgmeas t) (hameas t) (hbmeas t) (hf t) (hg t) (ha t) (hb t) (hfg t) (hflp t) (hglp t)) have hprod : (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) y)) x) =ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, (covariance (fun y : ∀ i, Ω i => f t (finsetCoordProj (B t) y)) (fun y : ∀ i, Ω i => g t (finsetCoordProj (B t) y)) (Measure.pi μ) + ((∫ y : (∀ i, Ω i), f t (finsetCoordProj (B t) y) ∂Measure.pi μ) - a t (finsetCoordProj B0 x)) * ((∫ y : (∀ i, Ω i), g t (finsetCoordProj (B t) y) ∂Measure.pi μ) - b t (finsetCoordProj B0 x)))) := by filter_upwards [hmean 0, hmean 1, hmean 2] with x h0 h1 h2 simp only [Fin.prod_univ_three, h0, h1, h2] rw [← hfun] exact hfactor.trans hprod
FourCoordinate 1 core · 0 supporting The training coordinate is coordinate zero, and the three held-out scores use coordinates one, two, and three. ★ condExp_shiftedFourCoordinateProduct
Four-coordinate shifted product moment
The training coordinate is coordinate zero, and the three held-out scores use coordinates one, two, and three. This is a direct generic specialization of the block formulation.
theorem condExp_shiftedFourCoordinateProduct reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.ThreeBlockShiftedProduct
A four-coordinate product probability law, three held-out coordinate scores and three coordinate-zero shifts with measurability and integrability, an integrable first shifted pair, and an integrable shifted three-factor product imply that the conditional mean given coordinate zero of the product of the three shifted scores is almost surely the product, over the three held-out coordinates, of the unconditional mean of the score minus its coordinate-zero shift.
Formal statement
hypotheses
X :
ν :
∀ i, IsProbabilityMeasure (ν i)
f :
(t : Fin 3) → X t.succ → ℝ
a :
(t : Fin 3) → X 0 → ℝ
hfmeas :
∀ t, Measurable (f t)
hameas :
∀ t, Measurable (a t)
hf :
∀ t, Integrable (fun x : ∀ i, X i => f t (x t.succ)) (Measure.pi ν)
ha :
∀ t, Integrable (fun x : ∀ i, X i => a t (x 0)) (Measure.pi ν)
hshift01 :
Integrable (fun x : ∀ i, X i => (f 0 (x 1) - a 0 (x 0)) * (f 1 (x 2) - a 1 (x 0))) (Measure.pi ν)
hshiftprod :
Integrable (fun x : ∀ i, X i => ∏ t : Fin 3, (f t (x t.succ) - a t (x 0))) (Measure.pi ν)
conclusion
condExp (comap (finsetCoordProj (Ω := X) ({0} : Finset (Fin 4))) inferInstance) (Measure.pi ν) (fun x : ∀ i, X i => ∏ t : Fin 3, (f t (x t.succ) - a t (x 0)))
=ᵐ[Measure.pi ν] (fun x => ∏ t : Fin 3, ((∫ y : (∀ i, X i), f t (y t.succ) ∂Measure.pi ν) - a t (x 0)))
Proof (Lean source)
theorem condExp_shiftedFourCoordinateProduct
{X : Fin 4 → Type*} [∀ i, MeasurableSpace (X i)]
[∀ i, StandardBorelSpace (X i)]
(ν : (i : Fin 4) → Measure (X i)) [∀ i, IsProbabilityMeasure (ν i)]
(f : (t : Fin 3) → X t.succ → ℝ) (a : (t : Fin 3) → X 0 → ℝ)
(hfmeas : ∀ t, Measurable (f t)) (hameas : ∀ t, Measurable (a t))
(hf : ∀ t, Integrable (fun x : ∀ i, X i => f t (x t.succ)) (Measure.pi ν))
(ha : ∀ t, Integrable (fun x : ∀ i, X i => a t (x 0)) (Measure.pi ν))
(hshift01 : Integrable (fun x : ∀ i, X i =>
(f 0 (x 1) - a 0 (x 0)) * (f 1 (x 2) - a 1 (x 0))) (Measure.pi ν))
(hshiftprod : Integrable (fun x : ∀ i, X i =>
∏ t : Fin 3, (f t (x t.succ) - a t (x 0))) (Measure.pi ν)) :
condExp (comap
(finsetCoordProj (Ω := X) ({0} : Finset (Fin 4))) inferInstance)
(Measure.pi ν)
(fun x : ∀ i, X i => ∏ t : Fin 3, (f t (x t.succ) - a t (x 0)))
=ᵐ[Measure.pi ν]
(fun x => ∏ t : Fin 3,
((∫ y : (∀ i, X i), f t (y t.succ) ∂Measure.pi ν) - a t (x 0))) := by
classical
let B : Fin 3 → Finset (Fin 4) := fun t => {t.succ}
have htrain : ∀ t, Disjoint ({0} : Finset (Fin 4)) (B t) := by
intro t
simpa [B] using (Fin.succ_ne_zero t).symm
have heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)) := by
intro s t hst
simpa [B] using (Fin.succ_injective 3).ne hst
let f' : (t : Fin 3) → ((i : {i // i ∈ B t}) → X i.val) → ℝ :=
fun t z => f t (z ⟨t.succ, Finset.mem_singleton_self _⟩)
let a' : (t : Fin 3) → ((i : {i // i ∈ ({0} : Finset (Fin 4))}) → X i.val) → ℝ :=
fun t z => a t (z ⟨0, Finset.mem_singleton_self _⟩)
have hf'meas (t : Fin 3) : Measurable (f' t) :=
(hfmeas t).comp (measurable_pi_apply
(⟨t.succ, Finset.mem_singleton_self _⟩ : {i // i ∈ B t}))
have ha'meas (t : Fin 3) : Measurable (a' t) :=
(hameas t).comp (measurable_pi_apply
(⟨0, Finset.mem_singleton_self _⟩ : {i // i ∈ ({0} : Finset (Fin 4))}))
have hf' (t : Fin 3) : Integrable
(fun x : ∀ i, X i => f' t (finsetCoordProj (B t) x)) (Measure.pi ν) := by
exact hf t
have ha' (t : Fin 3) : Integrable
(fun x : ∀ i, X i => a' t (finsetCoordProj ({0} : Finset (Fin 4)) x))
(Measure.pi ν) := by
exact ha t
have hshift01' : Integrable (fun x : ∀ i, X i =>
(f' 0 (finsetCoordProj (B 0) x) -
a' 0 (finsetCoordProj ({0} : Finset (Fin 4)) x)) *
(f' 1 (finsetCoordProj (B 1) x) -
a' 1 (finsetCoordProj ({0} : Finset (Fin 4)) x)))
(Measure.pi ν) := by
exact hshift01
have hshiftprod' : Integrable
(shiftedThreeBlockProduct ({0} : Finset (Fin 4)) B f' a')
(Measure.pi ν) := by
exact hshiftprod
have h := condExp_shiftedThreeBlockProduct ν ({0} : Finset (Fin 4)) B
htrain heval f' a' hf'meas ha'meas hf' ha' hshift01' hshiftprod'
have hfun : shiftedThreeBlockProduct ({0} : Finset (Fin 4)) B f' a' =
(fun x : ∀ i, X i => ∏ t : Fin 3, (f t (x t.succ) - a t (x 0))) := rfl
rw [hfun] at h
simpa only [finsetCoordProj, f', a', B] using h