RegressionConfidence.lean

1 import KomorebiLSM.RegressionGaussian
2 import KomorebiLSM.RegressionRadius
3 import KomorebiLSM.RegressionExponential
4 import KomorebiLSM.VilleInequality
5 
6 /-! P81: the actual ridge estimator is covered at every finite time by a
7 measurable event derived from the actual Gaussian-mixture supermartingale. -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM.RegressionConfidence
10 open MeasureTheory ProbabilityTheory Matrix
11 open scoped BigOperators ENNReal ComplexOrder
12 variable {I Ω : Type*} [Fintype I] [DecidableEq I] [mΩ : MeasurableSpace Ω]
13 variable {μ : Measure Ω} [IsProbabilityMeasure μ]
14 
15 /-- The noise is the literal deviation from the declared linear conditional mean. -/
16 noncomputable def regressionNoise (θ : I → ℝ) (φ : ℕ → Ω → I → ℝ)
17     (y : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ := y n ω-θ ⬝ᵥ φ n ω
18 
19 /-- The explicit measurable event used for the time-uniform confidence guarantee. -/
20 noncomputable def regressionGood (γ σ δ : ℝ) (φ : ℕ → Ω → I → ℝ)
21     (y : ℕ → Ω → ℝ) (θ : I → ℝ) : Set Ω :=
22   (VilleInequality.crossing
23     (exponentialMixture σ φ (regressionNoise θ φ y) (gaussianPrior γ)) (1/δ))ᶜ
24 
25 omit [DecidableEq I] [IsProbabilityMeasure μ] in
26 theorem regressionNoise_measurable (ℱ : Filtration ℕ mΩ)
27     (θ : I → ℝ) (φ : ℕ → Ω → I → ℝ) (y : ℕ → Ω → ℝ)
28     (hφ : ∀ n i,Measurable[ℱ n] (fun ω => φ n ω i))
29     (hy : ∀ n,Measurable[ℱ (n+1)] (y n)) (n : ℕ) :
30     Measurable[ℱ (n+1)] (regressionNoise θ φ y n) := by
31   unfold regressionNoise dotProduct
32   exact (hy n).sub (Finset.measurable_sum _ (fun i _ => measurable_const.mul
33     ((hφ n i).mono (ℱ.mono (by omega)) le_rfl)))
34 
35 omit mΩ [IsProbabilityMeasure μ] in
36 /-- Every sample in the explicit good event has the source's exact ridge
37 confidence radius at every finite horizon. -/
38 theorem regressionGood_error_bound (γ σ δ S : ℝ) (hγ : 0 < γ) (hσ : 0 < σ)
39     (hδ : 0 < δ) (φ : ℕ → Ω → I → ℝ) (y : ℕ → Ω → ℝ) (θ : I → ℝ)
40     (hθ : euclideanNorm θ ≤ S) (ω : Ω) (hgood : ω∈regressionGood γ σ δ φ y θ) (n : ℕ) :
41     weightedNorm (ridgeMatrix γ (fun i => φ i ω) n)
42       (ridgeEstimate γ (fun i => φ i ω) (fun i => y i ω) n-θ) ≤
43       noiseRadius γ σ δ (fun i => φ i ω) n+Real.sqrt γ*S := by
44   have hn : exponentialMixture σ φ (regressionNoise θ φ y) (gaussianPrior γ) n ω<1/δ := by
45     apply lt_of_not_ge
46     intro hc
47     exact hgood ⟨n,hc⟩
48   rw [exponentialMixture_eq σ φ (regressionNoise θ φ y) (ne_of_gt hσ),
49     gaussian_ridge_mixture γ σ hγ hσ] at hn
50   have hV := ridgeMatrix_posDef γ hγ (fun i => φ i ω) n
51   have hW : (γ • (1 : Matrix I I ℝ)).PosDef := Matrix.PosDef.one.smul hγ
52   have hnoise := mixture_lt_implies_noise_bound _ _ hV hW σ δ hσ hδ _ hn
53   apply (ridge_error_le γ hγ (fun i => φ i ω) (fun i => y i ω)
54     (fun i => regressionNoise θ φ y i ω) θ n (fun i _ => by
55       unfold regressionNoise
56       ring)).trans
57   exact add_le_add hnoise (mul_le_mul_of_nonneg_left hθ (Real.sqrt_nonneg γ))
58 
59 /-- Full P81. No design boundedness or excitation condition is added. The
60 noise hypothesis is the actual conditional exponential inequality, and the
61 mixture, its probability normalization and its crossing control are derived. -/
62 theorem regression_confidence_certificate (ℱ : Filtration ℕ mΩ)
63     (γ σ δ S : ℝ) (hγ : 0 < γ) (hσ : 0 < σ) (hδ : 0 < δ)
64     (φ : ℕ → Ω → I → ℝ) (y : ℕ → Ω → ℝ) (θ : I → ℝ)
65     (hφ : ∀ n i,Measurable[ℱ n] (fun ω => φ n ω i))
66     (hy : ∀ n,Measurable[ℱ (n+1)] (y n)) (hθ : euclideanNorm θ ≤ S)
67     (H : ∀ n,ConditionalSubgaussian (ℱ.le n) (regressionNoise θ φ y n) σ μ) :
68     MeasurableSet (regressionGood γ σ δ φ y θ) ∧
69     1-δ≤μ.real (regressionGood γ σ δ φ y θ) ∧
70     ∀ ω∈regressionGood γ σ δ φ y θ,∀ n,
71       weightedNorm (ridgeMatrix γ (fun i => φ i ω) n)
72         (ridgeEstimate γ (fun i => φ i ω) (fun i => y i ω) n-θ) ≤
73         noiseRadius γ σ δ (fun i => φ i ω) n+Real.sqrt γ*S := by
74   let : IsProbabilityMeasure (gaussianPrior (I := I) γ) := gaussianPrior_probability γ hγ
75   let M := exponentialMixture σ φ (regressionNoise θ φ y) (gaussianPrior γ)
76   have hM : Supermartingale M ℱ μ := exponentialMixture_supermartingale ℱ σ φ
77     (regressionNoise θ φ y) hφ (regressionNoise_measurable ℱ θ φ y hφ hy) H (gaussianPrior γ)
78   have hm := VilleInequality.crossing_measurable μ ℱ M hM (1/δ)
79   have hi : (∫ ω,M 0 ω∂μ)≤1 := by simp [M]
80   have hb := VilleInequality.crossing_bound μ ℱ M hM
81     (exponentialMixture_nonneg σ φ (regressionNoise θ φ y) (gaussianPrior γ)) hi (1/δ)
82       (one_div_pos.2 hδ)
83   simp only [one_div_one_div] at hb
84   have hbr : μ.real (VilleInequality.crossing M (1/δ))≤δ := by
85     have h := ENNReal.toReal_mono ENNReal.ofReal_ne_top hb
86     simpa only [Measure.real,ENNReal.toReal_ofReal hδ.le] using h
87   refine ⟨hm.compl,?_,?_⟩
88   · change 1-δ≤μ.real ((VilleInequality.crossing M (1/δ))ᶜ)
89     rw [measureReal_compl hm]
90     simpa using sub_le_sub_left hbr 1
91   · exact fun ω hω n => regressionGood_error_bound γ σ δ S hγ hσ hδ φ y θ hθ ω hω n
92 
93 end Komorebi.LSM.RegressionConfidence

Back to source controls