Gaussian identity and Fubini helpers for the logarithmic energy

• integral_gaussian_sub : ∫ x, exp (-b (x - c)²) = √(π/b);
• gaussian_conv : the completing-the-square identity ∫ u : ℂ, exp (-2s‖z-u‖²) exp (-2s‖w-u‖²) = π/(4s) exp (-s‖z-w‖²);
• intervalIntegral_swap_of_continuous : Fubini for interval integrals of continuous functions.

theorem Zeta5Irrational.integral_gaussian_sub {b : ℝ} (c : ℝ) : ∫ (x : ℝ), Real.exp (-b * (x - c) ^ 2) = √(Real.pi / b)

theorem Zeta5Irrational.integrable_gaussian_sub {b : ℝ} (hb : 0 < b) (c : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-b * (x - c) ^ 2)) MeasureTheory.volume

theorem Zeta5Irrational.sq_add_sq_eq (a b x : ℝ) : (a - x) ^ 2 + (b - x) ^ 2 = 2 * (x - (a + b) / 2) ^ 2 + (a - b) ^ 2 / 2

Completing the square in one variable.

theorem Zeta5Irrational.gaussian_conv_one (s a b : ℝ) : ∫ (x : ℝ), Real.exp (-(2 * s) * (a - x) ^ 2) * Real.exp (-(2 * s) * (b - x) ^ 2) = √(Real.pi / (4 * s)) * Real.exp (-s * (a - b) ^ 2)

theorem Zeta5Irrational.normSq_eq (z : ℂ) : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2

The norm squared on ℂ in terms of real and imaginary parts.

theorem Zeta5Irrational.gaussian_conv {s : ℝ} (hs : 0 < s) (z w : ℂ) : ∫ (u : ℂ), Real.exp (-(2 * s) * ‖z - u‖ ^ 2) * Real.exp (-(2 * s) * ‖w - u‖ ^ 2) = Real.pi / (4 * s) * Real.exp (-s * ‖z - w‖ ^ 2)

The completing-the-square identity on ℂ.

theorem Zeta5Irrational.intervalIntegral_swap_of_continuous {f : ℝ → ℝ → ℝ} (hf : Continuous (Function.uncurry f)) {a b c d : ℝ} (hab : a ≤ b) (hcd : c ≤ d) : ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, f x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, f x y

Fubini for interval integrals of a continuous function of two variables.