LiPrincipal.lean

Declarations

Source

/-
NguyenRH1/LiPrincipal.lean — tier ii′ sub-stage ii′-1b(ii) (D-064 §4 R1):
the principal-part integral. For the explicit principal part
  P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i,   A_i = F^{(n+1−i)}(1)/(n+1−i)!,
with F(w) = (wⁿ−(w−1)ⁿ)·hLi(w), on any rectangle with 1 in its interior:
  RectangleIntegral' P z w = A_1 = ResW1 n.

Method: P = A_1/(w−1) + (Σ_{i≥2} A_i/(w−1)^i). The first term is handled
by the vendored `ResidueTheoremInRectangle`; the tail has the explicit
global primitive G(w) = −Σ_{i≥2} A_i/((i−1)(w−1)^{i−1}), differentiable
on the border (1 is interior, hence off the border), so its rectangle
integral vanishes by per-side FTC (`rectInt_deriv_eq_zero`).

Archive references: D-036, D-064 (R1), journal-016.
-/
import Mathlib
import Zeta23.FromPNTPlus.ResidueCalcOnRectangles
import NguyenRH1.LiResidue

open Zeta23 Complex Filter Topology

noncomputable section

namespace NguyenRH1

/-! ## 1. Additivity of the primed rectangle integral -/

lemma RectangleIntegral'_add (f g : ℂ → ℂ) (z w : ℂ)
    (hf : RectangleBorderIntegrable f z w) (hg : RectangleBorderIntegrable g z w) :
    RectangleIntegral' (f + g) z w = RectangleIntegral' f z w + RectangleIntegral' g z w := by
  rw [RectangleIntegral', RectangleBorderIntegrable.add hf hg, RectangleIntegral', RectangleIntegral',
    smul_add]

/-! ## 2. Parametrized side derivatives and integrability -/

lemma hasDerivAt_add_const_I (y : ℝ) (x : ℝ) :
    HasDerivAt (fun t : ℝ => t + y * I) 1 x := by
  have hof : HasDerivAt (fun t : ℝ => (t : ℂ)) 1 x := by
    have h := Complex.ofRealCLM.hasDerivAt (x := x)
    rw [Complex.ofRealCLM_apply] at h
    exact h
  have h := hof.add_const (y * I)
  simpa using h

lemma hasDerivAt_const_add_I (x y : ℝ) :
    HasDerivAt (fun t : ℝ => x + t * I) I y := by
  have hof : HasDerivAt (fun t : ℝ => (t : ℂ)) 1 y := by
    have h := Complex.ofRealCLM.hasDerivAt (x := y)
    rw [Complex.ofRealCLM_apply] at h
    exact h
  have h1 : HasDerivAt (fun t : ℝ => (t : ℂ) * I) I y := by
    have := hof.mul_const I
    simpa using this
  have h := HasDerivAt.const_add (↑x : ℂ) h1
  simpa using h

/-- FTC on a horizontal side: ∫_{x₁}^{x₂} (deriv G)(x + yI) dx
= G(x₂ + yI) − G(x₁ + yI). -/
lemma HIntegral_deriv {G : ℂ → ℂ} {z w : ℂ} (y : ℝ)
    (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)
    (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s)
    (hmap : Set.MapsTo (fun x : ℝ => ↑x + y * I) (Set.uIcc z.re w.re) (RectangleBorder z w)) :
    ∫ x in z.re..w.re, deriv G (x + y * I) = G (w.re + y * I) - G (z.re + y * I) := by
  have hd : ∀ x ∈ Set.uIcc z.re w.re,
      HasDerivAt (fun x : ℝ => G (x + y * I)) (deriv G (x + y * I)) x := by
    intro x hx
    have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=
      (hG _ (hmap hx)).hasDerivAt
    have h2 : HasDerivAt (fun x : ℝ => x + y * I) 1 x := hasDerivAt_add_const_I y x
    have hcomp := h1.comp x h2
    rw [mul_one] at hcomp
    exact hcomp
  have hint : IntervalIntegrable (fun x => deriv G (x + y * I)) MeasureTheory.volume z.re w.re := by
    apply ContinuousOn.intervalIntegrable
    have hcon : ContinuousOn (deriv G) (RectangleBorder z w) := by
      intro s hs
      exact (hGc s hs).continuousWithinAt
    have hpath : ContinuousOn (fun x : ℝ => x + y * I) (Set.uIcc z.re w.re) := by
      apply Continuous.continuousOn
      have hof : Continuous (fun t : ℝ => (t : ℂ)) := Complex.continuous_ofReal
      exact hof.add_const (y * I)
    exact hcon.comp hpath (by intro x hx; exact hmap hx)
  have hftc := intervalIntegral.integral_eq_sub_of_hasDerivAt
    (f := fun x : ℝ => G (x + y * I)) (f' := fun x : ℝ => deriv G (x + y * I)) hd hint
  simpa using hftc

/-- FTC on a vertical side: ∫_{y₁}^{y₂} (deriv G)(x + yI) dy
= −I·(G(x + y₂I) − G(x + y₁I)). -/
lemma VIntegral_deriv {G : ℂ → ℂ} {z w : ℂ} (x : ℝ)
    (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)
    (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s)
    (hmap : Set.MapsTo (fun y : ℝ => ↑x + ↑y * I) (Set.uIcc z.im w.im) (RectangleBorder z w)) :
    ∫ y in z.im..w.im, deriv G (x + y * I) =
      -I * (G (x + w.im * I) - G (x + z.im * I)) := by
  have hd : ∀ y ∈ Set.uIcc z.im w.im,
      HasDerivAt (fun y : ℝ => G (x + y * I)) (I * deriv G (x + y * I)) y := by
    intro y hy
    have h1 : HasDerivAt G (deriv G (x + y * I)) (x + y * I) :=
      (hG _ (hmap hy)).hasDerivAt
    have h2 : HasDerivAt (fun y : ℝ => x + y * I) I y := hasDerivAt_const_add_I x y
    have hcomp := h1.comp y h2
    rw [mul_comm] at hcomp
    exact hcomp
  have hint : IntervalIntegrable (fun y : ℝ => I * deriv G (x + y * I)) MeasureTheory.volume z.im w.im := by
    apply ContinuousOn.intervalIntegrable
    have hcon : ContinuousOn (deriv G) (RectangleBorder z w) := by
      intro s hs
      exact (hGc s hs).continuousWithinAt
    have hpath : ContinuousOn (fun y : ℝ => x + y * I) (Set.uIcc z.im w.im) := by
      apply Continuous.continuousOn
      have hof : Continuous (fun t : ℝ => (t : ℂ)) := Complex.continuous_ofReal
      have hmul : Continuous (fun t : ℝ => (t : ℂ) * I) := hof.mul_const I
      exact hmul.const_add x
    have hcomp : ContinuousOn (fun y : ℝ => I * deriv G (x + y * I)) (Set.uIcc z.im w.im) := by
      apply ContinuousOn.mul continuousOn_const
      exact hcon.comp hpath (by intro y hy; exact hmap hy)
    exact hcomp
  have hftc := intervalIntegral.integral_eq_sub_of_hasDerivAt
    (f := fun y : ℝ => G (x + y * I)) (f' := fun y : ℝ => I * deriv G (x + y * I)) hd hint
  have h6 : I * ∫ y in z.im..w.im, deriv G (x + y * I) =
      G (x + w.im * I) - G (x + z.im * I) := by
    have e := intervalIntegral.integral_smul (μ := MeasureTheory.volume) (r := I)
      (f := fun y : ℝ => deriv G (x + y * I)) (a := z.im) (b := w.im)
    simp only [smul_eq_mul] at e
    rw [← e]
    exact hftc
  have h7 : ∫ y in z.im..w.im, deriv G (x + y * I) =
      (G (x + w.im * I) - G (x + z.im * I)) / I :=
    eq_div_of_mul_eq Complex.I_ne_zero (by rw [mul_comm]; exact h6)
  rw [h7, div_eq_mul_inv, Complex.inv_I]
  ring

/-- If `G : ℂ → ℂ` is differentiable at every point of the rectangle
border, then the rectangle integral of `deriv G` vanishes (each side
telescopes by FTC). -/
lemma rectInt_deriv_eq_zero {G : ℂ → ℂ} {z w : ℂ}
    (hG : ∀ s ∈ RectangleBorder z w, DifferentiableAt ℂ G s)
    (hGc : ∀ s ∈ RectangleBorder z w, ContinuousAt (deriv G) s) :
    RectangleIntegral (fun s => deriv G s) z w = 0 := by
  rw [RectangleIntegral, HIntegral, HIntegral, VIntegral, VIntegral]
  rw [HIntegral_deriv z.im hG hGc (mapsTo_rectangleBorder_left_im z w),
    HIntegral_deriv w.im hG hGc (mapsTo_rectangleBorder_right_im z w)]
  have hVr := VIntegral_deriv w.re hG hGc (mapsTo_rectangleBorder_right_re z w)
  have hVl := VIntegral_deriv z.re hG hGc (mapsTo_rectangleBorder_left_re z w)
  rw [hVr, hVl]
  simp only [smul_eq_mul]
  have e : ∀ X : ℂ, I * (-I * X) = X := by
    intro X
    rw [← mul_assoc]
    have h : I * -I = 1 := by
      rw [mul_neg, Complex.I_mul_I]
      ring
    rw [h, one_mul]
  rw [e, e]
  ring

/-! ## 3. The principal part and its integral -/

/-- The principal-part coefficients: A_i = F^{(n+1−i)}(1)/(n+1−i)!,
F(w) = (wⁿ−(w−1)ⁿ)·hLi(w). -/
def Acoeff (n i : ℕ) : ℂ :=
  iteratedDeriv (n + 1 - i) (fun w : ℂ => (w ^ n - (w - 1) ^ n) * hLi w) 1 /
    Nat.factorial (n + 1 - i)

lemma Acoeff_one (n : ℕ) : Acoeff n 1 = ResW1 n := by
  simp only [Acoeff, ResW1, show n + 1 - 1 = n from by omega]

/-- The principal part of J at w = 1: P(w) = Σ_{i=1}^{n+1} A_i/(w−1)^i. -/
def ppart (n : ℕ) (w : ℂ) : ℂ :=
  ∑ i ∈ Finset.Icc 1 (n + 1), Acoeff n i / (w - 1) ^ i

/-- The tail primitive G(w) = −Σ_{i=2}^{n+1} (A_i/(i−1))·(w−1)^{−(i−1)}. -/
def Gprim (n : ℕ) (w : ℂ) : ℂ :=
  ∑ i ∈ Finset.Icc 2 (n + 1), -(Acoeff n i / ((i : ℂ) - 1)) * (w - 1) ^ (-((i : ℤ) - 1))

lemma Gprim_differentiableAt {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
    DifferentiableAt ℂ (Gprim n) w := by
  unfold Gprim
  rw [show (fun w : ℂ => ∑ i ∈ Finset.Icc 2 (n + 1),
      -(Acoeff n i / (↑i - 1)) * (w - 1) ^ (-((i : ℤ) - 1))) =
    ∑ i ∈ Finset.Icc 2 (n + 1),
      (fun w : ℂ => -(Acoeff n i / (↑i - 1)) * (w - 1) ^ (-((i : ℤ) - 1))) from by
    funext w
    simp [Finset.sum_apply]]
  apply DifferentiableAt.sum
  intro i hi
  apply DifferentiableAt.mul (differentiableAt_const _)
  have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw
  exact (((hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1)).differentiableAt).comp w
    (((hasDerivAt_id w).sub_const 1).differentiableAt))

lemma deriv_Gprim {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
    deriv (Gprim n) w = ∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i := by
  unfold Gprim
  rw [show (fun w : ℂ => ∑ i ∈ Finset.Icc 2 (n + 1),
      -(Acoeff n i / (↑i - 1)) * (w - 1) ^ (-((i : ℤ) - 1))) =
    ∑ i ∈ Finset.Icc 2 (n + 1),
      (fun w : ℂ => -(Acoeff n i / (↑i - 1)) * (w - 1) ^ (-((i : ℤ) - 1))) from by
    funext w
    simp [Finset.sum_apply]]
  rw [deriv_sum (fun i hi => ?_)]
  · apply Finset.sum_congr rfl
    intro i hi
    rw [Finset.mem_Icc] at hi
    have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw
    have hi1 : ((i : ℂ) - 1) ≠ 0 := by
      have : 1 < (i : ℝ) := by exact_mod_cast (by omega : 1 < i)
      intro heq
      rw [sub_eq_zero] at heq
      have : (i : ℝ) = 1 := by exact_mod_cast heq
      linarith
    have hd : deriv (fun w => (w - 1) ^ (-((i : ℤ) - 1))) w
        = ((-((i : ℤ) - 1) : ℤ) : ℂ) * (w - 1) ^ (-((i : ℤ) - 1) - 1) := by
      have h2 : HasDerivAt (fun x : ℂ => x ^ (-((i : ℤ) - 1)))
          (((-((i : ℤ) - 1) : ℤ) : ℂ) * (w - 1) ^ (-((i : ℤ) - 1) - 1)) (w - 1) :=
        hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1)
      have h3 : HasDerivAt (fun w : ℂ => w - 1) 1 w := by
        simpa using (hasDerivAt_id w).sub_const 1
      have hcomp := h2.comp w h3
      rw [mul_one] at hcomp
      exact hcomp.deriv
    rw [deriv_const_mul _ (by
      have hw1' : w - 1 ≠ 0 := sub_ne_zero.mpr hw
      exact (((hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1')).differentiableAt).comp w
        (((hasDerivAt_id w).sub_const 1).differentiableAt))), hd]
    have hm : (-((i : ℤ) - 1) - 1 : ℤ) = -(i : ℤ) := by omega
    rw [hm]
    push_cast
    field_simp [hw1, hi1]
    rw [zpow_neg, zpow_natCast]
    field_simp [hw1]
  · apply DifferentiableAt.mul (differentiableAt_const _)
    have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw
    exact (((hasDerivAt_zpow (-((i : ℤ) - 1)) (w - 1) (Or.inl hw1)).differentiableAt).comp w
      (((hasDerivAt_id w).sub_const 1).differentiableAt))

lemma tail_continuousAt {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
    ContinuousAt (fun w => ∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i) w := by
  have hterm : ∀ i : ℕ, ContinuousAt (fun w => Acoeff n i / (w - 1) ^ i) w := by
    intro i
    have hw1 : w - 1 ≠ 0 := sub_ne_zero.mpr hw
    have hnum : ContinuousAt (fun w => Acoeff n i) w := continuousAt_const
    have hden : ContinuousAt (fun w => (w - 1) ^ i) w :=
      (continuousAt_id.sub continuousAt_const).pow _
    exact hnum.div hden (pow_ne_zero _ hw1)
  have : ∀ s : Finset ℕ, ContinuousAt (fun w => ∑ i ∈ s, Acoeff n i / (w - 1) ^ i) w := by
    intro s
    induction s using Finset.induction with
    | empty => exact continuousAt_const
    | insert a s has hs =>
      simp_rw [Finset.sum_insert has]
      exact ContinuousAt.add (hterm a) hs
  exact this _

lemma ppart_eq_deriv_add {n : ℕ} {w : ℂ} (hw : w ≠ 1) :
    ppart n w = Acoeff n 1 / (w - 1) + deriv (Gprim n) w := by
  rw [ppart, deriv_Gprim hw]
  have hsplit : Finset.Icc 1 (n + 1) = {1} ∪ Finset.Icc 2 (n + 1) := by
    ext j
    simp [Finset.mem_Icc]
    omega
  rw [hsplit, Finset.sum_union (by simp)]
  simp [pow_one]

/-- The principal-part integral: on any rectangle with 1 in its interior,
RectangleIntegral' (ppart n) z w = ResW1 n. -/
theorem rectInt'_ppart {n : ℕ} {z w : ℂ}
    (hre : z.re ≤ w.re) (him : z.im ≤ w.im) (h1 : Rectangle z w ∈ 𝓝 (1 : ℂ)) :
    RectangleIntegral' (ppart n) z w = ResW1 n := by
  have h1not : (1 : ℂ) ∉ RectangleBorder z w := not_mem_rectangleBorder_of_rectangle_mem_nhds h1
  have hdecomp : Set.EqOn (ppart n) (fun w => Acoeff n 1 / (w - 1) + deriv (Gprim n) w)
      (RectangleBorder z w) := by
    intro s hs
    have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)
    exact ppart_eq_deriv_add hs1
  rw [RectangleIntegral'_congr hdecomp]
  rw [show (fun w => Acoeff n 1 / (w - 1) + deriv (Gprim n) w) =
    (fun w => Acoeff n 1 / (w - 1)) + deriv (Gprim n) from by
    funext w; simp [Pi.add_apply]]
  have hAint : RectangleBorderIntegrable (fun w => Acoeff n 1 / (w - 1)) z w := by
    apply HolomorphicOn.rectangleBorderIntegrable' _ h1
    intro s hs
    have hs1 : s ≠ 1 := hs.2
    exact (((differentiableAt_const (Acoeff n 1)).div
      ((differentiableAt_id.sub (differentiableAt_const 1)))
      (sub_ne_zero.mpr hs1))).differentiableWithinAt
  have hGint : RectangleBorderIntegrable (deriv (Gprim n)) z w := by
    apply HolomorphicOn.rectangleBorderIntegrable' _ h1
    have hopen : DifferentiableOn ℂ (deriv (Gprim n)) {1}ᶜ := by
      have hd : DifferentiableOn ℂ (Gprim n) {1}ᶜ := by
        intro s hs
        exact (Gprim_differentiableAt (Set.mem_compl_singleton_iff.mp hs)).differentiableWithinAt
      exact hd.deriv isOpen_compl_singleton
    exact hopen.mono (by intro s hs; exact hs.2)
  rw [RectangleIntegral'_add _ _ _ _ hAint hGint]
  rw [ResidueTheoremInRectangle hre him h1]
  have hzero : RectangleIntegral (deriv (Gprim n)) z w = 0 := by
    apply rectInt_deriv_eq_zero
    · intro s hs
      have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)
      exact Gprim_differentiableAt hs1
    · intro s hs
      have hs1 : s ≠ 1 := fun heq => h1not (heq ▸ hs)
      have hev : (fun w => ∑ i ∈ Finset.Icc 2 (n + 1), Acoeff n i / (w - 1) ^ i) =ᶠ[𝓝 s]
          deriv (Gprim n) := by
        filter_upwards [isOpen_compl_singleton.eventually_mem hs1] with w hw
        exact (deriv_Gprim (Set.mem_compl_singleton_iff.mp hw)).symm
      exact (tail_continuousAt hs1).congr hev
  rw [RectangleIntegral', hzero]
  rw [Acoeff_one]
  simp

end NguyenRH1