ScalarRegressionConfidence.lean

1 import KomorebiLSM.RegressionConfidence
2 
3 /-! The literal scalar ridge-one, unit-prior-bound specialization of P81. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.RegressionConfidence
6 open MeasureTheory ProbabilityTheory Matrix
7 open scoped BigOperators
8 
9 noncomputable def scalarV (x : ℕ → ℝ) (n : ℕ) : ℝ := 1+∑ i∈Finset.range n,(x i)^2
10 noncomputable def scalarEstimate (x y : ℕ → ℝ) (n : ℕ) : ℝ :=
11   (∑ i∈Finset.range n,x i*y i)/scalarV x n
12 noncomputable def scalarRadius (σ δ : ℝ) (x : ℕ → ℝ) (n : ℕ) : ℝ :=
13   σ*Real.sqrt ((Real.log (scalarV x n)+2*Real.log (1/δ))/scalarV x n)+
14     Real.sqrt (1/scalarV x n)
15 
16 theorem scalarV_ge_one (x : ℕ → ℝ) (n : ℕ) : 1≤scalarV x n := by
17   exact le_add_of_nonneg_right (Finset.sum_nonneg (fun i _ => sq_nonneg (x i)))
18 
19 theorem scalarV_pos (x : ℕ → ℝ) (n : ℕ) : 0<scalarV x n :=
20   lt_of_lt_of_le zero_lt_one (scalarV_ge_one x n)
21 
22 theorem ridgeMatrix_scalar_entry (x : ℕ → ℝ) (n : ℕ) :
23     ridgeMatrix (I := Fin 1) 1 (fun i _ => x i) n 0 0=scalarV x n := by
24   simp [ridgeMatrix,designGram,scalarV,Matrix.sum_apply,Matrix.vecMulVec_apply,pow_two]
25 
26 theorem ridgeEstimate_scalar (x y : ℕ → ℝ) (n : ℕ) :
27     ridgeEstimate (I := Fin 1) 1 (fun i _ => x i) y n 0=scalarEstimate x y n := by
28   unfold ridgeEstimate
29   rw [Matrix.inv_subsingleton]
30   simp [Matrix.mulVec,dotProduct,Ring.inverse_eq_inv,responseVector,
31     Finset.sum_apply,ridgeMatrix_scalar_entry,scalarEstimate,div_eq_mul_inv,mul_comm]
32 
33 theorem weightedNorm_scalar (V : Matrix (Fin 1) (Fin 1) ℝ) (z : Fin 1 → ℝ)
34     (hV : 0≤V 0 0) : weightedNorm V z=Real.sqrt (V 0 0)*|z 0| := by
35   have hq : z ⬝ᵥ (V *ᵥ z)=V 0 0*(z 0)^2 := by
36     simp [dotProduct,Matrix.mulVec,pow_two]
37     ring
38   unfold weightedNorm
39   rw [hq,Real.sqrt_mul hV,Real.sqrt_sq_eq_abs]
40 
41 theorem euclideanNorm_scalar (θ : ℝ) : euclideanNorm (fun _ : Fin 1 => θ)=|θ| := by
42   simp [euclideanNorm_eq,dotProduct,← pow_two,Real.sqrt_sq_eq_abs]
43 
44 variable {Ω : Type*}
45 /-- The same actual generic Gaussian-mixture good event, specialized to Fin1. -/
46 noncomputable def scalarGood (σ δ : ℝ) (x y : ℕ → Ω → ℝ) (θ : ℝ) : Set Ω :=
47   regressionGood 1 σ δ (fun i ω (_ : Fin 1) => x i ω) y (fun _ => θ)
48 
49 theorem scalarGood_error_bound (σ δ : ℝ) (hσ : 0<σ) (hδ : 0<δ) (hδ1 : δ≤1)
50     (x y : ℕ → Ω → ℝ) (θ : ℝ) (hθ : |θ|≤1) (ω : Ω)
51     (hg : ω∈scalarGood σ δ x y θ) (n : ℕ) :
52     |scalarEstimate (fun i => x i ω) (fun i => y i ω) n-θ|≤
53       scalarRadius σ δ (fun i => x i ω) n := by
54   have hprior : euclideanNorm (fun _ : Fin 1 => θ)≤1 := by simpa only [euclideanNorm_scalar] using hθ
55   have h := regressionGood_error_bound 1 σ δ 1 (by norm_num) hσ hδ
56     (fun i ω (_ : Fin 1) => x i ω) y (fun _ => θ) hprior ω hg n
57   rw [weightedNorm_scalar _ _ (by rw [ridgeMatrix_scalar_entry]; exact (scalarV_pos _ _).le),
58     ridgeMatrix_scalar_entry] at h
59   simp only [Pi.sub_apply,ridgeEstimate_scalar,noiseRadius,Matrix.det_fin_one,
60     ridgeMatrix_scalar_entry,one_smul,Matrix.one_apply_eq,div_one,Real.sqrt_one,mul_one] at h
61   have hbound : |scalarEstimate (fun i => x i ω) (fun i => y i ω) n-θ|≤
62       (σ*Real.sqrt (Real.log (scalarV (fun i => x i ω) n)+2*Real.log (1/δ))+1)/
63         Real.sqrt (scalarV (fun i => x i ω) n) := by
64     apply (le_div_iff₀ (Real.sqrt_pos.2 (scalarV_pos _ _))).2
65     simpa only [mul_comm] using h
66   apply hbound.trans_eq
67   unfold scalarRadius
68   have hlog : 0≤Real.log (1/δ) :=
69     Real.log_nonneg ((le_div_iff₀ hδ).2 (by simpa using hδ1))
70   have ha : 0≤Real.log (scalarV (fun i => x i ω) n)+2*Real.log (1/δ) :=
71     add_nonneg (Real.log_nonneg (scalarV_ge_one _ _)) (mul_nonneg (by norm_num) hlog)
72   rw [Real.sqrt_div ha,Real.sqrt_div (show (0:ℝ)≤1 by norm_num),Real.sqrt_one]
73   ring
74 
75 variable [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
76 /-- The literal scalar estimator and source radius inherit the actual generic
77 P81 probability event, without an independent scalar concentration assumption. -/
78 theorem scalar_regression_confidence_certificate (ℱ : Filtration ℕ mΩ)
79     (σ δ : ℝ) (hσ : 0<σ) (hδ : 0<δ) (hδ1 : δ≤1)
80     (x y : ℕ → Ω → ℝ) (θ : ℝ)
81     (hx : ∀ n,Measurable[ℱ n] (x n)) (hy : ∀ n,Measurable[ℱ (n+1)] (y n)) (hθ : |θ|≤1)
82     (H : ∀ n,ConditionalSubgaussian (ℱ.le n) (fun ω => y n ω-θ*x n ω) σ μ) :
83     MeasurableSet (scalarGood σ δ x y θ) ∧ 1-δ≤μ.real (scalarGood σ δ x y θ) ∧
84     ∀ ω∈scalarGood σ δ x y θ,∀ n,
85       |scalarEstimate (fun i => x i ω) (fun i => y i ω) n-θ|≤
86         scalarRadius σ δ (fun i => x i ω) n := by
87   have hprior : euclideanNorm (fun _ : Fin 1 => θ)≤1 := by simpa only [euclideanNorm_scalar] using hθ
88   have H' : ∀ n,ConditionalSubgaussian (ℱ.le n)
89       (regressionNoise (fun _ : Fin 1 => θ) (fun i ω _ => x i ω) y n) σ μ := by
90     intro n
91     unfold regressionNoise
92     simpa [dotProduct] using H n
93   have hc := regression_confidence_certificate ℱ 1 σ δ 1 (by norm_num) hσ hδ
94     (fun i ω (_ : Fin 1) => x i ω) y (fun _ => θ) (fun n _ => hx n) hy hprior H'
95   exact ⟨hc.1,hc.2.1,fun ω hω n => scalarGood_error_bound σ δ hσ hδ hδ1 x y θ hθ ω hω n⟩
96 
97 end Komorebi.LSM.RegressionConfidence

Back to source controls