Lemma 6.2 (zero-mass logarithmic energy) for the truncated kernel

We work with explicit "atoms": a finite family of continuous curves γ k : ℝ → ℂ (parametrised over [0, 2π]) with real weights s k. The double integral of a kernel f against the atoms k, l is pairInt γ f k l, and the energy is energy s γ f = ∑ k l, s k * s l * pairInt γ f k l.

For the truncated kernel Ltr a b r = (1/2) ∫_a^b (e^{-s} - e^{-s r²})/s ds and zero total mass ∑ s k = 0, the energy is nonpositive (energy_Ltr_nonpos): this is the Gaussian positivity argument of the paper.

noncomputable def Zeta5Irrational.Ltr (a b r : ℝ) : ℝ

The truncated logarithmic kernel L_{a,b}(r).

Equations

• Zeta5Irrational.Ltr a b r = 1 / 2 * ∫ (s : ℝ) in a..b, (Real.exp (-s) - Real.exp (-s * r ^ 2)) / s

noncomputable def Zeta5Irrational.pairInt {ι : Type u_1} (γ : ι → ℝ → ℂ) (f : ℂ → ℂ → ℝ) (k l : ι) : ℝ

Double integral of a kernel against two atoms.

Equations

• Zeta5Irrational.pairInt γ f k l = ∫ (θ : ℝ) (φ : ℝ) in 0..2 * Real.pi, f (γ k θ) (γ l φ)

noncomputable def Zeta5Irrational.energy {ι : Type u_1} [Fintype ι] (s : ι → ℝ) (γ : ι → ℝ → ℂ) (f : ℂ → ℂ → ℝ) : ℝ

The energy of the signed combination of atoms.

Equations

• Zeta5Irrational.energy s γ f = ∑ k : ι, ∑ l : ι, s k * s l * Zeta5Irrational.pairInt γ f k l

noncomputable def Zeta5Irrational.Gk {ι : Type u_1} (γ : ι → ℝ → ℂ) (t : ℝ) (k l : ι) : ℝ

Gaussian pair integral.

Equations

• Zeta5Irrational.Gk γ t k l = ∫ (θ : ℝ) (φ : ℝ) in 0..2 * Real.pi, Real.exp (-t * ‖γ k θ - γ l φ‖ ^ 2)

noncomputable def Zeta5Irrational.gk {ι : Type u_1} (γ : ι → ℝ → ℂ) (t : ℝ) (k : ι) (u : ℂ) : ℝ

Gaussian smoothing of one atom.

Equations

• Zeta5Irrational.gk γ t k u = ∫ (θ : ℝ) in 0..2 * Real.pi, Real.exp (-(2 * t) * ‖γ k θ - u‖ ^ 2)

theorem Zeta5Irrational.sq_sub_comm' (a b : ℝ) : (a - b) ^ 2 = (b - a) ^ 2

theorem Zeta5Irrational.integrable_gaussC {c : ℝ} (hc : 0 < c) (z : ℂ) : MeasureTheory.Integrable (fun (u : ℂ) => Real.exp (-c * ‖z - u‖ ^ 2)) MeasureTheory.volume

Integrability of a Gaussian on ℂ.

theorem Zeta5Irrational.exp_gauss_le {t R : ℝ} (ht : 0 ≤ t) {γ u : ℂ} (hγ : ‖γ‖ ≤ R) : Real.exp (-(2 * t) * ‖γ - u‖ ^ 2) ≤ Real.exp (2 * t * R ^ 2) * Real.exp (-t * ‖u‖ ^ 2)

‖γ - u‖² ≥ ‖u‖²/2 - ‖γ‖², in exponential form.

theorem Zeta5Irrational.swap_interval_complex {F : ℝ → ℂ → ℝ} (hF : Continuous (Function.uncurry F)) {c C : ℝ} (hc : 0 < c) {a b : ℝ} (hab : a ≤ b) (hbound : ∀ θ ∈ Set.Icc a b, ∀ (u : ℂ), |F θ u| ≤ C * Real.exp (-c * ‖u‖ ^ 2)) : ∫ (θ : ℝ) in a..b, ∫ (u : ℂ), F θ u = ∫ (u : ℂ), ∫ (θ : ℝ) in a..b, F θ u

Fubini between an interval integral and an integral over ℂ, for a continuous integrand with a Gaussian bound in the complex variable.

theorem Zeta5Irrational.gk_nonneg {ι : Type u_1} (γ : ι → ℝ → ℂ) (t : ℝ) (k : ι) (u : ℂ) : 0 ≤ gk γ t k u

theorem Zeta5Irrational.continuous_gk {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) (t : ℝ) (k : ι) : Continuous (gk γ t k)

theorem Zeta5Irrational.gk_le_two_pi {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {t : ℝ} (ht : 0 ≤ t) (k : ι) (u : ℂ) : gk γ t k u ≤ 2 * Real.pi

theorem Zeta5Irrational.gk_le {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {R : ℝ} (hR : ∀ (k : ι) (θ : ℝ), ‖γ k θ‖ ≤ R) {t : ℝ} (ht : 0 ≤ t) (k : ι) (u : ℂ) : gk γ t k u ≤ 2 * Real.pi * Real.exp (2 * t * R ^ 2) * Real.exp (-t * ‖u‖ ^ 2)

theorem Zeta5Irrational.Gk_eq {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {R : ℝ} (hR : ∀ (k : ι) (θ : ℝ), ‖γ k θ‖ ≤ R) {t : ℝ} (ht : 0 < t) (k l : ι) : Gk γ t k l = 4 * t / Real.pi * ∫ (u : ℂ), gk γ t k u * gk γ t l u

The Gaussian pair integral as an integral over ℂ of a product of smoothed atoms.

theorem Zeta5Irrational.gaussian_energy_nonneg {ι : Type u_1} [Fintype ι] {s : ι → ℝ} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {R : ℝ} (hR : ∀ (k : ι) (θ : ℝ), ‖γ k θ‖ ≤ R) {t : ℝ} (ht : 0 < t) : 0 ≤ ∑ k : ι, ∑ l : ι, s k * s l * Gk γ t k l

The Gaussian energy is nonnegative.

The truncated kernel

theorem Zeta5Irrational.continuous_inv_max {a : ℝ} (ha : 0 < a) : Continuous fun (s : ℝ) => (max s a)⁻¹

theorem Zeta5Irrational.Ltr_eq_max {a b : ℝ} (_ha : 0 < a) (hab : a ≤ b) (r : ℝ) : Ltr a b r = 1 / 2 * ∫ (s : ℝ) in a..b, (Real.exp (-s) - Real.exp (-s * r ^ 2)) * (max s a)⁻¹

theorem Zeta5Irrational.continuous_Gk {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) (k l : ι) : Continuous fun (t : ℝ) => Gk γ t k l

Continuity of the Gaussian pair integral in the parameter.

theorem Zeta5Irrational.pairInt_Ltr {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (k l : ι) : pairInt γ (fun (z w : ℂ) => Ltr a b ‖z - w‖) k l = 1 / 2 * ∫ (s : ℝ) in a..b, (Real.exp (-s) * (2 * Real.pi) ^ 2 - Gk γ s k l) / s

The truncated-kernel pair integral in terms of Gaussian pair integrals.

theorem Zeta5Irrational.energy_Ltr_nonpos {ι : Type u_1} [Fintype ι] {s : ι → ℝ} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {R : ℝ} (hR : ∀ (k : ι) (θ : ℝ), ‖γ k θ‖ ≤ R) (hmass : ∑ k : ι, s k = 0) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : (energy s γ fun (z w : ℂ) => Ltr a b ‖z - w‖) ≤ 0

Lemma 6.2 for the truncated kernel: the energy of a zero-mass combination of atoms with respect to L_{a,b} is nonpositive.