refactor(SpecialFunctions/Gaussian): shorten long pole (#12104)

This splits up `Analysis/SpecialFunctions/Gaussian.lean` into three pieces, with the heaviest imports only needed in the later chunks. As only the first chunk is needed for many applications, including those on the critical path towards `NumberTheory/Cyclotomic/PID.lean`, this should improve overall build parallelism and shorten mathlib's overall compilation time.

Mathlib.lean

@@ -1028,7 +1028,9 @@ import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
 import Mathlib.Analysis.SpecialFunctions.Gamma.Beta
 import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
 import Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
-import Mathlib.Analysis.SpecialFunctions.Gaussian
+import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
+import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
+import Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
 import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Mathlib/Analysis/Fourier/Inversion.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.Analysis.SpecialFunctions.Gaussian
 import Mathlib.MeasureTheory.Integral.PeakFunction
+import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
 
 /-!
 # Fourier inversion formula

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
 import Mathlib.MeasureTheory.Integral.ExpDecay
-import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
 import Mathlib.Analysis.MellinTransform
 
 #align_import analysis.special_functions.gamma.basic from "leanprover-community/mathlib"@"cca40788df1b8755d5baf17ab2f27dacc2e17acb"

Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -7,6 +7,7 @@ import Mathlib.Analysis.Convolution
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
 import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
 import Mathlib.Analysis.Analytic.IsolatedZeros
+import Mathlib.Analysis.Complex.CauchyIntegral
 
 #align_import analysis.special_functions.gamma.beta from "leanprover-community/mathlib"@"a3209ddf94136d36e5e5c624b10b2a347cc9d090"
 

Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

@@ -3,8 +3,7 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
-import Mathlib.Analysis.SpecialFunctions.Gaussian
+import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
 
 #align_import analysis.special_functions.gamma.bohr_mollerup from "leanprover-community/mathlib"@"a3209ddf94136d36e5e5c624b10b2a347cc9d090"
 

Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean

@@ -0,0 +1,138 @@
+/-
+Copyright (c) 2023 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+
+import Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
+import Mathlib.Analysis.Fourier.PoissonSummation
+
+/-!
+# Poisson summation applied to the Gaussian
+
+In `Real.tsum_exp_neg_mul_int_sq` and `Complex.tsum_exp_neg_mul_int_sq`, we use Poisson summation
+to prove the identity
+
+`∑' (n : ℤ), exp (-π * a * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), exp (-π / a * n ^ 2)`
+
+for positive real `a`, or complex `a` with positive real part. (See also
+`NumberTheory.ModularForms.JacobiTheta`.)
+-/
+
+open Real Set MeasureTheory Filter Asymptotics intervalIntegral
+
+open scoped Real Topology FourierTransform RealInnerProductSpace BigOperators
+
+open Complex hiding exp continuous_exp abs_of_nonneg sq_abs
+
+noncomputable section
+
+section GaussianPoisson
+
+variable {E : Type*} [NormedAddCommGroup E]
+
+/-! First we show that Gaussian-type functions have rapid decay along `cocompact ℝ`. -/
+
+lemma rexp_neg_quadratic_isLittleO_rpow_atTop {a : ℝ} (ha : a < 0) (b s : ℝ) :
+    (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s) := by
+  suffices (fun x ↦ rexp (a * x ^ 2 + b * x)) =o[atTop] (fun x ↦ rexp (-x)) by
+    refine this.trans ?_
+    simpa only [neg_one_mul] using isLittleO_exp_neg_mul_rpow_atTop zero_lt_one s
+  rw [isLittleO_exp_comp_exp_comp]
+  have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
+    ext1 x; ring_nf
+  rw [this]
+  exact tendsto_id.atTop_mul_atTop <|
+    Filter.tendsto_atTop_add_const_right _ _ <| tendsto_id.const_mul_atTop (neg_pos.mpr ha)
+
+lemma cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
+    (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[atTop] (· ^ s) := by
+  apply Asymptotics.IsLittleO.of_norm_left
+  convert rexp_neg_quadratic_isLittleO_rpow_atTop ha b.re s with x
+  simp_rw [Complex.norm_eq_abs, Complex.abs_exp, add_re, ← ofReal_pow, mul_comm (_ : ℂ) ↑(_ : ℝ),
+      re_ofReal_mul, mul_comm _ (re _)]
+
+lemma cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) :
+    (fun x : ℝ ↦ cexp (a * x ^ 2 + b * x)) =o[cocompact ℝ] (|·| ^ s) := by
+  rw [cocompact_eq_atBot_atTop, isLittleO_sup]
+  constructor
+  · refine ((cexp_neg_quadratic_isLittleO_rpow_atTop ha (-b) s).comp_tendsto
+      Filter.tendsto_neg_atBot_atTop).congr' (eventually_of_forall fun x ↦ ?_) ?_
+    · simp only [neg_mul, Function.comp_apply, ofReal_neg, neg_sq, mul_neg, neg_neg]
+    · refine (eventually_lt_atBot 0).mp (eventually_of_forall fun x hx ↦ ?_)
+      simp only [Function.comp_apply, abs_of_neg hx]
+  · refine (cexp_neg_quadratic_isLittleO_rpow_atTop ha b s).congr' EventuallyEq.rfl ?_
+    refine (eventually_gt_atTop 0).mp (eventually_of_forall fun x hx ↦ ?_)
+    simp_rw [abs_of_pos hx]
+
+theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) :
+    Tendsto (fun x : ℝ => |x| ^ s * rexp (-a * x ^ 2)) (cocompact ℝ) (𝓝 0) := by
+  conv in rexp _ => rw [← sq_abs]
+  erw [cocompact_eq_atBot_atTop, ← comap_abs_atTop,
+    @tendsto_comap'_iff _ _ _ (fun y => y ^ s * rexp (-a * y ^ 2)) _ _ _
+      (mem_atTop_sets.mpr ⟨0, fun b hb => ⟨b, abs_of_nonneg hb⟩⟩)]
+  exact
+    (rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg ha s).tendsto_zero_of_tendsto
+      (tendsto_exp_atBot.comp <| tendsto_id.neg_const_mul_atTop (neg_lt_zero.mpr one_half_pos))
+#align tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact
+
+theorem isLittleO_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) :
+    (fun x : ℝ => Complex.exp (-a * x ^ 2)) =o[cocompact ℝ] fun x : ℝ => |x| ^ s := by
+  convert cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_ : (-a).re < 0) 0 s using 1
+  · simp_rw [zero_mul, add_zero]
+  · rwa [neg_re, neg_lt_zero]
+#align is_o_exp_neg_mul_sq_cocompact isLittleO_exp_neg_mul_sq_cocompact
+
+/-- Jacobi's theta-function transformation formula for the sum of `exp -Q(x)`, where `Q` is a
+negative definite quadratic form. -/
+theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
+    (∑' n : ℤ, cexp (-π * a * n ^ 2 + 2 * π * b * n)) =
+      1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n + I * b) ^ 2) := by
+  let f : ℝ → ℂ := fun x ↦ cexp (-π * a * x ^ 2 + 2 * π * b * x)
+  have hCf : Continuous f := by
+    refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
+    · exact continuous_const.mul (Complex.continuous_ofReal.pow 2)
+    · exact continuous_const.mul Complex.continuous_ofReal
+  have hFf : 𝓕 f = fun x : ℝ ↦ 1 / a ^ (1 / 2 : ℂ) * cexp (-π / a * (x + I * b) ^ 2) :=
+    fourierIntegral_gaussian_pi' ha b
+  have h1 : 0 < (↑π * a).re := by
+    rw [re_ofReal_mul]
+    exact mul_pos pi_pos ha
+  have h2 : 0 < (↑π / a).re := by
+    rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
+    refine' mul_pos pi_pos (div_pos ha <| normSq_pos.mpr _)
+    contrapose! ha
+    rw [ha, zero_re]
+  have f_bd : f =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
+    convert (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO
+    rwa [neg_mul, neg_re, neg_lt_zero]
+  have Ff_bd : (𝓕 f) =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) := by
+    rw [hFf]
+    have : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 =
+        -↑π / a * x ^ 2 + (-2 * π * I * b) / a * x + π * b ^ 2 / a := by
+      intro x; ring_nf; rw [I_sq]; ring
+    simp_rw [this]
+    conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
+    refine ((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact
+      (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left _).const_mul_left _
+    rwa [neg_div, neg_re, neg_lt_zero]
+  convert Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0 using 1
+  · simp only [f, zero_add, ofReal_int_cast]
+  · rw [← tsum_mul_left]
+    simp only [QuotientAddGroup.mk_zero, fourier_eval_zero, mul_one, hFf, ofReal_int_cast]
+
+theorem Complex.tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) :
+    (∑' n : ℤ, cexp (-π * a * (n : ℂ) ^ 2)) =
+      1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n : ℂ) ^ 2) := by
+  simpa only [mul_zero, zero_mul, add_zero] using Complex.tsum_exp_neg_quadratic ha 0
+#align complex.tsum_exp_neg_mul_int_sq Complex.tsum_exp_neg_mul_int_sq
+
+theorem Real.tsum_exp_neg_mul_int_sq {a : ℝ} (ha : 0 < a) :
+    (∑' n : ℤ, exp (-π * a * (n : ℝ) ^ 2)) =
+      (1 : ℝ) / a ^ (1 / 2 : ℝ) * (∑' n : ℤ, exp (-π / a * (n : ℝ) ^ 2)) := by
+  simpa only [← ofReal_inj, ofReal_tsum, ofReal_exp, ofReal_mul, ofReal_neg, ofReal_pow,
+    ofReal_int_cast, ofReal_div, ofReal_one, ofReal_cpow ha.le, ofReal_ofNat, mul_zero, zero_mul,
+    add_zero] using Complex.tsum_exp_neg_quadratic (by rwa [ofReal_re] : 0 < (a : ℂ).re) 0
+#align real.tsum_exp_neg_mul_int_sq Real.tsum_exp_neg_mul_int_sq
+
+end GaussianPoisson

Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean

@@ -5,7 +5,6 @@ Authors: David Loeffler
 -/
 
 import Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
-import Mathlib.Analysis.PSeries
 /-!
 # Dirichlet series as Mellin transforms
 

Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import Mathlib.Analysis.SpecialFunctions.Gaussian
+import Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation
 import Mathlib.Analysis.Calculus.SmoothSeries
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod
 

Mathlib/Probability/Distributions/Gaussian.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lorenzo Luccioli, Rémy Degenne, Alexander Bentkamp
 -/
-import Mathlib.Analysis.SpecialFunctions.Gaussian
+import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
 import Mathlib.Probability.Notation
 import Mathlib.MeasureTheory.Decomposition.Lebesgue