Lemma 6.2 for the logarithmic kernel

Passing to the limit a → 0, b → ∞ in energy_Ltr_nonpos by dominated convergence. The hypotheses are integrability of log ‖γ k θ - γ l φ‖ on the torus and the a.e. distinctness γ k θ ≠ γ l φ.

@[reducible, inline]

noncomputable abbrev Zeta5Irrational.μcirc : MeasureTheory.Measure ℝ

The measure on [0, 2π].

Equations

• Zeta5Irrational.μcirc = MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))

theorem Zeta5Irrational.pairInt_eq_prod {ι : Type u_1} (γ : ι → ℝ → ℂ) (f : ℂ → ℂ → ℝ) (k l : ι) (hf : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => f (γ k p.1) (γ l p.2)) (μcirc.prod μcirc)) : pairInt γ f k l = ∫ (p : ℝ × ℝ), f (γ k p.1) (γ l p.2) ∂μcirc.prod μcirc

pairInt as an integral over the product measure.

theorem Zeta5Irrational.integrable_of_continuous_torus {F : ℝ × ℝ → ℝ} (hF : Continuous F) : MeasureTheory.Integrable F (μcirc.prod μcirc)

theorem Zeta5Irrational.tendsto_pairInt_Ltr {ι : Type u_1} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) (k l : ι) (hint : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => Real.log ‖γ k p.1 - γ l p.2‖) (μcirc.prod μcirc)) (hae : ∀ᵐ (p : ℝ × ℝ) ∂μcirc.prod μcirc, γ k p.1 ≠ γ l p.2) : Filter.Tendsto (fun (n : ℕ) => pairInt γ (fun (z w : ℂ) => Ltr (1 / (↑n + 1)) (↑n + 1) ‖z - w‖) k l) Filter.atTop (nhds (pairInt γ (fun (z w : ℂ) => Real.log ‖z - w‖) k l))

Limit of the truncated pair integrals.

theorem Zeta5Irrational.energy_log_nonpos {ι : Type u_1} [Fintype ι] {s : ι → ℝ} {γ : ι → ℝ → ℂ} (hγ : ∀ (k : ι), Continuous (γ k)) {R : ℝ} (hR : ∀ (k : ι) (θ : ℝ), ‖γ k θ‖ ≤ R) (hmass : ∑ k : ι, s k = 0) (hint : ∀ (k l : ι), MeasureTheory.Integrable (fun (p : ℝ × ℝ) => Real.log ‖γ k p.1 - γ l p.2‖) (μcirc.prod μcirc)) (hae : ∀ (k l : ι), ∀ᵐ (p : ℝ × ℝ) ∂μcirc.prod μcirc, γ k p.1 ≠ γ l p.2) : (energy s γ fun (z w : ℂ) => Real.log ‖z - w‖) ≤ 0

Lemma 6.2 (zero-mass logarithmic energy) for explicit atoms.