StatisticalRefinement.lean

1 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
2 
3 /-! P11: finer information improves the ideal squared-error predictor.
4 
5 The predictors below are actual conditional expectations. Orthogonality is
6 derived from the conditional-expectation projection, rather than supplied as
7 an extra hypothesis. The result holds in every complete real Hilbert space,
8 so in particular in the manuscript's finite-dimensional setting.
9 -/
10 set_option autoImplicit false
11 
12 open MeasureTheory
13 open scoped ENNReal MeasureTheory
14 
15 namespace Komorebi.LSM.StatisticalRefinement
16 
17 variable {Ω E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
18   {m₀ : MeasurableSpace Ω} {μ : Measure Ω}
19 
20 /-- Expected squared error between two square-integrable random variables. -/
21 noncomputable def squaredRisk (Y Z : Lp E 2 μ) : ℝ :=
22   ∫ ω, ‖Y ω - Z ω‖ ^ 2 ∂μ
23 
24 theorem integral_sq_norm (Y : Lp E 2 μ) :
25     (∫ ω, ‖Y ω‖ ^ 2 ∂μ) = ‖Y‖ ^ 2 := by
26   rw [← real_inner_self_eq_norm_sq Y, L2.inner_def]
27   simp_rw [real_inner_self_eq_norm_sq]
28 
29 theorem squaredRisk_eq_norm_sq (Y Z : Lp E 2 μ) :
30     squaredRisk Y Z = ‖Y - Z‖ ^ 2 := by
31   rw [← integral_sq_norm (Y - Z)]
32   apply integral_congr_ae
33   filter_upwards [Lp.coeFn_sub Y Z] with ω hω
34   exact congrArg (fun x : E => ‖x‖ ^ 2) hω.symm
35 
36 variable [CompleteSpace E]
37 
38 /-- Conditional-expectation residuals are orthogonal to every observable in
39 the conditioning information set. -/
40 theorem residual_orthogonal {m : MeasurableSpace Ω} (hm : m ≤ m₀)
41     (Y Z : Lp E 2 μ) (hZ : AEStronglyMeasurable[m] Z μ) :
42     inner ℝ (Y - (condExpL2 E ℝ hm Y : Lp E 2 μ)) Z = 0 := by
43   rw [inner_sub_left, inner_condExpL2_eq_inner_fun hm Y Z hZ, sub_self]
44 
45 /-- P11 in L2, with both predictors constructed by conditional expectation. -/
46 theorem conditional_expectation_pythagoras {mF mG : MeasurableSpace Ω}
47     (hF : mF ≤ m₀) (hG : mG ≤ m₀) (hFG : mF ≤ mG) (Y : Lp E 2 μ) :
48     squaredRisk Y (condExpL2 E ℝ hF Y : Lp E 2 μ) =
49       squaredRisk Y (condExpL2 E ℝ hG Y : Lp E 2 μ) +
50       squaredRisk (condExpL2 E ℝ hG Y : Lp E 2 μ)
51         (condExpL2 E ℝ hF Y : Lp E 2 μ) := by
52   let F : Lp E 2 μ := condExpL2 E ℝ hF Y
53   let G : Lp E 2 μ := condExpL2 E ℝ hG Y
54   have hFmeas : AEStronglyMeasurable[mG] F μ :=
55     (aestronglyMeasurable_condExpL2 hF Y).mono hFG
56   have hGmeas : AEStronglyMeasurable[mG] G μ :=
57     aestronglyMeasurable_condExpL2 hG Y
58   have hdiff : AEStronglyMeasurable[mG] (G - F) μ :=
59     (hGmeas.sub hFmeas).congr (Lp.coeFn_sub G F).symm
60   have horth : inner ℝ (Y - G) (G - F) = 0 :=
61     residual_orthogonal hG Y (G - F) hdiff
62   have hsplit : Y - F = (Y - G) + (G - F) := by abel
63   simp only [squaredRisk_eq_norm_sq]
64   change ‖Y - F‖ ^ 2 = ‖Y - G‖ ^ 2 + ‖G - F‖ ^ 2
65   rw [hsplit]
66   simpa only [pow_two] using
67     norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ horth
68 
69 /-- A finer sigma algebra cannot increase the ideal squared prediction risk. -/
70 theorem conditional_expectation_risk_mono {mF mG : MeasurableSpace Ω}
71     (hF : mF ≤ m₀) (hG : mG ≤ m₀) (hFG : mF ≤ mG) (Y : Lp E 2 μ) :
72     squaredRisk Y (condExpL2 E ℝ hG Y : Lp E 2 μ) ≤
73       squaredRisk Y (condExpL2 E ℝ hF Y : Lp E 2 μ) := by
74   rw [conditional_expectation_pythagoras hF hG hFG Y]
75   exact le_add_of_nonneg_right (by rw [squaredRisk_eq_norm_sq]; positivity)
76 
77 section FunctionRepresentatives
78 
79 variable [IsFiniteMeasure μ]
80 
81 /-- The L2 risk is the ordinary integral against the actual conditional
82 expectation of any square-integrable representative. -/
83 theorem squaredRisk_toLp_condExp {m : MeasurableSpace Ω} (hm : m ≤ m₀)
84     {Y : Ω → E} (hY : MemLp Y 2 μ) :
85     squaredRisk hY.toLp (condExpL2 E ℝ hm hY.toLp : Lp E 2 μ) =
86       ∫ ω, ‖Y ω - μ[Y | m] ω‖ ^ 2 ∂μ := by
87   unfold squaredRisk
88   apply integral_congr_ae
89   filter_upwards [hY.coeFn_toLp,
90     hY.condExpL2_ae_eq_condExp (𝕜 := ℝ) hm] with ω hω hcond
91   rw [hω, hcond]
92 
93 theorem squaredRisk_condExp_difference {mF mG : MeasurableSpace Ω}
94     (hF : mF ≤ m₀) (hG : mG ≤ m₀) {Y : Ω → E} (hY : MemLp Y 2 μ) :
95     squaredRisk (condExpL2 E ℝ hG hY.toLp : Lp E 2 μ)
96       (condExpL2 E ℝ hF hY.toLp : Lp E 2 μ) =
97       ∫ ω, ‖μ[Y | mG] ω - μ[Y | mF] ω‖ ^ 2 ∂μ := by
98   unfold squaredRisk
99   apply integral_congr_ae
100   filter_upwards [hY.condExpL2_ae_eq_condExp (𝕜 := ℝ) hF,
101     hY.condExpL2_ae_eq_condExp (𝕜 := ℝ) hG] with ω hcondF hcondG
102   rw [hcondF, hcondG]
103 
104 /-- P11 exactly as an expected-squared-error identity for a
105 square-integrable Hilbert-valued random variable and nested information.
106 Probability measures are included among these finite measures. -/
107 theorem ideal_statistical_benefit {mF mG : MeasurableSpace Ω}
108     (hF : mF ≤ m₀) (hG : mG ≤ m₀) (hFG : mF ≤ mG)
109     {Y : Ω → E} (hY : MemLp Y 2 μ) :
110     (∫ ω, ‖Y ω - μ[Y | mF] ω‖ ^ 2 ∂μ) =
111       (∫ ω, ‖Y ω - μ[Y | mG] ω‖ ^ 2 ∂μ) +
112       (∫ ω, ‖μ[Y | mG] ω - μ[Y | mF] ω‖ ^ 2 ∂μ) := by
113   rw [← squaredRisk_toLp_condExp hF hY,
114     ← squaredRisk_toLp_condExp hG hY, ← squaredRisk_condExp_difference hF hG hY]
115   exact conditional_expectation_pythagoras hF hG hFG hY.toLp
116 
117 theorem ideal_statistical_risk_mono {mF mG : MeasurableSpace Ω}
118     (hF : mF ≤ m₀) (hG : mG ≤ m₀) (hFG : mF ≤ mG)
119     {Y : Ω → E} (hY : MemLp Y 2 μ) :
120     (∫ ω, ‖Y ω - μ[Y | mG] ω‖ ^ 2 ∂μ) ≤
121       ∫ ω, ‖Y ω - μ[Y | mF] ω‖ ^ 2 ∂μ := by
122   rw [ideal_statistical_benefit hF hG hFG hY]
123   exact le_add_of_nonneg_right (integral_nonneg fun ω => sq_nonneg _)
124 
125 /-- The manuscript's finite second-moment hypothesis, expressed as
126 integrability of the nonnegative squared norm, implies the same identity. -/
127 theorem ideal_statistical_benefit_of_integrable_sq_norm
128     {mF mG : MeasurableSpace Ω} (hF : mF ≤ m₀) (hG : mG ≤ m₀)
129     (hFG : mF ≤ mG) {Y : Ω → E} (hYmeas : AEStronglyMeasurable[m₀] Y μ)
130     (hYsq : Integrable (fun ω => ‖Y ω‖ ^ 2) μ) :
131     (∫ ω, ‖Y ω - μ[Y | mF] ω‖ ^ 2 ∂μ) =
132       (∫ ω, ‖Y ω - μ[Y | mG] ω‖ ^ 2 ∂μ) +
133       (∫ ω, ‖μ[Y | mG] ω - μ[Y | mF] ω‖ ^ 2 ∂μ) :=
134   ideal_statistical_benefit hF hG hFG
135     ((memLp_two_iff_integrable_sq_norm hYmeas).mpr hYsq)
136 
137 end FunctionRepresentatives
138 
139 end Komorebi.LSM.StatisticalRefinement

Back to source controls