DiagonalInexactRate.lean

1 import KomorebiSpace.DiagonalNoisyRate
2 
3 set_option autoImplicit false
4 noncomputable section
5 
6 namespace KomorebiSpace.DiagonalRegularization
7 
8 /-- An inexact solve retains the printed diagonal rate at the literal rounded
9 parameter. The normal residual is evaluated against the measured datum `s`.
10 Here `T`, `b`, and `w` belong to the actual infinite diagonal Hilbert model,
11 and `alpha m = ((m : ℝ)^2)⁻¹`. No exact-data bias hypothesis is assumed. -/
12 theorem diagonal_inexact_rounded_rate (s a : H) {δ κ ε : ℝ}
13     (hδ : 0 < δ) (hδ₁ : δ ≤ 1) (hκ : 0 ≤ κ)
14     (hdata : ‖s - b‖ ≤ δ)
15     (hsolve : ‖T.adjoint (T a - s) +
16       alpha (Nat.ceil (δ ^ (-(2 : ℝ) / 3))) • a‖ ≤ ε)
17     (hε : ε ≤ κ * alpha (Nat.ceil (δ ^ (-(2 : ℝ) / 3))) *
18       δ ^ ((1 : ℝ) / 3)) :
19     ‖a - w‖ ≤ (Real.sqrt 2 + 1 + κ) * δ ^ ((1 : ℝ) / 3) := by
20   let m := Nat.ceil (δ ^ (-(2 : ℝ) / 3))
21   have hm : 1 ≤ m := one_le_noiseSchedule hδ
22   have hα : 0 < alpha m := alpha_pos hm
23   have hres : ‖RegularizedHilbertRepair.gradient T (alpha m) s a‖ ≤ ε := by
24     have he : RegularizedHilbertRepair.gradient T (alpha m) s a =
25         T.adjoint (T a - s) + alpha m • a := by
26       simp only [RegularizedHilbertRepair.gradient,
27         RegularizedHilbertRepair.normal_apply, map_sub]
28       abel
29     rw [he]
30     exact hsolve
31   have hbudget : 0 ≤ κ * δ ^ ((1 : ℝ) / 3) :=
32     mul_nonneg hκ (Real.rpow_pos_of_pos hδ _).le
33   have hsolver :
34       ‖a - RegularizedHilbertRepair.correction T (alpha m) hα s‖ ≤
35         κ * δ ^ ((1 : ℝ) / 3) := by
36     refine (RegularizedHilbertRepair.correction_error_bound T (alpha m) hα s a).trans ?_
37     apply (div_le_iff₀ hα).2
38     have hr := hres.trans hε
39     change _ ≤ κ * alpha m * δ ^ ((1 : ℝ) / 3) at hr
40     nlinarith [hbudget]
41   have hnoisy := corollary_30_3 s hδ hδ₁ hdata
42   change ‖RegularizedHilbertRepair.correction T (alpha m) hα s - w‖ ≤
43       Real.sqrt (2 / (m : ℝ)) + δ * (m : ℝ) / 2 ∧
44     Real.sqrt (2 / (m : ℝ)) + δ * (m : ℝ) / 2 ≤
45       (Real.sqrt 2 + 1) * δ ^ ((1 : ℝ) / 3) at hnoisy
46   have he : a - w =
47       (a - RegularizedHilbertRepair.correction T (alpha m) hα s) +
48       (RegularizedHilbertRepair.correction T (alpha m) hα s - w) := by abel
49   rw [he]
50   exact (norm_add_le _ _).trans
51     ((add_le_add hsolver (hnoisy.1.trans hnoisy.2)).trans_eq (by ring))
52 
53 end KomorebiSpace.DiagonalRegularization

Back to source controls