StrictRationalGeometry.lean

1 import KomorebiLSM.RationalTransform
2 import Mathlib.Topology.Compactness.Compact
3 
4 set_option autoImplicit false
5 namespace Komorebi.LSM.StrictRationalGeometry
6 open scoped Topology
7 open Filter LorentzCylinder RobustOrientedMargin RationalTransform
8 noncomputable section
9 variable {n : ℕ}
10 
11 /-- Joint output continuity uses the literal inverse-conjugated density. -/
12 theorem continuousAt_conjugated_slack (G : Fin n → RationalMatrix) (T : RealMatrix)
13     (hT : IsUnit T.det) (y : ℝ × ℂ) :
14     ContinuousAt (fun Ty : RealMatrix × (ℝ × ℂ) => slack (conjugated Ty.1 G Ty.2.1 (1,Ty.2.2))) (T,y) := by
15   have hcoords : Continuous (fun Ty : RealMatrix × (ℝ × ℂ) => (Ty.1,Ty.2.1)) :=
16     continuous_fst.prodMk continuous_snd.fst
17   have hc : ContinuousAt (fun Ty : RealMatrix × (ℝ × ℂ) => conjugated Ty.1 G Ty.2.1) (T,y) :=
18     ContinuousAt.comp (f := fun Ty : RealMatrix × (ℝ × ℂ) => (Ty.1,Ty.2.1))
19       (x := (T,y)) (continuousAt_conjugated G T hT y.1) (hcoords.continuousAt (x := (T,y)))
20   have hz : Continuous (fun Ty : RealMatrix × (ℝ × ℂ) => ((1 : ℝ),Ty.2.2)) :=
21     continuous_const.prodMk continuous_snd.snd
22   exact continuous_slack.continuousAt.comp (hc.clm_apply (hz.continuousAt (x := (T,y))))
23 
24 /-- Compact observation and input sets turn pointwise continuity into one transform neighborhood. -/
25 theorem eventually_margin (G : Fin n → RationalMatrix) (T : RealMatrix)
26     (hT : IsUnit T.det) (kappa : ℝ)
27     (hmargin : ∀ u∈Set.Icc (-1 : ℝ) 1, kappa<sigma (conjugated T G u)) :
28     ∀ᶠ S in 𝓝 T, ∀ u∈Set.Icc (-1 : ℝ) 1, kappa<sigma (conjugated S G u) := by
29   let K : Set (ℝ × ℂ) := Set.Icc (-1 : ℝ) 1  ×ˢ Metric.closedBall 0 1
30   have hK : IsCompact K := isCompact_Icc.prod (isCompact_closedBall (0 : ℂ) 1)
31   have hpoint : ∀ y∈K, ∀ᶠ Ty : RealMatrix × (ℝ × ℂ) in 𝓝 (T,y),
32       kappa<slack (conjugated Ty.1 G Ty.2.1 (1,Ty.2.2)) := by
33     intro y hy
34     have hv : ‖y.2‖≤1 := by simpa using hy.2
35     have hm := (hmargin y.1 hy.1).trans_le (sigma_le (conjugated T G y.1) y.2 hv)
36     exact (continuousAt_conjugated_slack G T hT y).eventually (Ioi_mem_nhds hm)
37   have he := hK.eventually_forall_of_forall_eventually (x₀ := T)
38     (P := fun S y => kappa<slack (conjugated S G y.1 (1,y.2))) hpoint
39   filter_upwards [he] with S hS
40   intro u hu
41   apply hS (u,worstInput (conjugated S G u))
42   exact ⟨hu,by simpa using worstInput_mem (conjugated S G u)⟩
43 
44 theorem eventually_initial (T : RealMatrix) (z : State ℂ) (hz : 0<slack (operator T z)) :
45     ∀ᶠ S in 𝓝 T, 0<slack (operator S z) := by
46   have hc : Continuous (fun S : RealMatrix => slack (operator S z)) :=
47     continuous_slack.comp (continuous_operator.clm_apply continuous_const)
48   exact hc.continuousAt.eventually (Ioi_mem_nhds hz)
49 
50 /-- A real strict finite sector contains an actual rational mass-preserving invertible transform. -/
51 theorem rational_strict_sector {I A J : Type*} [Fintype I] [Fintype A] [Fintype J]
52     (G : I → A → Fin n → RationalMatrix) (z : J → State ℂ)
53     (T : RealMatrix) (hT : IsUnit T.det) (hmass : MassPreserving T)
54     (hinit : ∀ j, 0<slack (operator T (z j))) (eta : ℝ) (heta : 0<eta)
55     (hmargin : ∀ i a u, u∈Set.Icc (-1 : ℝ) 1 → eta≤sigma (conjugated T (G i a) u)) :
56     ∃ q : Parameters ℚ, ∃ kappa : ℚ, 0<kappa ∧ IsUnit (affineMatrix q).det ∧
57       (∀ j, 0<slack (operator (castMatrix (affineMatrix q)) (z j))) ∧
58       ∀ i a u, u∈Set.Icc (-1 : ℝ) 1 →
59         (kappa : ℝ)<sigma (PolynomialGram.operatorPolynomial
60           (fun k => RationalBernsteinMargin.matrixOperator
61             (rationalConjugated (affineMatrix q) (G i a) k)) u) := by
62   obtain ⟨kappa,hk0,hketa⟩ := exists_rat_btwn heta
63   have hi : ∀ᶠ S in 𝓝 T, ∀ j,0<slack (operator S (z j)) :=
64     Filter.eventually_all.mpr (fun j => eventually_initial T (z j) (hinit j))
65   have hf : ∀ᶠ S in 𝓝 T, ∀ i a u,u∈Set.Icc (-1 : ℝ) 1 →
66       (kappa : ℝ)<sigma (conjugated S (G i a) u) := by
67     apply Filter.eventually_all.mpr
68     intro i
69     apply Filter.eventually_all.mpr
70     intro a
71     exact eventually_margin (G i a) T hT kappa (fun u hu => hketa.trans_le (hmargin i a u hu))
72   have hd : ∀ᶠ S in 𝓝 T, IsUnit S.det := by
73     have hne : T.det≠0 := isUnit_iff_ne_zero.mp hT
74     have he := continuous_id.matrix_det.continuousAt.eventually
75       (isOpen_ne.mem_nhds hne)
76     simpa [isUnit_iff_ne_zero] using he
77   have hall : ∀ᶠ S in 𝓝 T, IsUnit S.det ∧ (∀ j,0<slack (operator S (z j))) ∧
78       ∀ i a u,u∈Set.Icc (-1 : ℝ) 1 → (kappa : ℝ)<sigma (conjugated S (G i a) u) := by
79     filter_upwards [hd,hi,hf] with S hS hI hF
80     exact ⟨hS,hI,hF⟩
81   have hc : Tendsto (affineMatrix (R := ℝ)) (𝓝 (parametersOf T)) (𝓝 T) := by
82     have hcont : Tendsto (affineMatrix (R := ℝ)) (𝓝 (parametersOf T))
83         (𝓝 (affineMatrix (parametersOf T))) := continuous_affineMatrix.continuousAt
84     rwa [affineMatrix_parametersOf T hmass] at hcont
85   obtain ⟨q,hq⟩ := dense_castParameters.mem_nhds (hc.eventually hall)
86   change IsUnit (affineMatrix (castParameters q)).det ∧
87     (∀ j, 0<slack (operator (affineMatrix (castParameters q)) (z j))) ∧
88     (∀ i a u, u∈Set.Icc (-1 : ℝ) 1 →
89       (kappa : ℝ)<sigma (conjugated (affineMatrix (castParameters q)) (G i a) u)) at hq
90   rw [affineMatrix_cast] at hq
91   have hqdet := unit_of_castMatrix (affineMatrix q) hq.1
92   refine ⟨q,kappa,by exact_mod_cast hk0,hqdet,hq.2.1,?_⟩
93   intro i a u hu
94   rw [rational_conjugated_operator (affineMatrix q) hqdet]
95   exact hq.2.2 i a u hu
96 
97 end
98 end Komorebi.LSM.StrictRationalGeometry

Back to source controls