Transform.lean

/-
Copyright (c) 2025 Chris Birkbeck. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Birkbeck
-/

module

public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
public import Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

/-!
# Slash action on E2

## Overview

This file proves how the weight-2 Eisenstein series `E2` (and `G2`) transforms under the
slash action of `SL₂(ℤ)`. Unlike modular forms of weight `k ≥ 4`, the
functions `G2` and `E2` are **not** modular forms because they acquire a correction term under
the action of `S = [[0, -1], [1, 0]]`.

## Main Results

* **`G2_T_transform`**: `G2` is invariant under `T = [[1, 1], [0, 1]]`:
  `G₂|[2] T = G₂`


* **`G2_S_transform`**: The transformation under `S` involves a correction term:
  `G₂(z) = z⁻² G₂(-1/z) - 2πi/z`

  Equivalently: `G₂|[2] S = G₂ - D₂(S)`

* **`G2_slash_action`**: For any `γ ∈ SL₂(ℤ)`:
  `G₂|[2] γ = G₂ - D₂(γ)`

  where `D₂(γ)` is a correction term satisfying a cocycle condition.

* **`E2_slash_action`**: The normalized version:
  `E₂|[2] γ = E₂ - (1/(2ζ(2))) D₂(γ)`

## Proof Strategy

The proof of `G2_S_transform` is the heart of this file. The strategy is:

1. **Write as absolutely convergent series**: Express `G2` as an absolutely convergent double sum
   by adding and subtracting telescoping terms:
   `G₂(z) = 2ζ(2) + ∑' m n, 1/((mz+n)²(mz+n+1)) + δ(m,n)`
   where `δ` is a correction for boundary terms.

2. **Swapping summation order**: The S-action on `G2` corresponds to swapping the roles of
   `m` and `n`. After writing as an abs. conv. series, we can legitimately swap the order because
   the series is absolutely convergent.

3. **The correction term**: The difference between the two orderings of summation
   is precisely the term `-2πi/z`, which comes from the results in the Summable file
   (`tsum_symmetricIco_tsum_sub_eq` vs `tsum_tsum_symmetricIco_sub_eq`).

4. **General γ**: Since `SL₂(ℤ)` is generated by `S` and `T`, and we've
   computed the transformation under both generators, we can deduce the transformation under
   any element using the cocycle property of `D₂`.

## References
* P. Bruin and S. Dahmen, Modular Forms, https://www.few.vu.nl/~sdn249/modularforms16/notes.pdf

-/

open UpperHalfPlane hiding I

open ModularForm ModularGroup Filter Complex MatrixGroups Set SummationFilter

open scoped Real Topology

noncomputable section

namespace EisensteinSeries

/-- This is an auxiliary correction term for proving how E2 transforms. It allows us to work with
nicer indexing sets for our infinite sums. The key is the `aux_identity` below. -/
def δ (x : Fin 2 → ℤ) : ℂ := if x = ![0,0] then 1 else if x = ![0, -1] then 2 else 0

@[simp]
lemma δ_eq : δ ![0,0] = 1 := by simp [δ]

@[simp]
lemma δ_eq_two : δ ![0, -1] = 2 := by simp [δ]

lemma δ_eventually_cofinite : δ =ᶠ[cofinite] 0 := by
  filter_upwards [eventually_cofinite_ne ![0, 0], eventually_cofinite_ne ![0, -1]] with x hx hx'
  simp_all [δ]

/-- This term gives an alternative infinite sum for G2 which is absolutely convergent. -/
abbrev G2Term (z : ℍ) (m : Fin 2 → ℤ) : ℂ :=
    (((m 0 : ℂ) * z + m 1) ^ 2 * (m 0 * z + m 1 + 1))⁻¹ + δ m

lemma G2Term_summable (z : ℍ) : Summable (G2Term z) := by
  have H : Summable fun m ↦ G2Term z m - δ m := by
    simp_rw [G2Term, add_sub_cancel_right]
    apply summable_of_isBigO_rpow_norm (a := 3) (by linarith)
    simpa [pow_three, pow_two, ← mul_assoc] using ((isBigO_linear_add_const_vec z 0 1).mul
      (isBigO_linear_add_const_vec z 0 0)).mul (isBigO_linear_add_const_vec z 0 0)
  exact H.congr_cofinite <| δ_eventually_cofinite.mp <| .of_forall <| by simp +contextual

--This is the version we use the most.
lemma G2Term_prod_summable (z : ℍ) : Summable (fun p : ℤ × ℤ ↦ G2Term z ![p.1, p.2]) := by
  apply (finTwoArrowEquiv _).symm.summable_iff.mpr (G2Term_summable z)

lemma aux_identity (z : ℍ) (b n : ℤ) : ((b : ℂ) * z + n + 1)⁻¹ * (((b : ℂ) * z + n) ^ 2)⁻¹ +
    (δ ![b, n]) + (((b : ℂ) * z + n)⁻¹ - ((b : ℂ) * z + n + 1)⁻¹) = (((b : ℂ) * z + n) ^ 2)⁻¹ := by
  by_cases h : b = 0 ∧ n = 0
  · simp [h.1, h.2]
  · simp only [not_and] at h
    by_cases hb : b = 0
    · by_cases hn : n = -1
      · simp [hb,  hn, δ_eq_two]
        ring
      · have hn0 : (n : ℂ) ≠ 0 := by aesop
        have hn1 : (n : ℂ) + 1 ≠ 0 := by norm_cast; grind
        simp [δ, h, hb, hn]
        grind
    · have h0 : (b : ℂ) * z + n + 1 ≠ 0 := by
        simpa [add_assoc] using linear_ne_zero (cd := ![b, n + 1]) z (by aesop)
      have h1 : (b : ℂ) * z + n ≠ 0 := linear_ne_zero (cd := ![b, n]) z (by aesop)
      simp [δ]
      grind

/-- This shows `G2` can be defined as a certain absolutely convergent double sum. -/
lemma G2_eq_tsum_G2Term (z : ℍ) : G2 z = ∑' m, ∑' n, G2Term z ![m, n] := by
  set t := ∑' m, ∑' n, (G2Term z ![m, n])
  rw [G2, show t = t + 0 by ring, ← tsum_tsum_symmetricIco_sub_eq z, ← Summable.tsum_add]
  · rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]
    · congr with a
      rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]
      exact tsum_congr (fun b ↦ by simp [eisSummand, G2Term, aux_identity z a b, zpow_ofNat])
    · simpa only [tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z, add_zero]
        using (G2Term_prod_summable z).prod
  · exact (G2Term_prod_summable z).prod
  · exact summable_zero.congr
      fun b ↦ by simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

lemma G2_S_action_eq_tsum_G2Term (z : ℍ) : ((z : ℂ) ^ 2)⁻¹ * G2 (S • z) - -2 * π * I / z =
    ∑' n : ℤ, ∑' m : ℤ, G2Term z ![m, n] := by
  rw [← tsum_symmetricIco_tsum_sub_eq z, ← tsum_symmetricIco_tsum_eq_S_act z,
    ← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ), ← Summable.tsum_sub]
  · apply tsum_congr (fun N ↦ ?_)
    rw [← Summable.tsum_sub]
    · apply tsum_congr (fun M ↦ ?_)
      simp only [one_div, G2Term, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
        Matrix.cons_val_fin_one, mul_inv_rev]
      nth_rw 1 [← aux_identity z M N]
      ring
    · simpa using linear_left_summable (ne_zero z) N le_rfl
    · simpa [add_assoc] using summable_left_one_div_linear_sub_one_div_linear z N (N + 1)
  · apply HasSum.summable (a := (z.1 ^ 2)⁻¹ * G2 (S • z))
    rw [hasSum_symmetricIco_int_iff]
    apply (tendsto_double_sum_S_act z).congr (fun x ↦ ?_)
    rw [Summable.tsum_finsetSum (fun i hi ↦ ?_)]
    simpa using linear_left_summable (ne_zero z) i (k := 2) (by norm_num)
  · apply HasSum.summable (a := -2 * π * I / z)
    rw [hasSum_symmetricIco_int_iff, ← tendsto_comp_val_Ioi_atTop]
    exact tendsto_tsum_one_div_linear_sub_succ_eq z
  · have := G2Term_summable z
    rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at this
    exact this.prod

lemma tsum_G2Term_eq_tsum (z : ℍ) : ∑' (m : Fin 2 → ℤ), G2Term z m =
    ∑' m : ℤ, ∑' n : ℤ, G2Term z ![m, n] := by
  rw [← (finTwoArrowEquiv _).symm.tsum_eq]
  exact Summable.tsum_prod' (G2Term_prod_summable z) ((G2Term_prod_summable z).prod_factor)

lemma tsum_G2Term_eq_tsum' (z : ℍ) : ∑' (m : Fin 2 → ℤ), G2Term z m =
    ∑' n : ℤ, ∑' m : ℤ, G2Term z ![m, n] := by
  rw [Summable.tsum_comm', tsum_G2Term_eq_tsum]
  · exact G2Term_prod_summable z
  · exact (G2Term_prod_summable z).prod_factor
  · have H := G2Term_summable z
    rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at H
    exact H.prod_factor


@[expose] public section

section transform

/-- This is the key identity for how `G2` transforms under the slash action by `S`. -/
lemma G2_S_transform (z : ℍ) : G2 z = ((z : ℂ) ^ 2)⁻¹ * G2 (S • z) - -2 * π * I / z := by
  rw [G2_S_action_eq_tsum_G2Term, G2_eq_tsum_G2Term z , ← tsum_G2Term_eq_tsum',
  tsum_G2Term_eq_tsum]

lemma G2_T_transform : G2 ∣[(2 : ℤ)] T = G2 := by
  ext z
  simp_rw [SL_slash_def, modular_T_smul z]
  simp [G2_eq_tsum_cexp,  T, denom_apply,  ← exp_periodic.nat_mul 1 (2 * π * I * z)]
  grind

lemma G2_slash_action (γ : SL(2, ℤ)) : G2 ∣[(2 : ℤ)] γ = G2 - D2 γ := by
  have : γ ∈ Subgroup.closure {S, T} := by simp [SpecialLinearGroup.SL2Z_generators]
  induction this using Subgroup.closure_induction with
  | one => simp only [SlashAction.slash_one, D2_one, sub_zero]
  | mem g hg =>
      simp only [mem_insert_iff, mem_singleton_iff] at hg
      rcases hg with (h1 | h2)
      · ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop
      · simpa only [h2, D2_T, sub_zero] using G2_T_transform
  | mul g h _ _ ig ih =>
      rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
      grind [SlashAction.neg_slash, SL_slash]
  | inv g _ ig =>
      have H1 : (G2 ∣[(2 : ℤ)] g)∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g)∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]

lemma E2_slash_action (γ : SL(2, ℤ)) : E2 ∣[(2 : ℤ)] γ = E2 - (1 / (2 * riemannZeta 2)) • D2 γ := by
  ext z
  simp [E2, SL_smul_slash, G2_slash_action γ, mul_sub]

end transform

end

end EisensteinSeries