Zero-mass logarithmic energy inequality for finite measures on ℂ (the proof notes (12), GLOBAL-INTEGRAL-v1 §4): for finite measures μ_k and real weights w_k with Σ w_k μ_k(ℂ) = 0, integrable log|z − w| and null diagonals, Σ_{k,l} w_k w_l ∫∫ log|z − w| dμ_k dμ_l ≤ 0.

Gaussian positivity for the truncated kernel L_{a,b}(r) = ½∫_a^b (e^{-s} − e^{-s r²})/s ds, then dominated convergence L_{1/(n+1), n+1} → log. The scalar kernel facts and the Gaussian convolution on ℂ are adapted from the Li₂(1/2) formalization (Li2Unified/Modular/Positive/Packed/P183–P185, themselves a port of mo271/Zeta5 Apery/Gaussian, Kernel, ZeroMass, EnergyLimit, Apache-2.0); the measure-level Gaussian positivity is new here (the Li₂ version needs bounded continuous curve densities; our comparison density is unbounded).

Shared truncated-kernel and Gaussian facts

Gaussian positivity for finite measures (new)

noncomputable def Zeta32.Analytic.EnergyI.gM (μ : MeasureTheory.Measure ℂ) (t : ℝ) (u : ℂ) : ℝ

The Gaussian smoothing of a measure.

Equations

• Zeta32.Analytic.EnergyI.gM μ t u = ∫ (z : ℂ), Real.exp (-(2 * t) * ‖z - u‖ ^ 2) ∂μ

noncomputable def Zeta32.Analytic.EnergyI.gF (t : ℝ) (q : (ℂ × ℂ) × ℂ) : ℝ

The integrand of the Gaussian convolution.

Equations

• Zeta32.Analytic.EnergyI.gF t q = Real.exp (-(2 * t) * ‖q.1.1 - q.2‖ ^ 2) * Real.exp (-(2 * t) * ‖q.1.2 - q.2‖ ^ 2)

theorem Zeta32.Analytic.EnergyI.continuous_gF (t : ℝ) : Continuous (gF t)

theorem Zeta32.Analytic.EnergyI.integral_gF {t : ℝ} (ht : 0 < t) (p : ℂ × ℂ) : ∫ (u : ℂ), gF t (p, u) = Real.pi / (4 * t) * Real.exp (-t * ‖p.1 - p.2‖ ^ 2)

theorem Zeta32.Analytic.EnergyI.integrable_gF_slice {t : ℝ} (ht : 0 < t) (p : ℂ × ℂ) : MeasureTheory.Integrable (fun (u : ℂ) => gF t (p, u)) MeasureTheory.volume

theorem Zeta32.Analytic.EnergyI.integrable_gF {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (gF t) ((μ.prod ν).prod MeasureTheory.volume)

theorem Zeta32.Analytic.EnergyI.gM_mul_eq {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {t : ℝ} (u : ℂ) : ∫ (p : ℂ × ℂ), gF t (p, u) ∂μ.prod ν = gM μ t u * gM ν t u

theorem Zeta32.Analytic.EnergyI.integrable_gM_mul {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (u : ℂ) => gM μ t u * gM ν t u) MeasureTheory.volume

theorem Zeta32.Analytic.EnergyI.gauss_pair_eq {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {t : ℝ} (ht : 0 < t) : ∫ (p : ℂ × ℂ), Real.exp (-t * ‖p.1 - p.2‖ ^ 2) ∂μ.prod ν = 4 * t / Real.pi * ∫ (u : ℂ), gM μ t u * gM ν t u

∫∫ e^{-t|z−w|²} dμ dν = (4t/π) ∫ g_μ g_ν.

theorem Zeta32.Analytic.EnergyI.gauss_energy_nonneg {ι : Type u_1} [Fintype ι] (m : ι → MeasureTheory.Measure ℂ) [∀ (k : ι), MeasureTheory.IsFiniteMeasure (m k)] (w : ι → ℝ) {t : ℝ} (ht : 0 < t) : 0 ≤ ∑ k : ι, ∑ l : ι, w k * w l * ∫ (p : ℂ × ℂ), Real.exp (-t * ‖p.1 - p.2‖ ^ 2) ∂(m k).prod (m l)

Gaussian positivity of a signed finite combination.

The truncated kernel against finite measures

noncomputable def Zeta32.Analytic.EnergyI.ltrF (p : ℂ × ℂ) (s : ℝ) : ℝ

The integrand of Ltr as a function of (p, s).

Equations

• Zeta32.Analytic.EnergyI.ltrF p s = (Real.exp (-s) - Real.exp (-s * ‖p.1 - p.2‖ ^ 2)) / s

theorem Zeta32.Analytic.EnergyI.measurable_ltrF : Measurable (Function.uncurry ltrF)

theorem Zeta32.Analytic.EnergyI.integrable_ltrF {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {α β : ℝ} (hα : 0 < α) : MeasureTheory.Integrable (Function.uncurry ltrF) ((μ.prod ν).prod (MeasureTheory.volume.restrict (Set.Ioc α β)))

theorem Zeta32.Analytic.EnergyI.integral_Ltr_eq {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {α β : ℝ} (hα : 0 < α) (hαβ : α ≤ β) : ∫ (p : ℂ × ℂ), Ltr α β ‖p.1 - p.2‖ ∂μ.prod ν = 1 / 2 * ∫ (s : ℝ) in Set.Ioc α β, ∫ (p : ℂ × ℂ), ltrF p s ∂μ.prod ν

∫ Ltr(|z − w|) dμ dν = ½ ∫_α^β ∫ ltrF.

theorem Zeta32.Analytic.EnergyI.integral_ltrF {μ ν : MeasureTheory.Measure ℂ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : ℝ} (hs : 0 ≤ s) : ∫ (p : ℂ × ℂ), ltrF p s ∂μ.prod ν = (Real.exp (-s) * (μ.real Set.univ * ν.real Set.univ) - ∫ (p : ℂ × ℂ), Real.exp (-s * ‖p.1 - p.2‖ ^ 2) ∂μ.prod ν) / s

theorem Zeta32.Analytic.EnergyI.zero_mass_energy_nonpos {ι : Type u_1} [Fintype ι] (μ : ι → MeasureTheory.Measure ℂ) [∀ (k : ι), MeasureTheory.IsFiniteMeasure (μ k)] (w : ι → ℝ) (hmass : ∑ k : ι, w k * (μ k).real Set.univ = 0) (hint : ∀ (k l : ι), MeasureTheory.Integrable (fun (p : ℂ × ℂ) => Real.log ‖p.1 - p.2‖) ((μ k).prod (μ l))) (hdiag : ∀ (k l : ι), ∀ᵐ (p : ℂ × ℂ) ∂(μ k).prod (μ l), p.1 ≠ p.2) : ∑ k : ι, ∑ l : ι, w k * w l * ∫ (p : ℂ × ℂ), Real.log ‖p.1 - p.2‖ ∂(μ k).prod (μ l) ≤ 0

Zero-mass logarithmic energy inequality for a finite signed combination of finite measures on ℂ.