RegressionRadius.lean

1 import KomorebiLSM.RegressionGeometry
2 import Mathlib.Analysis.SpecialFunctions.Log.Basic
3 import Mathlib.Tactic
4 
5 /-! The logarithmic inversion of the actual Gaussian-mixture crossing bound. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RegressionConfidence
8 open Matrix
9 open scoped BigOperators
10 variable {I : Type*} [Fintype I] [DecidableEq I]
11 
12 /-- The literal determinant-dependent noise radius in Proposition81. -/
13 noncomputable def noiseRadius (γ σ δ : ℝ) (φ : ℕ → I → ℝ) (n : ℕ) : ℝ :=
14   σ * Real.sqrt (Real.log ((ridgeMatrix γ φ n).det/(γ • (1 : Matrix I I ℝ)).det)+
15     2*Real.log (1/δ))
16 
17 /-- Below a Gaussian-mixture crossing threshold, taking actual logarithms
18 bounds the genuine inverse-matrix score norm. -/
19 theorem mixture_lt_implies_noise_bound (V W : Matrix I I ℝ) (hV : V.PosDef) (hW : W.PosDef)
20     (σ δ : ℝ) (hσ : 0 < σ) (hδ : 0 < δ) (score : I → ℝ)
21     (h : Real.sqrt (W.det/V.det)*Real.exp ((weightedNorm V⁻¹ score)^2/(2*σ^2))<1/δ) :
22     weightedNorm V⁻¹ score ≤
23       σ*Real.sqrt (Real.log (V.det/W.det)+2*Real.log (1/δ)) := by
24   have hp : 0 < Real.sqrt (W.det/V.det) := Real.sqrt_pos.2 (div_pos hW.det_pos hV.det_pos)
25   have ht := (Real.log_lt_log_iff (mul_pos hp (Real.exp_pos _)) (one_div_pos.2 hδ)).2 h
26   rw [Real.log_mul (ne_of_gt hp) (Real.exp_ne_zero _),Real.log_exp,
27     Real.log_sqrt (div_nonneg hW.det_pos.le hV.det_pos.le),
28     Real.log_div (ne_of_gt hW.det_pos) (ne_of_gt hV.det_pos)] at ht
29   have hden : 0 < 2*σ^2 := mul_pos (by norm_num) (sq_pos_of_ne_zero (ne_of_gt hσ))
30   have ht' : (weightedNorm V⁻¹ score)^2/(2*σ^2) <
31       (Real.log V.det-Real.log W.det)/2+Real.log (1/δ) := by linarith
32   have hm := (div_lt_iff₀ hden).mp ht'
33   have hs : (weightedNorm V⁻¹ score)^2 <
34       σ^2*(Real.log (V.det/W.det)+2*Real.log (1/δ)) := by
35     rw [Real.log_div (ne_of_gt hV.det_pos) (ne_of_gt hW.det_pos)]
36     nlinarith
37   have ha : 0 ≤ Real.log (V.det/W.det)+2*Real.log (1/δ) := by
38     by_contra hneg
39     have hprod := mul_neg_of_pos_of_neg (sq_pos_of_ne_zero (ne_of_gt hσ)) (lt_of_not_ge hneg)
40     nlinarith [sq_nonneg (weightedNorm V⁻¹ score)]
41   have he : (σ*Real.sqrt (Real.log (V.det/W.det)+2*Real.log (1/δ)))^2 =
42       σ^2*(Real.log (V.det/W.det)+2*Real.log (1/δ)) := by
43     rw [mul_pow,Real.sq_sqrt ha]
44   rw [← he] at hs
45   nlinarith [weightedNorm_nonneg V⁻¹ score,
46     mul_nonneg hσ.le (Real.sqrt_nonneg (Real.log (V.det/W.det)+2*Real.log (1/δ)))]
47 
48 end Komorebi.LSM.RegressionConfidence

Back to source controls