SignedRealPhase.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.LargeZeroCompletion
6 import KomorebiPaperIV.AnalyticCycles
7 
8 namespace Komorebi.PaperIV
9 noncomputable section
10 
11 /-- All canonical signed sections commute with complex conjugation. -/
12 theorem entireSigned_canonical_conj {N j : ℕ} (hN : 0 < N) (hj : j < N) (z : ℂ) :
13     entireSigned N j (canonicalPrimitiveRoot N) (canonicalSignedRoot N) (star z) =
14       star (entireSigned N j (canonicalPrimitiveRoot N) (canonicalSignedRoot N) z) := by
15   have hs := (hasSum_entireSigned hN hj (canonicalPrimitiveRoot_isPrimitive hN)
16     (canonicalSignedRoot_pow hN) z).star
17   have ht := hasSum_entireSigned hN hj (canonicalPrimitiveRoot_isPrimitive hN)
18     (canonicalSignedRoot_pow hN) (star z)
19   apply ht.unique
20   convert hs using 1
21   funext n
22   by_cases h : n % N = j <;> simp [coeff_signedSection, signedSectionCoeff, h]
23 
24 theorem entireSigned_canonical_real {N j : ℕ} (hN : 0 < N) (hj : j < N) (x : ℝ) :
25     (entireSigned N j (canonicalPrimitiveRoot N) (canonicalSignedRoot N) (x : ℂ)).im = 0 := by
26   have h := congrArg Complex.im (entireSigned_canonical_conj hN hj (x : ℂ))
27   simp only [Complex.star_def, Complex.conj_ofReal, Complex.conj_im] at h
28   linarith
29 
30 theorem canonicalSignedDenominator_derivative_real {N : ℕ} (hN : 0 < N) (x : ℝ) :
31     (deriv (canonicalSignedDenominator N) (x : ℂ)).im = 0 := by
32   change (deriv (entireSigned N 0 (canonicalPrimitiveRoot N) (canonicalSignedRoot N)) (x : ℂ)).im = 0
33   rw [entireSigned_derivative_zero hN (canonicalPrimitiveRoot_isPrimitive hN) (canonicalSignedRoot_pow hN)]
34   simp only [Complex.neg_im, entireSigned_canonical_real hN (by omega : N - 1 < N), neg_zero]
35 
36 theorem signed_sine_mul_center {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
37     Real.sin (Real.pi / N) * signedZeroCenter N m = Real.pi * ((m : ℝ) + 1 / 2) := by
38   unfold signedZeroCenter
39   field_simp [(signed_sine_pos hN).ne']
40 
41 theorem signedZeroCenter_positive_phase {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
42     Complex.exp ((Real.sin (Real.pi / N) * signedZeroCenter N m : ℝ) * Complex.I) =
43       (-1 : ℂ) ^ m * Complex.I := by
44   rw [signed_sine_mul_center hN]
45   have he : ((Real.pi * ((m : ℝ) + 1 / 2) : ℝ) : ℂ) * Complex.I =
46       (m : ℂ) * ((Real.pi : ℂ) * Complex.I) + (Real.pi : ℂ) / 2 * Complex.I := by
47     push_cast
48     ring
49   rw [he, Complex.exp_add, Complex.exp_nat_mul, Complex.exp_pi_mul_I,
50     Complex.exp_pi_div_two_mul_I]
51 
52 theorem signedZeroCenter_negative_phase {N : ℕ} (hN : 2 ≤ N) (m : ℕ) :
53     Complex.exp ((-(Real.sin (Real.pi / N) * signedZeroCenter N m) : ℝ) * Complex.I) =
54       (-1 : ℂ) ^ m * (-Complex.I) := by
55   have h := congrArg star (signedZeroCenter_positive_phase hN m)
56   simpa only [map_mul, map_pow, map_neg, map_one, Complex.star_def, ← Complex.exp_conj,
57     Complex.conj_ofReal, Complex.conj_I, Complex.ofReal_neg,
58     neg_mul, mul_neg] using h
59 
60 def signedDerivativeScale (N : ℕ) (x : ℝ) : ℝ :=
61   (2 * Real.sin (Real.pi / N) / N) * Real.exp (Real.cos (Real.pi / N) * x)
62 
63 def signedDerivativeMainTerm (N m : ℕ) (x : ℝ) : ℝ :=
64   (-1 : ℝ) ^ (m + 1) * signedDerivativeScale N x
65 
66 theorem signedDerivativeScale_pos {N : ℕ} (hN : 2 ≤ N) (x : ℝ) :
67     0 < signedDerivativeScale N x :=
68   mul_pos (div_pos (mul_pos (by norm_num) (signed_sine_pos hN)) (by exact_mod_cast (show 0 < N by omega))) (Real.exp_pos _)
69 
70 theorem signedDerivativeMainTerm_ne_zero {N : ℕ} (hN : 2 ≤ N) (m : ℕ) (x : ℝ) :
71     signedDerivativeMainTerm N m x ≠ 0 :=
72   mul_ne_zero (pow_ne_zero _ (by norm_num)) (signedDerivativeScale_pos hN x).ne'
73 
74 /-- Exact phase decomposition of the leading derivative at every real point. -/
75 theorem signed_derivative_leading_phase {N : ℕ} (hN : 2 ≤ N) (m : ℕ) (x : ℝ) :
76     -signedZeroFrequency N / signedNormalizationFactor N (x : ℂ) =
77       (signedDerivativeMainTerm N m x : ℂ) *
78         Complex.exp ((-(Real.sin (Real.pi / N) * (x - signedZeroCenter N m)) : ℝ) * Complex.I) := by
79   have hn : (N : ℂ) ≠ 0 := by exact_mod_cast (show N ≠ 0 by omega)
80   have hv : canonicalSignedVertex N (N - 1) =
81       (Real.cos (Real.pi / N) : ℂ) - (Real.sin (Real.pi / N) : ℂ) * Complex.I := by
82     apply Complex.ext
83     · simp only [canonicalSignedVertex_last_re (show 0 < N by omega), Complex.sub_re,
84         Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.ofReal_im, Complex.I_im,
85         mul_zero, zero_mul, sub_zero]
86     · simp only [canonicalSignedVertex_last_im (show 0 < N by omega), Complex.sub_im,
87         Complex.ofReal_im, Complex.mul_im, Complex.I_im, Complex.I_re, Complex.ofReal_re,
88         mul_one, zero_mul, add_zero, zero_sub]
89   have he : canonicalSignedVertex N (N - 1) * (x : ℂ) =
90       ((Real.cos (Real.pi / N) * x : ℝ) : ℂ) +
91       ((-(Real.sin (Real.pi / N) * signedZeroCenter N m) : ℝ) : ℂ) * Complex.I +
92       ((-(Real.sin (Real.pi / N) * (x - signedZeroCenter N m)) : ℝ) : ℂ) * Complex.I := by
93     rw [hv]; push_cast; ring
94   rw [signedNormalizationFactor, Complex.exp_neg, div_mul_eq_div_div, div_inv_eq_mul,
95     he, Complex.exp_add, Complex.exp_add, signedZeroCenter_negative_phase hN,
96     ← Complex.ofReal_exp, signedZeroFrequency, canonicalSignedVertex_adjacent_difference (by omega),
97     signedDerivativeMainTerm, signedDerivativeScale]
98   push_cast
99   rw [pow_succ]
100   field_simp
101   ring_nf
102   simp [Complex.I_sq]
103 
104 end
105 end Komorebi.PaperIV

Back to source controls