RationalRegressionConfidence.lean

1 import KomorebiLSM.ScalarRegressionConfidence
2 import KomorebiLSM.BoundedResponseNoise
3 import KomorebiLSM.OutwardConfidenceIntervals
4 
5 /-! P84: actual scalar regression events are retained through exact outer
6 radius construction, outward endpoint rounding and intersection with the prior. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.RationalRegressionConfidence
9 open MeasureTheory RegressionConfidence
10 open OutwardConfidenceIntervals
11 open scoped BigOperators
12 variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
13 
14 noncomputable def variance (x : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
15   scalarV (fun i => x i ω) n
16 noncomputable def estimate (x y : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
17   scalarEstimate (fun i => x i ω) (fun i => y i ω) n
18 noncomputable def radius (denominator : ℕ) (sigma : ℚ) (delta : ℝ)
19     (x : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℚ :=
20   RationalConfidenceArithmetic.outerRadius denominator sigma (variance x n ω) delta
21 noncomputable def lower (radiusGrid endpointGrid : ℕ) (sigma : ℚ) (delta : ℝ)
22     (x y : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℚ :=
23   lowerEndpoint endpointGrid (estimate x y n ω) (radius radiusGrid sigma delta x n ω)
24 noncomputable def upper (radiusGrid endpointGrid : ℕ) (sigma : ℚ) (delta : ℝ)
25     (x y : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℚ :=
26   upperEndpoint endpointGrid (estimate x y n ω) (radius radiusGrid sigma delta x n ω)
27 
28 /-- The scalar covariance and ridge estimate are the actual P81 objects;
29 the returned event is its actual Gaussian-mixture no-crossing event. -/
30 theorem scalar_outer_certificate (F : Filtration ℕ mΩ)
31     (radiusGrid endpointGrid : ℕ) (hr : 0<radiusGrid) (he : 0<endpointGrid)
32     (sigma : ℚ) (hs : 0<sigma) (delta : ℝ) (hd : 0<delta) (hd1 : delta≤1)
33     (x y : ℕ → Ω → ℝ) (theta : ℝ)
34     (hx : ∀ n,Measurable[F n] (x n)) (hy : ∀ n,Measurable[F (n+1)] (y n)) (htheta : |theta|≤1)
35     (H : ∀ n,ConditionalSubgaussian (F.le n) (fun ω => y n ω-theta*x n ω) sigma μ) :
36     MeasurableSet (scalarGood sigma delta x y theta) ∧
37     1-delta≤μ.real (scalarGood sigma delta x y theta) ∧
38     ∀ ω∈scalarGood sigma delta x y theta,∀ n,
39       theta∈Set.Icc (lower radiusGrid endpointGrid sigma delta x y n ω : ℝ)
40         (upper radiusGrid endpointGrid sigma delta x y n ω : ℝ) := by
41   have hsr : (0 : ℝ)<sigma := by exact_mod_cast hs
42   have hc := scalar_regression_confidence_certificate F sigma delta hsr hd hd1 x y theta hx hy htheta H
43   refine ⟨hc.1,hc.2.1,?_⟩
44   intro ω hω n
45   have herr := hc.2.2 ω hω n
46   have hbound := RationalConfidenceArithmetic.scalarRadius_le_outer radiusGrid hr sigma hs.le
47     (variance x n ω) delta (scalarV_ge_one _ _) hd hd1
48   change |estimate x y n ω-theta|≤
49     RationalConfidenceArithmetic.scalarRadius sigma (variance x n ω) delta at herr
50   exact contains_true endpointGrid he _ theta _ _ herr hbound htheta
51 
52 theorem two_good_coverage (A B : Set Ω) (hA : MeasurableSet A) (hB : MeasurableSet B)
53     (hpA : 1-(1/40 : ℝ)≤μ.real A) (hpB : 1-(1/40 : ℝ)≤μ.real B) :
54     (19/20 : ℝ)≤μ.real (A∩B) := by
55   have ha := measureReal_add_measureReal_compl (μ := μ) hA
56   have hb := measureReal_add_measureReal_compl (μ := μ) hB
57   have hg := measureReal_add_measureReal_compl (μ := μ) (hA.inter hB)
58   simp only [probReal_univ] at ha hb hg
59   have hu := measureReal_union_le (μ := μ) Aᶜ Bᶜ
60   rw [← Set.compl_inter] at hu
61   linarith
62 
63 /-- No independence between response coordinates is required for their
64 simultaneous all-time coverage. The two exact source noise scales are derived. -/
65 theorem two_regression_outer_certificate (F : Filtration ℕ mΩ)
66     (endpointGrid : ℕ) (he : 0<endpointGrid)
67     (xA yA xB yB : ℕ → Ω → ℝ) (thetaA thetaB : ℝ)
68     (hxA : ∀ n,Measurable[F n] (xA n)) (hyA : ∀ n,Measurable[F (n+1)] (yA n))
69     (hxB : ∀ n,Measurable[F n] (xB n)) (hyB : ∀ n,Measurable[F (n+1)] (yB n))
70     (hbA : ∀ n,∀ᵐ ω∂μ,yA n ω∈Set.Icc (-1 : ℝ) 1)
71     (hbB : ∀ n,∀ᵐ ω∂μ,yB n ω∈Set.Icc (-(1/2) : ℝ) 1)
72     (hmA : ∀ n,(μ[yA n|F n])=ᵐ[μ] (fun ω => thetaA*xA n ω))
73     (hmB : ∀ n,(μ[yB n|F n])=ᵐ[μ] (fun ω => thetaB*xB n ω))
74     (htA : |thetaA|≤1) (htB : |thetaB|≤1) :
75     let G := scalarGood 1 (1/40) xA yA thetaA∩scalarGood (3/4) (1/40) xB yB thetaB
76     MeasurableSet G ∧ (19/20 : ℝ)≤μ.real G ∧ ∀ ω∈G,∀ n,
77       thetaA∈Set.Icc (lower (10^12) endpointGrid 1 (1/40) xA yA n ω : ℝ)
78         (upper (10^12) endpointGrid 1 (1/40) xA yA n ω : ℝ) ∧
79       thetaB∈Set.Icc (lower (10^12) endpointGrid (3/4) (1/40) xB yB n ω : ℝ)
80         (upper (10^12) endpointGrid (3/4) (1/40) xB yB n ω : ℝ) := by
81   have hA := scalar_outer_certificate F (10^12) endpointGrid (by norm_num) he 1 (by norm_num)
82     (1/40) (by norm_num) (by norm_num) xA yA thetaA hxA hyA htA
83     (by simpa only [Rat.cast_one] using
84       BoundedResponseNoise.process_neg_one_one F thetaA xA yA hxA hyA hbA hmA)
85   have hB := scalar_outer_certificate F (10^12) endpointGrid (by norm_num) he (3/4) (by norm_num)
86     (1/40) (by norm_num) (by norm_num) xB yB thetaB hxB hyB htB
87     (by simpa only [Rat.cast_div,Rat.cast_ofNat] using
88       BoundedResponseNoise.process_neg_half_one F thetaB xB yB hxB hyB hbB hmB)
89   simp only [Rat.cast_one,Rat.cast_div,Rat.cast_ofNat] at hA hB
90   exact ⟨hA.1.inter hB.1,two_good_coverage _ _ hA.1 hB.1 hA.2.1 hB.2.1,
91     fun ω hω n => ⟨hA.2.2 ω hω.1 n,hB.2.2 ω hω.2 n⟩⟩
92 
93 end Komorebi.LSM.RationalRegressionConfidence

Back to source controls