RationalSemicircle.lean

1 import KomorebiLSM.RobustOrientedMargin
2 import Mathlib.Analysis.Complex.Basic
3 import Mathlib.Analysis.Normed.Module.Convex
4 
5 /-! The two literal rational circle charts and the oriented full-disk consequence. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RationalSemicircle
8 open LorentzCylinder RobustOrientedMargin
9 noncomputable section
10 
11 /-- The strictly positive denominator shared by both semicircles. -/
12 def denominator (t : ℝ) : ℝ := 1+t^2
13 
14 theorem denominator_pos (t : ℝ) : 0<denominator t := by
15   unfold denominator
16   positivity
17 
18 /-- `false` is the right semicircle and `true` its antipodal left semicircle. -/
19 def numerator (left : Bool) (t : ℝ) : ℂ :=
20   if left then ⟨-(1-t^2),-(2*t)⟩ else ⟨1-t^2,2*t⟩
21 
22 def chart (left : Bool) (t : ℝ) : ℂ := (denominator t)⁻¹ • numerator left t
23 
24 def lift (left : Bool) (t : ℝ) : State ℂ := (denominator t,numerator left t)
25 
26 theorem lift_eq (left : Bool) (t : ℝ) :
27     lift left t=denominator t • (1,chart left t) := by
28   apply Prod.ext
29   · simp [lift]
30   · change numerator left t=denominator t • ((denominator t)⁻¹ • numerator left t)
31     rw [smul_smul,mul_inv_cancel₀ (denominator_pos t).ne',one_smul]
32 
33 theorem chart_norm (left : Bool) (t : ℝ) : ‖chart left t‖=1 := by
34   have hn : Complex.normSq (numerator left t)=(denominator t)^2 := by
35     cases left <;> simp [numerator,Complex.normSq_apply,denominator] <;> ring
36   have hsq : ‖chart left t‖^2=1 := by
37     rw [chart,norm_smul,Real.norm_eq_abs,abs_of_pos (inv_pos.mpr (denominator_pos t)),
38       mul_pow,← Complex.normSq_eq_norm_sq,hn]
39     field_simp [(denominator_pos t).ne']
40   nlinarith [norm_nonneg (chart left t)]
41 
42 /-- The inverse stereographic coordinate is bounded on the entire right semicircle. -/
43 theorem right_chart_surjective (z : ℂ) (hz : ‖z‖=1) (hre : 0≤z.re) :
44     ∃ t∈Set.Icc (-1 : ℝ) 1,chart false t=z := by
45   have hs : z.re^2+z.im^2=1 := by
46     have h := Complex.normSq_eq_norm_sq z
47     rw [hz] at h
48     simpa [Complex.normSq_apply,pow_two] using h
49   have hi : |z.im|≤1 := by
50     apply (sq_le_sq₀ (abs_nonneg _) (by norm_num : (0:ℝ)≤1)).mp
51     rw [sq_abs]
52     nlinarith [sq_nonneg z.re]
53   have hd : 0<1+z.re := by linarith
54   let t : ℝ := z.im/(1+z.re)
55   have ht : t∈Set.Icc (-1 : ℝ) 1 := by
56     dsimp [t]
57     constructor
58     · apply (le_div_iff₀ hd).mpr
59       have := neg_abs_le z.im
60       linarith
61     · apply (div_le_iff₀ hd).mpr
62       have := le_abs_self z.im
63       linarith
64   refine ⟨t,ht,?_⟩
65   apply Complex.ext
66   · simp [chart,numerator,Complex.real_smul]
67     dsimp [t,denominator]
68     field_simp
69     linear_combination -(1+z.re)*hs
70   · simp [chart,numerator,Complex.real_smul]
71     dsimp [t,denominator]
72     field_simp
73     linear_combination -z.im*hs
74 
75 /-- Both signs, including their endpoints, cover the actual unit circle. -/
76 theorem charts_cover (z : ℂ) (hz : ‖z‖=1) :
77     ∃ left : Bool,∃ t∈Set.Icc (-1 : ℝ) 1,chart left t=z := by
78   by_cases h : 0≤z.re
79   · obtain ⟨t,ht,he⟩ := right_chart_surjective z hz h
80     exact ⟨false,t,ht,he⟩
81   · obtain ⟨t,ht,he⟩ := right_chart_surjective (-z) (by simpa using hz) (by simp; linarith)
82     refine ⟨true,t,ht,?_⟩
83     have heq : chart true t= -chart false t := by
84       unfold chart
85       rw [← smul_neg]
86       congr 1
87     rw [heq,he,neg_neg]
88 
89 /-- Literal polynomial orientation and squared-spatial tests, with no square roots. -/
90 def orientation (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ) (left : Bool) (t : ℝ) : ℝ :=
91   (F (lift left t)).1-kappa*denominator t
92 
93 def squareGap (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ) (left : Bool) (t : ℝ) : ℝ :=
94   (orientation F kappa left t)^2-(F (lift left t)).2.re^2-(F (lift left t)).2.im^2
95 
96 theorem chart_slack (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ)
97     (left : Bool) (t : ℝ) (hf : 0≤orientation F kappa left t)
98     (hh : 0≤squareGap F kappa left t) : kappa≤slack (F (1,chart left t)) := by
99   have hs : ‖(F (lift left t)).2‖^2≤(orientation F kappa left t)^2 := by
100     rw [← Complex.normSq_eq_norm_sq,Complex.normSq_apply]
101     unfold squareGap at hh
102     linarith
103   have hn : ‖(F (lift left t)).2‖≤orientation F kappa left t :=
104     (sq_le_sq₀ (norm_nonneg _) hf).mp hs
105   unfold orientation at hn
106   rw [lift_eq,map_smul] at hn
107   change ‖denominator t • (F (1,chart left t)).2‖≤
108     (denominator t • F (1,chart left t)).1-kappa*denominator t at hn
109   rw [norm_smul,Real.norm_eq_abs,abs_of_pos (denominator_pos t)] at hn
110   change kappa≤(F (1,chart left t)).1-‖(F (1,chart left t)).2‖
111   change denominator t*‖(F (1,chart left t)).2‖≤
112     denominator t*(F (1,chart left t)).1-kappa*denominator t at hn
113   nlinarith [denominator_pos t]
114 
115 /-- The superlevel is convex because output mass is affine and output norm is convex. -/
116 theorem convex_slack_superlevel (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ) :
117     Convex ℝ {v : ℂ | kappa≤slack (F (1,v))} := by
118   intro v hv w hw a b ha hb hab
119   have he : ((1 : ℝ),a • v+b • w)=(a : ℝ) • ((1 : ℝ),v)+b • ((1 : ℝ),w) := by
120     apply Prod.ext <;> simp [hab]
121   change kappa≤slack (F (1,a • v+b • w))
122   rw [he,map_add,map_smul,map_smul]
123   have hn := norm_add_le (a • (F (1,v)).2) (b • (F (1,w)).2)
124   rw [norm_smul,norm_smul,Real.norm_eq_abs,Real.norm_eq_abs,abs_of_nonneg ha,
125     abs_of_nonneg hb] at hn
126   change kappa≤(a*(F (1,v)).1+b*(F (1,w)).1)-‖a • (F (1,v)).2+b • (F (1,w)).2‖
127   dsimp [slack] at hv hw
128   have hk : a*kappa+b*kappa=kappa := by rw [← add_mul,hab,one_mul]
129   nlinarith [mul_nonneg ha (sub_nonneg.mpr hv),mul_nonneg hb (sub_nonneg.mpr hw)]
130 
131 /-- The circle inequalities extend to the full closed disk, not a sampled boundary. -/
132 theorem disk_slack_of_charts (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ)
133     (hf : ∀ left t,t∈Set.Icc (-1 : ℝ) 1 → 0≤orientation F kappa left t)
134     (hh : ∀ left t,t∈Set.Icc (-1 : ℝ) 1 → 0≤squareGap F kappa left t)
135     (v : ℂ) (hv : ‖v‖≤1) : kappa≤slack (F (1,v)) := by
136   have hs : Metric.sphere (0 : ℂ) 1⊆{v : ℂ | kappa≤slack (F (1,v))} := by
137     intro z hz
138     have hz1 : ‖z‖=1 := by simpa using hz
139     obtain ⟨left,t,ht,he⟩ := charts_cover z hz1
140     rw [← he]
141     exact chart_slack F kappa left t (hf left t ht) (hh left t ht)
142   have h := convexHull_min hs (convex_slack_superlevel F kappa)
143   rw [convexHull_sphere_eq_closedBall (0 : ℂ) (by norm_num : (0:ℝ)≤1)] at h
144   exact h (by simpa using hv)
145 
146 /-- P75's conclusion uses the actual attained minimum from P71. -/
147 theorem margin_of_charts (F : State ℂ →L[ℝ] State ℂ) (kappa : ℝ)
148     (hf : ∀ left t,t∈Set.Icc (-1 : ℝ) 1 → 0≤orientation F kappa left t)
149     (hh : ∀ left t,t∈Set.Icc (-1 : ℝ) 1 → 0≤squareGap F kappa left t) : kappa≤sigma F :=
150   (le_sigma_iff F kappa).mpr (disk_slack_of_charts F kappa hf hh)
151 
152 end
153 end Komorebi.LSM.RationalSemicircle

Back to source controls