CertifiedRepairUpper.lean

1 import KomorebiLSM.ConvexRepairBracketing
2 import KomorebiLSM.RationalBernsteinMargin
3 
4 /-! An actual complete rational subdivision certificate supplies P80's upper
5 bracket for the same repaired family, rather than an assumed feasibility result. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.CertifiedRepairUpper
8 open LorentzCylinder RobustOrientedMargin InteriorRepair ConvexRepairBracketing RationalBernsteinMargin
9 variable {A : Type*} {n : ℕ}
10 
11 /-- Exact family identification connects the finite P75 witness to the repair being bracketed. -/
12 theorem bernstein_upper_bound
13     (H : A → ℝ → State ℂ →L[ℝ] State ℂ) (G : A → Fin n → RationalMatrix) (kappa : ℚ)
14     (etaU : ℝ) (hetaU : etaU∈Set.Icc 0 1) (certificate : ∀ a,Certificate (G a) kappa)
15     (sameFamily : ∀ a u,PolynomialGram.operatorPolynomial (fun k => matrixOperator (G a k)) u=
16       repair (H a u) 1 etaU) :
17     etaStar H (kappa : ℝ)≤etaU := by
18   apply certificate_upper_bound H (kappa : ℝ) etaU hetaU
19   intro a u hu
20   simpa only [sameFamily a u] using (certificate a).margin u hu
21 
22 /-- The lower endpoint is bracketed by a genuine evaluated positive functional
23 and a complete, sound certificate on the entire repaired family. -/
24 theorem certified_bracket
25     (H : A → ℝ → State ℂ →L[ℝ] State ℂ) (G : A → Fin n → RationalMatrix) (kappa : ℚ)
26     (hkappa : kappa∈Set.Icc 0 1) (etaU : ℝ) (hetaU : etaU∈Set.Icc 0 1)
27     (certificate : ∀ a,Certificate (G a) kappa)
28     (sameFamily : ∀ a u,PolynomialGram.operatorPolynomial (fun k => matrixOperator (G a k)) u=
29       repair (H a u) 1 etaU)
30     (a : A) (u : ℝ) (hu : u∈Set.Icc (-1 : ℝ) 1) (v q : ℂ) (hv : ‖v‖≤1) (hq : ‖q‖≤1)
31     (hbad : separator q (H a u (1,v))<(kappa : ℝ)) :
32     etaStar H (kappa : ℝ)∈Set.Icc 0 1 ∧
33       (kappa-separator q (H a u (1,v)))/(1-separator q (H a u (1,v)))≤etaStar H (kappa : ℝ) ∧
34       etaStar H (kappa : ℝ)≤etaU := by
35   have hkappa1 : (kappa : ℝ)≤1 := by exact_mod_cast hkappa.2
36   exact ⟨etaStar_in_unit H _ hkappa1,
37     separator_lower_endpoint H _ hkappa1 a u hu v q hv hq hbad,
38     bernstein_upper_bound H G kappa etaU hetaU certificate sameFamily⟩
39 
40 end Komorebi.LSM.CertifiedRepairUpper

Back to source controls