HolonomyGapCertificate.lean

1 import KomorebiSpace.HolonomyProjection
2 import Mathlib.Analysis.SpecialFunctions.Pow.Real
3 import Mathlib.Tactic.Linarith
4 
5 set_option autoImplicit false
6 
7 /-!
8 # Quadratic gap certificates with the correct residual-norm conversion
9 
10 The existing edge-family norm is the maximum norm. A squared Euclidean
11 stacking estimate therefore contributes sqrt(card I), not a silent
12 identification of the maximum norm with a Hilbert norm.
13 The generic finite-dimensional gain is derived independently; this module
14 supplies one way to certify an explicit bound for it.
15 -/
16 universe u v w
17 noncomputable section
18 namespace KomorebiSpace
19 namespace KernelProjection
20 variable {E : Type u} {F : Type v} {I : Type w}
21 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
22 variable [NormedAddCommGroup F] [NormedSpace ℝ F] [Fintype I]
23 variable (d : E →L[ℝ] (I → F))
24 
25 /-- A checkable lower bound on the squared loop defect in complementary directions. -/
26 def QuadraticGap (lam : ℝ) : Prop :=
27   ∀ x : E, x ∈ d.kerᗮ → lam * ‖x‖^2 ≤ ∑ i : I, ‖d x i‖^2
28 
29 omit [FiniteDimensional ℝ E] in
30 /-- Squared stacked residual is bounded by the number of components times the max norm squared. -/
31 theorem sum_squared_le_card (x : E) :
32     (∑ i : I, ‖d x i‖^2) ≤ (Fintype.card I : ℝ) * ‖d x‖^2 := by
33   calc
34     _ ≤ ∑ _i : I, ‖d x‖^2 := by
35       apply Finset.sum_le_sum
36       intro i _hi
37       have hn := norm_le_pi_norm (d x) i
38       have h0 := norm_nonneg (d x i)
39       nlinarith
40     _ = _ := by simp [Finset.sum_const, nsmul_eq_mul]
41 
42 /-- An explicit squared estimate for the constructed orthogonal correction. -/
43 theorem error_sq_of_quadratic_gap (lam : ℝ) (hg : QuadraticGap d lam) (x : E) :
44     lam * ‖x-projection d x‖^2 ≤ (Fintype.card I : ℝ) * ‖d x‖^2 := by
45   have hb := hg (x-projection d x) (error_orthogonal d x)
46   have hn := sum_squared_le_card d (x-projection d x)
47   rw [defect_error] at hn hb
48   exact hb.trans hn
49 
50 /-- Explicit max-residual bound; the sqrt(card I) conversion is retained. -/
51 theorem error_of_quadratic_gap (lam : ℝ) (hpos : 0 < lam)
52     (hg : QuadraticGap d lam) (x : E) :
53     ‖x-projection d x‖ ≤ Real.sqrt ((Fintype.card I : ℝ)/lam) * ‖d x‖ := by
54   have hs := error_sq_of_quadratic_gap d lam hg x
55   have hb : ‖x-projection d x‖^2 ≤ ((Fintype.card I : ℝ) * ‖d x‖^2)/lam := by
56     apply (le_div_iff₀ hpos).mpr
57     nlinarith
58   have hn : 0 ≤ (Fintype.card I : ℝ)/lam := by positivity
59   have he : ((Fintype.card I : ℝ) * ‖d x‖^2)/lam =
60       (Real.sqrt ((Fintype.card I : ℝ)/lam) * ‖d x‖)^2 := by
61     rw [mul_pow, Real.sq_sqrt hn]
62     ring
63   rw [he] at hb
64   exact (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp hb
65 
66 theorem gain_le_of_quadratic_gap (lam : ℝ) (hpos : 0 < lam)
67     (hg : QuadraticGap d lam) :
68     gain d ≤ Real.sqrt ((Fintype.card I : ℝ)/lam) :=
69   gain_le_of_bound d _ (Real.sqrt_nonneg _) (error_of_quadratic_gap d lam hpos hg)
70 
71 end KernelProjection
72 
73 namespace HolonomyTransport
74 namespace Rooted
75 variable {V : Type u} {H : Type v}
76 variable [NormedAddCommGroup H] [InnerProductSpace ℝ H] [FiniteDimensional ℝ H]
77 variable [Fintype V]
78 variable (T : Connection V H) {graph : SimpleGraph V} {o : V}
79 variable (p : OverlapTransport.Routing graph o)
80 
81 theorem holonomyGain_certificate (lam : ℝ) (hpos : 0 < lam)
82     (hg : KernelProjection.QuadraticGap (rootResidualMap T p) lam) :
83     holonomyGain T p ≤ Real.sqrt ((Fintype.card (OverlapTransport.Edges graph) : ℝ)/lam) :=
84   KernelProjection.gain_le_of_quadratic_gap (rootResidualMap T p) lam hpos hg
85 
86 /-- A certified squared spectral lower bound yields a numerical graph repair bound
87 without replacing the existing maximum residual norm by a Euclidean product norm. -/
88 theorem certified_orthogonalRepair_error (lam : ℝ) (hpos : 0 < lam)
89     (hg : KernelProjection.QuadraticGap (rootResidualMap T p) lam) (x : V → H) :
90     ‖x-orthogonalRepair T p x‖ ≤
91       ((p.radius : ℝ) + Real.sqrt ((Fintype.card (OverlapTransport.Edges graph) : ℝ)/lam) *
92         (2*(p.radius : ℝ)+1)) * ‖T.differential graph x‖ := by
93   have hc := mul_le_mul_of_nonneg_right (holonomyGain_certificate T p lam hpos hg)
94     (show 0 ≤ 2*(p.radius : ℝ)+1 by positivity)
95   exact (orthogonalRepair_error T p x).trans
96     (mul_le_mul_of_nonneg_right (add_le_add le_rfl hc) (norm_nonneg _))
97 
98 end Rooted
99 end HolonomyTransport
100 end KomorebiSpace
101 end

Back to source controls