PointwiseAddition.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.PointwiseFilters
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 
10 theorem pointwiseRootAverage_scaled_exp (N j : ℕ) (omega lambda z : ℂ) :
11     pointwiseRootAverage N j omega (fun t => Complex.exp (lambda * z * t)) 1 =
12       entireTransfer N j omega lambda z := by
13   unfold pointwiseRootAverage entireTransfer
14   congr 1
15   apply Finset.sum_congr rfl
16   intro l _
17   congr 2
18   ring
19 
20 theorem entireTransfer_addition {N k : ℕ} (hN : 0 < N) (hk : k < N)
21     {omega : ℂ} (ho : IsPrimitiveRoot omega N) (lambda z w : ℂ) :
22     entireTransfer N k omega lambda (z + w) =
23       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
24         if (i + j) % N = k then
25           entireTransfer N i omega lambda z * entireTransfer N j omega lambda w
26         else 0 := by
27   have h := pointwiseRootAverage_product hN ho k
28     (fun t => Complex.exp (lambda * z * t)) (fun t => Complex.exp (lambda * w * t)) 1
29   have he : (fun t => Complex.exp (lambda * z * t) * Complex.exp (lambda * w * t)) =
30       (fun t => Complex.exp (lambda * (z + w) * t)) := by
31     funext t
32     rw [← Complex.exp_add]
33     congr 1
34     ring
35   rw [he, pointwiseRootAverage_scaled_exp] at h
36   simpa only [pointwiseRootAverage_scaled_exp, Nat.mod_eq_of_lt hk] using h
37 
38 theorem signed_addition_weight {N : ℕ} (hN : 0 < N) {rho : ℂ}
39     (hr : rho ^ N = -1) (i j : ℕ) :
40     (rho ^ ((i + j) % N))⁻¹ =
41       (-1 : ℂ) ^ ((i + j) / N) * (rho ^ i)⁻¹ * (rho ^ j)⁻¹ := by
42   have hr0 : rho ≠ 0 := by intro h; simp [h, hN.ne'] at hr
43   have hp : rho ^ i * rho ^ j =
44       (-1 : ℂ) ^ ((i + j) / N) * rho ^ ((i + j) % N) := by
45     rw [← pow_add, ← hr, ← pow_mul, ← pow_add, Nat.div_add_mod]
46   field_simp
47   exact hp.trans (mul_comm _ _)
48 
49 theorem entireSigned_addition {N k : ℕ} (hN : 0 < N) (hk : k < N)
50     {omega rho : ℂ} (ho : IsPrimitiveRoot omega N) (hr : rho ^ N = -1)
51     (z w : ℂ) :
52     entireSigned N k omega rho (z + w) =
53       ∑ i ∈ Finset.range N, ∑ j ∈ Finset.range N,
54         if (i + j) % N = k then
55           (-1 : ℂ) ^ ((i + j) / N) * entireSigned N i omega rho z *
56             entireSigned N j omega rho w
57         else 0 := by
58   rw [entireSigned, entireTransfer_addition hN hk ho]
59   simp_rw [Finset.mul_sum]
60   apply Finset.sum_congr rfl
61   intro i _
62   apply Finset.sum_congr rfl
63   intro j _
64   split_ifs with h
65   · rw [← h, signed_addition_weight hN hr]
66     unfold entireSigned
67     ring
68   · simp
69 
70 end
71 end Komorebi.PaperIV

Back to source controls