import Mathlib

open UpperHalfPlane Set
open scoped MatrixGroups Topology

noncomputable section

namespace ModularCurve.SmoothedFundamental

def mob (γ : SL(2, ℤ)) (z : ℂ) : ℂ := num γ z / denom γ z

theorem coe_smul (γ : SL(2, ℤ)) (τ : ℍ) : ((γ • τ : ℍ) : ℂ) = mob γ τ := by
  rw [ModularGroup.sl_moeb, coe_smul_of_det_pos (by simp)]; rfl

theorem mob_mob (γ γ' : SL(2, ℤ)) (τ : ℍ) : mob γ (mob γ' τ) = mob (γ * γ') τ := by
  rw [← coe_smul, ← coe_smul, ← coe_smul, mul_smul]

theorem mob_one_apply (z : ℂ) : mob 1 z = z := by
  simp [mob, num, denom]

def pOne (x : ℝ) : ℝ := Real.smoothTransition (x + 1) - Real.smoothTransition x

theorem pOne_nonneg (x : ℝ) : 0 ≤ pOne x :=
  sub_nonneg.2 (Real.smoothTransition.monotone (by linarith))

theorem pOne_le_one (x : ℝ) : pOne x ≤ 1 := by
  have := Real.smoothTransition.le_one (x + 1)
  have := Real.smoothTransition.nonneg x
  unfold pOne; linarith

theorem pOne_eq_zero_of_le {x : ℝ} (hx : x ≤ -1) : pOne x = 0 := by
  simp [pOne, Real.smoothTransition.zero_of_nonpos (show x + 1 ≤ 0 by linarith),
    Real.smoothTransition.zero_of_nonpos (show x ≤ 0 by linarith)]

theorem pOne_eq_zero_of_ge {x : ℝ} (hx : 1 ≤ x) : pOne x = 0 := by
  simp [pOne, Real.smoothTransition.one_of_one_le (show 1 ≤ x + 1 by linarith),
    Real.smoothTransition.one_of_one_le hx]

theorem mem_Ioo_of_pOne_ne_zero {x : ℝ} (hx : pOne x ≠ 0) : -1 < x ∧ x < 1 := by
  by_contra h
  rcases not_and_or.1 h with h | h <;> push Not at h
  exacts [hx (pOne_eq_zero_of_le h), hx (pOne_eq_zero_of_ge h)]

theorem pOne_sub_one_add {u : ℝ} (h0 : 0 ≤ u) (h1 : u ≤ 1) : pOne (u - 1) + pOne u = 1 := by
  unfold pOne
  rw [sub_add_cancel, Real.smoothTransition.zero_of_nonpos (by linarith : u - 1 ≤ 0),
    Real.smoothTransition.one_of_one_le (by linarith : 1 ≤ u + 1)]
  ring

def pTwo (T y : ℝ) : ℝ := Real.smoothTransition (8 * y - 5) * Real.smoothTransition (T + 4 - y)

theorem pTwo_nonneg (T y : ℝ) : 0 ≤ pTwo T y :=
  mul_nonneg (Real.smoothTransition.nonneg _) (Real.smoothTransition.nonneg _)

theorem pTwo_le_one (T y : ℝ) : pTwo T y ≤ 1 :=
  mul_le_one₀ (Real.smoothTransition.le_one _) (Real.smoothTransition.nonneg _)
    (Real.smoothTransition.le_one _)

theorem pTwo_eq_zero_of_le {T y : ℝ} (hy : y ≤ 5 / 8) : pTwo T y = 0 := by
  simp [pTwo, Real.smoothTransition.zero_of_nonpos (show 8 * y - 5 ≤ 0 by linarith)]

theorem pTwo_eq_zero_of_ge {T y : ℝ} (hy : T + 4 ≤ y) : pTwo T y = 0 := by
  simp [pTwo, Real.smoothTransition.zero_of_nonpos (show T + 4 - y ≤ 0 by linarith)]

theorem pTwo_eq_one {T y : ℝ} (h1 : 3 / 4 ≤ y) (h2 : y ≤ T + 3) : pTwo T y = 1 := by
  simp [pTwo, Real.smoothTransition.one_of_one_le (show 1 ≤ 8 * y - 5 by linarith),
    Real.smoothTransition.one_of_one_le (show 1 ≤ T + 4 - y by linarith)]

theorem mem_Ioo_of_pTwo_ne_zero {T y : ℝ} (h : pTwo T y ≠ 0) : 5 / 8 < y ∧ y < T + 4 := by
  by_contra h'
  rcases not_and_or.1 h' with h' | h' <;> push Not at h'
  exacts [h (pTwo_eq_zero_of_le h'), h (pTwo_eq_zero_of_ge h')]

def bump (T : ℝ) (z : ℂ) : ℝ := pOne z.re * pTwo T z.im

theorem bump_nonneg (T : ℝ) (z : ℂ) : 0 ≤ bump T z := mul_nonneg (pOne_nonneg _) (pTwo_nonneg _ _)

theorem bump_le_one (T : ℝ) (z : ℂ) : bump T z ≤ 1 :=
  mul_le_one₀ (pOne_le_one _) (pTwo_nonneg _ _) (pTwo_le_one _ _)

theorem mem_of_bump_ne_zero {T : ℝ} {z : ℂ} (h : bump T z ≠ 0) :
    (-1 < z.re ∧ z.re < 1) ∧ (5 / 8 < z.im ∧ z.im < T + 4) :=
  ⟨mem_Ioo_of_pOne_ne_zero (left_ne_zero_of_mul h),
    mem_Ioo_of_pTwo_ne_zero (right_ne_zero_of_mul h)⟩

theorem im_pos_of_bump_ne_zero {T : ℝ} {z : ℂ} (h : bump T z ≠ 0) : 0 < z.im := by
  have := (mem_of_bump_ne_zero h).2.1; linarith

def box (T : ℝ) : Set ℂ := Icc (-1 : ℝ) 1 ×ℂ Icc (5 / 8 : ℝ) (T + 4)

theorem isCompact_box (T : ℝ) : IsCompact (box T) := isCompact_Icc.reProdIm isCompact_Icc

theorem isClosed_box (T : ℝ) : IsClosed (box T) := isClosed_Icc.reProdIm isClosed_Icc

theorem im_pos_of_mem_box {T : ℝ} {z : ℂ} (hz : z ∈ box T) : 0 < z.im := by
  have := (Complex.mem_reProdIm.1 hz).2.1; linarith

theorem support_bump_subset (T : ℝ) : Function.support (bump T) ⊆ box T := by
  intro z hz
  obtain ⟨⟨h1, h2⟩, h3, h4⟩ := mem_of_bump_ne_zero hz
  exact Complex.mem_reProdIm.2 ⟨⟨h1.le, h2.le⟩, h3.le, h4.le⟩

theorem tsupport_bump_subset (T : ℝ) : tsupport (bump T) ⊆ box T :=
  closure_minimal (support_bump_subset T) (isClosed_box T)

def recip (t : ℝ) : ℝ := Real.smoothTransition (4 * t - 1) / t

theorem recip_nonneg {t : ℝ} (ht : 0 ≤ t) : 0 ≤ recip t :=
  div_nonneg (Real.smoothTransition.nonneg _) ht

theorem mul_recip_of_half_le {t : ℝ} (ht : 1 / 2 ≤ t) : t * recip t = 1 := by
  unfold recip
  rw [Real.smoothTransition.one_of_one_le (by linarith)]
  field_simp

theorem mul_recip_le_one (t : ℝ) : t * recip t ≤ 1 := by
  unfold recip
  by_cases ht : t = 0
  · simp [ht]
  · rw [mul_div_cancel₀ _ ht]; exact Real.smoothTransition.le_one _

def gcut (T : ℝ) (z : ℂ) : ℝ := 1 - Real.smoothTransition (z.im - T)

theorem gcut_eq_one {T : ℝ} {z : ℂ} (h : z.im ≤ T) : gcut T z = 1 := by
  simp [gcut, Real.smoothTransition.zero_of_nonpos (show z.im - T ≤ 0 by linarith)]

theorem gcut_eq_zero {T : ℝ} {z : ℂ} (h : T + 1 ≤ z.im) : gcut T z = 0 := by
  simp [gcut, Real.smoothTransition.one_of_one_le (show 1 ≤ z.im - T by linarith)]

theorem gcut_nonneg (T : ℝ) (z : ℂ) : 0 ≤ gcut T z :=
  sub_nonneg.2 (Real.smoothTransition.le_one _)

theorem gcut_le_one (T : ℝ) (z : ℂ) : gcut T z ≤ 1 :=
  sub_le_self _ (Real.smoothTransition.nonneg _)

def cover (T : ℝ) (z : ℂ) : ℝ := ∑ᶠ γ : SL(2, ℤ), bump T (mob γ z)

theorem cover_nonneg (T : ℝ) (z : ℂ) : 0 ≤ cover T z := finsum_nonneg fun _ => bump_nonneg _ _

def pu (T : ℝ) (z : ℂ) : ℝ := bump T z * recip (cover T z)

theorem pu_nonneg (T : ℝ) (z : ℂ) : 0 ≤ pu T z :=
  mul_nonneg (bump_nonneg _ _) (recip_nonneg (cover_nonneg _ _))

theorem support_pu_subset (T : ℝ) : Function.support (pu T) ⊆ Function.support (bump T) :=
  fun _ hz => left_ne_zero_of_mul hz

theorem tsupport_pu_subset (T : ℝ) : tsupport (pu T) ⊆ box T :=
  (closure_mono (support_pu_subset T)).trans (tsupport_bump_subset T)

def puCut (T : ℝ) (z : ℂ) : ℝ := pu T z * gcut T z

theorem puCut_nonneg (T : ℝ) (z : ℂ) : 0 ≤ puCut T z :=
  mul_nonneg (pu_nonneg _ _) (gcut_nonneg _ _)

theorem puCut_le_pu (T : ℝ) (z : ℂ) : puCut T z ≤ pu T z :=
  mul_le_of_le_one_right (pu_nonneg _ _) (gcut_le_one _ _)

theorem support_puCut_subset (T : ℝ) : Function.support (puCut T) ⊆ box T :=
  fun _ hz => support_bump_subset T (support_pu_subset T (left_ne_zero_of_mul hz))

theorem tsupport_puCut_subset (T : ℝ) : tsupport (puCut T) ⊆ box T :=
  closure_minimal (support_puCut_subset T) (isClosed_box T)

theorem puCut_eq_pu_of_im_le {T : ℝ} {z : ℂ} (h : z.im ≤ T) : puCut T z = pu T z := by
  rw [puCut, gcut_eq_one h, mul_one]

end ModularCurve.SmoothedFundamental

def ModularCurve.smoothedFundamental (Γ : Subgroup SL(2, ℤ)) (T : ℝ) (z : ℂ) : ℝ :=
  ∑ᶠ q : SL(2, ℤ) ⧸ Γ,
    ModularCurve.SmoothedFundamental.puCut T (ModularCurve.SmoothedFundamental.mob (Quotient.out q) z)

namespace ModularCurve.SmoothedFundamental

theorem smoothedFundamental_nonneg (Γ : Subgroup SL(2, ℤ)) (T : ℝ) (z : ℂ) :
    0 ≤ ModularCurve.smoothedFundamental Γ T z :=
  finsum_nonneg fun _ => puCut_nonneg _ _

theorem smoothedFundamental_eq_sum (Γ : Subgroup SL(2, ℤ)) [Fintype (SL(2, ℤ) ⧸ Γ)] (T : ℝ)
    (z : ℂ) : ModularCurve.smoothedFundamental Γ T z =
      ∑ q : SL(2, ℤ) ⧸ Γ, puCut T (mob (Quotient.out q) z) :=
  finsum_eq_sum_of_fintype _

end ModularCurve.SmoothedFundamental

end