RegularPolygon.lean

1 import KomorebiLSM.RegularPolygonAngles
2 import Mathlib.Analysis.InnerProductSpace.Dual
3 import Mathlib.Analysis.Convex.Topology
4 import Mathlib.Analysis.LocallyConvex.Separation
5 import Mathlib.Analysis.Complex.Basic
6 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
7 import Mathlib.Tactic
8 
9 set_option autoImplicit false
10 namespace Komorebi.LSM.RegularPolygon
11 
12 theorem ball_subset_convexHull_of_support (s : Set ℂ) (hs : s.Finite) (r : ℝ)
13     (hsupport : ∀ v : ℂ, ∃ p ∈ s, ‖v‖*r ≤ inner ℝ v p) :
14     {z : ℂ | ‖z‖≤r} ⊆ convexHull ℝ s := by
15   intro z hz
16   by_contra hnot
17   obtain ⟨f,u,hfu,huz⟩ := geometric_hahn_banach_closed_point
18     (convex_convexHull ℝ s) (hs.isCompact_convexHull ℝ).isClosed hnot
19   let v : ℂ := (InnerProductSpace.toDual ℝ ℂ).symm f
20   have hf (x : ℂ) : f x = inner ℝ v x :=
21     (InnerProductSpace.toDual_symm_apply (x:=x) (y:=f)).symm
22   obtain ⟨p,hp,hvp⟩ := hsupport v
23   have hp' := hfu p (subset_convexHull ℝ s hp)
24   have hz' : f z ≤ ‖v‖*r := by
25     rw [hf]
26     exact (real_inner_le_norm v z).trans (mul_le_mul_of_nonneg_left hz (norm_nonneg v))
27   rw [hf] at hp'
28   linarith
29 
30 theorem attenuation_cos_of_vertex_bound {η : ℝ} (hη : 0<η) {n : ℕ}
31     (hn : 0<n) (hbound : Real.pi/Real.sqrt (2*η) ≤ (n:ℝ)) :
32     1-η ≤ Real.cos (Real.pi/(n:ℝ)) := by
33   have hs : 0<Real.sqrt (2*η) := Real.sqrt_pos.2 (by positivity)
34   have hnR : (0:ℝ)<n := by exact_mod_cast hn
35   have hp : Real.pi ≤ (n:ℝ)*Real.sqrt (2*η) := (div_le_iff₀ hs).mp hbound
36   have hangle : Real.pi/(n:ℝ) ≤ Real.sqrt (2*η) :=
37     (div_le_iff₀ hnR).mpr (by simpa [mul_comm] using hp)
38   have hsq : (Real.pi/(n:ℝ))^2 ≤ 2*η := by
39     have h0 : 0≤Real.pi/(n:ℝ) := by positivity
40     have he := Real.sq_sqrt (by positivity : 0≤2*η)
41     nlinarith
42   have hc := Real.one_sub_sq_div_two_le_cos (x:=Real.pi/(n:ℝ))
43   linarith
44 
45 noncomputable def polygon (n : ℕ) : Set ℂ := convexHull ℝ (Set.range (vertex n))
46 
47 theorem polygon_closed (n : ℕ) : IsClosed (polygon n) :=
48   ((Set.finite_range (vertex n)).isCompact_convexHull ℝ).isClosed
49 
50 theorem polygon_convex (n : ℕ) : Convex ℝ (polygon n) := convex_convexHull ℝ _
51 
52 theorem closedBall_subset_polygon (n : ℕ) (hn : 3≤n) :
53     Metric.closedBall (0:ℂ) (Real.cos (Real.pi/(n:ℝ))) ⊆ polygon n := by
54   intro z hz
55   refine (ball_subset_convexHull_of_support (Set.range (vertex n)) (Set.finite_range _)
56     (Real.cos (Real.pi/(n:ℝ))) ?_) ?_
57   · intro v
58     obtain ⟨j,hj⟩ := support_lower n hn v
59     exact ⟨vertex n j,⟨j,rfl⟩,hj⟩
60   · change ‖z‖≤Real.cos (Real.pi/(n:ℝ))
61     simpa only [Metric.mem_closedBall,dist_zero_right] using hz
62 
63 theorem polygon_subset_closedBall (n : ℕ) : polygon n ⊆ Metric.closedBall (0:ℂ) 1 := by
64   apply convexHull_min ?_ (convex_closedBall (0:ℂ) 1)
65   rintro _ ⟨j,rfl⟩
66   simp only [Metric.mem_closedBall,dist_zero_right,vertex_norm,le_refl]
67 
68 theorem cos_radius_nonneg (n : ℕ) (hn : 3≤n) : 0≤Real.cos (Real.pi/(n:ℝ)) := by
69   have hnR : (3:ℝ)≤n := by exact_mod_cast hn
70   have hp : (0:ℝ)<n := by linarith
71   apply Real.cos_nonneg_of_mem_Icc
72   constructor
73   · have : 0≤Real.pi/(n:ℝ) := by positivity
74     linarith [Real.pi_pos]
75   · apply (div_le_iff₀ hp).mpr
76     nlinarith [Real.pi_pos]
77 
78 theorem zero_mem_polygon (n : ℕ) (hn : 3≤n) : (0:ℂ) ∈ polygon n :=
79   closedBall_subset_polygon n hn (by simpa using cos_radius_nonneg n hn)
80 
81 theorem one_mem_polygon (n : ℕ) (hn : 0<n) : (1:ℂ) ∈ polygon n := by
82   have he : vertex n ⟨0,hn⟩=(1:ℂ) := by simp [vertex]
83   rw [← he]
84   exact subset_convexHull ℝ _ ⟨_,rfl⟩
85 
86 theorem scaled_rotation_mem_polygon (n : ℕ) (hn : 3≤n) (q : Circle)
87     (α : ℝ) (hα : 0≤α) (hsmall : α≤Real.cos (Real.pi/(n:ℝ)))
88     (z : ℂ) (hz : z∈polygon n) : α • ((q:ℂ)*z) ∈ polygon n := by
89   apply closedBall_subset_polygon n hn
90   have hz1 : ‖z‖≤1 := by simpa only [Metric.mem_closedBall,dist_zero_right] using polygon_subset_closedBall n hz
91   simp only [Metric.mem_closedBall,dist_zero_right,norm_smul,Real.norm_eq_abs,abs_of_nonneg hα,norm_mul,Circle.norm_coe,one_mul]
92   exact (mul_le_of_le_one_right hα hz1).trans hsmall
93 
94 noncomputable def sufficientVertexCount (η : ℝ) : ℕ :=
95   max 3 ⌈Real.pi/Real.sqrt (2*η)⌉₊
96 
97 theorem sufficient_vertex_count (η : ℝ) (hη : 0<η) :
98     3≤sufficientVertexCount η ∧ 1-η ≤ Real.cos (Real.pi/(sufficientVertexCount η:ℝ)) := by
99   have hn : 3≤sufficientVertexCount η := le_max_left _ _
100   refine ⟨hn,attenuation_cos_of_vertex_bound hη (by omega) ?_⟩
101   exact (Nat.le_ceil _).trans (by exact_mod_cast (le_max_right 3 ⌈Real.pi/Real.sqrt (2*η)⌉₊))
102 
103 end Komorebi.LSM.RegularPolygon

Back to source controls