RegularPolygonAngles.lean

1 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
2 import Mathlib.Algebra.Order.Round
3 import Mathlib.Tactic
4 
5 /-! Exact vertices, angle rounding and directional support of a regular polygon. -/
6 set_option autoImplicit false
7 namespace Komorebi.LSM.RegularPolygon
8 open scoped ComplexConjugate RealInnerProductSpace
9 open Set
10 
11 noncomputable def vertex (n : ℕ) (j : Fin n) : ℂ :=
12   Circle.exp (2*Real.pi*(j:ℝ)/(n:ℝ))
13 
14 theorem vertex_norm (n : ℕ) (j : Fin n) : ‖vertex n j‖=1 := Circle.norm_coe _
15 
16 /-- Every integer-indexed vertex equals a member of the actual finite vertex family. -/
17 theorem int_vertex_mem {n : ℕ} (hn : 0<n) (k : ℤ) :
18     (Circle.exp (2*Real.pi*(k:ℝ)/(n:ℝ)) : ℂ) ∈ range (vertex n) := by
19   have hnZ : (0:ℤ)<n := by exact_mod_cast hn
20   have hnR : (n:ℝ) ≠ 0 := by exact_mod_cast Nat.ne_of_gt hn
21   have hnonneg : 0 ≤ k % (n:ℤ) := Int.emod_nonneg k (ne_of_gt hnZ)
22   have hlt : (k % (n:ℤ)).toNat < n := by
23     have h : (k % (n:ℤ)).toNat < (n:ℤ) := by
24       rw [Int.toNat_of_nonneg hnonneg]
25       exact Int.emod_lt_of_pos k hnZ
26     exact_mod_cast h
27   let j : Fin n := ⟨(k % (n:ℤ)).toNat,hlt⟩
28   have hjZ : ((j:ℕ):ℤ) = k % (n:ℤ) := Int.toNat_of_nonneg hnonneg
29   have hj := congrArg (Int.castRingHom ℝ) hjZ
30   simp only [Int.coe_castRingHom, Int.cast_natCast] at hj
31   refine ⟨j, ?_⟩
32   change (Circle.exp (2*Real.pi*(j:ℝ)/(n:ℝ)) : ℂ) = _
33   apply congrArg (fun u : Circle => (u:ℂ))
34   apply Circle.exp_eq_exp.mpr
35   refine ⟨-(k/(n:ℤ)), ?_⟩
36   have he := Int.emod_add_mul_ediv k (n:ℤ)
37   have her := congrArg (Int.castRingHom ℝ) he
38   simp only [map_add, map_mul, Int.coe_castRingHom, Int.cast_natCast] at her
39   rw [hj]
40   simp only [Int.cast_neg]
41   field_simp [hnR]
42   linear_combination her
43 
44 /-- Some vertex angle is at angular distance at most `pi/n` from any real angle. -/
45 theorem nearest_angle {n : ℕ} (hn : 0<n) (θ : ℝ) :
46     ∃ k : ℤ, |2*Real.pi*(k:ℝ)/(n:ℝ)-θ| ≤ Real.pi/(n:ℝ) := by
47   let k : ℤ := round ((n:ℝ)*θ/(2*Real.pi))
48   refine ⟨k, ?_⟩
49   have hr := abs_sub_round ((n:ℝ)*θ/(2*Real.pi))
50   have hnR : (0:ℝ)<n := by exact_mod_cast hn
51   have hp : (0:ℝ)<2*Real.pi := by positivity
52   have he : 2*Real.pi*(k:ℝ)/(n:ℝ)-θ =
53       -(2*Real.pi/(n:ℝ))*((n:ℝ)*θ/(2*Real.pi)-(k:ℝ)) := by
54     field_simp [ne_of_gt hnR, Real.pi_ne_zero]
55     ring
56   rw [he, abs_mul, abs_neg, abs_of_pos (div_pos hp hnR)]
57   calc
58     _ ≤ (2*Real.pi/(n:ℝ))*(1/2) := mul_le_mul_of_nonneg_left hr (by positivity)
59     _ = _ := by ring
60 
61 /-- Directional support of a unit complex exponential, including the zero vector. -/
62 theorem inner_exp (v : ℂ) (θ : ℝ) :
63     inner ℝ v (Circle.exp θ : ℂ) = ‖v‖*Real.cos (θ-Complex.arg v) := by
64   have hr := Complex.norm_mul_cos_arg v
65   have hi := Complex.norm_mul_sin_arg v
66   rw [Complex.inner]
67   have he : ((Circle.exp θ : ℂ)*conj v).re = Real.cos θ*v.re+Real.sin θ*v.im := by
68     simp [Circle.coe_exp, Complex.exp_mul_I, Complex.mul_re,
69       ← Complex.ofReal_cos, ← Complex.ofReal_sin]
70   rw [he,Real.cos_sub,←hr,←hi]
71   ring
72 
73 /-- Every linear direction has support at least `norm(v)*cos(pi/n)`
74 on an actual vertex of the finite regular polygon. -/
75 theorem support_lower (n : ℕ) (hn : 3≤n) (v : ℂ) :
76     ∃ j : Fin n, ‖v‖*Real.cos (Real.pi/(n:ℝ)) ≤ inner ℝ v (vertex n j) := by
77   have hn0 : 0<n := by omega
78   have hn1 : (1:ℝ)≤n := by exact_mod_cast (by omega : 1≤n)
79   obtain ⟨k,hk⟩ := nearest_angle hn0 (Complex.arg v)
80   obtain ⟨j,hj⟩ := int_vertex_mem hn0 k
81   refine ⟨j, ?_⟩
82   rw [hj, inner_exp]
83   have hπ : Real.pi/(n:ℝ) ≤ Real.pi := div_le_self Real.pi_nonneg hn1
84   have hc : Real.cos (Real.pi/(n:ℝ)) ≤
85       Real.cos (2*Real.pi*(k:ℝ)/(n:ℝ)-Complex.arg v) := by
86     simpa only [Real.cos_abs] using
87       Real.cos_le_cos_of_nonneg_of_le_pi
88         (abs_nonneg (2*Real.pi*(k:ℝ)/(n:ℝ)-Complex.arg v)) hπ hk
89   exact mul_le_mul_of_nonneg_left hc (norm_nonneg v)
90 
91 end Komorebi.LSM.RegularPolygon

Back to source controls