TangentBoundary.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ZeroMomentLogarithm
6 
7 namespace Komorebi.PaperIV
8 open Set
9 noncomputable section
10 
11 theorem canonicalSignedDenominator_one (z : ℂ) :
12     canonicalSignedDenominator 1 z = Complex.exp (-z) := by
13   have h := entireSigned_independent_roots (N := 1) (j := 0) (by omega) (by omega)
14     (canonicalPrimitiveRoot_isPrimitive (by omega)) IsPrimitiveRoot.one
15     (canonicalSignedRoot_pow (by omega)) (show (-1 : ℂ) ^ 1 = -1 by simp) z
16   change canonicalSignedDenominator 1 z = _ at h
17   simpa [entireSigned, entireTransfer] using h
18 
19 theorem analyticTransferTangent_one : analyticTransferTangent 1 = fun _ => 1 := by
20   have he : canonicalSignedDenominator 1 = fun z => Complex.exp (-z) :=
21     funext canonicalSignedDenominator_one
22   funext z
23   rw [analyticTransferTangent, he, logDeriv_apply]
24   have hd : HasDerivAt (fun w : ℂ => Complex.exp (-w)) (-Complex.exp (-z)) z := by
25     simpa only [id_eq, mul_neg, mul_one] using ((hasDerivAt_id z).fun_neg.cexp)
26   rw [hd.deriv]
27   simp [Complex.exp_ne_zero]
28 
29 theorem transferTangentCoeff_one_order (n : ℕ) :
30     transferTangentCoeff (R := ℂ) 1 n = if n = 0 then 1 else 0 := by
31   induction n using Nat.strong_induction_on with
32   | h n ih =>
33     by_cases hn : n = 0
34     · subst n
35       simp [transferTangentCoeff_zero 1 (by omega)]
36     · rw [transferTangentCoeff_recurrence 1 n (by omega)]
37       rw [Finset.sum_eq_single n]
38       · simp [transferTangentCoeff_zero 1 (by omega), hn]
39       · intro k hk hkn
40         obtain ⟨hk1, hkn1⟩ := Finset.mem_Ico.mp hk
41         have hlt : n - k < n := by omega
42         have hne : n - k ≠ 0 := by omega
43         simp [ih _ hlt, hne]
44       · intro hbad
45         exact (hbad (Finset.mem_Ico.mpr (by omega))).elim
46 
47 theorem analyticTransferTangent_one_hasSum (z : ℂ) :
48     HasSum (fun n => transferTangentCoeff (R := ℂ) 1 n /
49       ((1 * n + 1 - 1).factorial : ℂ) * z ^ (1 * n + 1 - 1))
50       (analyticTransferTangent 1 z) := by
51   simp only [analyticTransferTangent_one, transferTangentCoeff_one_order]
52   have h := hasSum_single (f := fun n : ℕ =>
53     (if n = 0 then (1 : ℂ) else 0) / ((1 * n + 1 - 1).factorial : ℂ) *
54       z ^ (1 * n + 1 - 1)) 0 (by intro n hn; simp [hn])
55   simpa using h
56 
57 /-- The actual tangent expansion, including the order-one boundary. -/
58 theorem analyticTransferTangent_hasSum_all_orders {N : ℕ} (hN : 0 < N) {R : ℝ}
59     (hn : ∀ w ∈ Metric.ball (0 : ℂ) R, entireReducedDenominator N w ≠ 0)
60     {z : ℂ} (hz : z ^ N ∈ Metric.ball (0 : ℂ) R) :
61     HasSum (fun n => transferTangentCoeff (R := ℂ) N n /
62       ((N * n + N - 1).factorial : ℂ) * z ^ (N * n + N - 1))
63       (analyticTransferTangent N z) := by
64   by_cases h : N = 1
65   · subst N
66     exact analyticTransferTangent_one_hasSum z
67   · exact analyticTransferTangent_coefficient_hasSum (by omega) hn hz
68 
69 end
70 end Komorebi.PaperIV

Back to source controls