InformationTheory.Shannon.EPI.ScoreCrossTermOrth

Imports 5

Score cross-term orthogonality (toward Blachman / Stam) #

E[s_X(X) · s_Y(Y)] = 0 for independent X, Y with mean-zero scores. Independence factors the expectation (IndepFun.integral_fun_mul_eq_mul_integral), and the mean-zero score factor kills the product; the mean-zero input itself comes from FisherInfo.integral_logDeriv_density_eq_zero.

This is the cross-term a Blachman-style score expansion consumes; the score-of-convolution identity s_Z = E[s_X | σ(X+Y)] itself is not proved here.

theorem

InformationTheory.Shannon.EPIScoreCrossTermOrth.score_cross_term_eq_zero

source

{Ω : Type u_1} [MeasurableSpace Ω] {X Y : Ω → ℝ} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {sX sY : ℝ → ℝ} (hXY : ProbabilityTheory.IndepFun X Y P) (hsXmeas : Measurable sX) (hsYmeas : Measurable sY) (hsX : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => sX (X ω)) P) (hsY : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => sY (Y ω)) P) (hmeanX : ∫ (ω : Ω), sX (X ω) ∂P = 0) :

∫ (ω : Ω), sX (X ω) * sY (Y ω) ∂P = 0

Score cross-term orthogonality (full-expectation version). For independent X, Y whose score functions sX, sY have zero mean (here only sX needs mean zero), the cross-term ∫ sX(X ω) · sY(Y ω) dP = 0. Built from IndepFun.comp + IndepFun.integral_fun_mul_eq_mul_integral + the mean-zero hypothesis hmeanX. This is not the Blachman score-of-convolution identity.

hsXmeas / hsYmeas are Measurable sX / Measurable sY regularity preconditions (needed for IndepFun.comp), not load-bearing. hmeanX constrains the input score's mean (E[sX∘X] = 0), which is distinct from the conclusion E[sX·sY] = 0. @audit:ok

Used by