The configuration inequality (13′) of the proof notes, §5.3 for a density on [-a, a].

Replace each point x_i by the circle of radius ε about it (angular measure, mass 2π) and the comparison density by the measure ν = ρ(t)dt on [-a, a] ⊂ ℂ; apply the zero-mass energy inequality (ZeroMass) to ν − (1/(2πh)) Σ circles. Circle self energy (2π)² log ε, circle–circle ≥ (2π)² log|x_i − x_j| (CircleTools, from Li₂), circle–ν: 2π ∫ ρ(t) log max(ε, |x_i − t|) dt = 2π(L(x_i) + ∫ ρ K) with the truncation error K ≥ 0, K = 0 for |x_i − t| ≥ ε, and ∫ ρK ≤ √ε(N²/2 + 2) by AM–GM and ∫ K² ≤ 4ε (this replaces the rearrangement step of the proof notes (13′); only ρ ∈ L² is used).

structure Zeta32.Analytic.EnergyI.GoodDensity (ρ : ℝ → ℝ) (a : ℝ) : Prop

A probability density on [-a, a] with square-integrable density.

• pos : 0 < a
• meas : Measurable ρ
• nonneg : ∀ᵐ (t : ℝ), t ∈ Set.Icc (-a) a → 0 ≤ ρ t
• int : IntervalIntegrable ρ MeasureTheory.volume (-a) a
• int2 : IntervalIntegrable (fun (t : ℝ) => ρ t ^ 2) MeasureTheory.volume (-a) a
• mass : ∫ (t : ℝ) in -a..a, ρ t = 1

∫ log²

noncomputable def Zeta32.Analytic.EnergyI.gLog2 (t : ℝ) : ℝ

t log²t − 2t log t + 2t, written so that it is visibly continuous at 0.

Equations

• Zeta32.Analytic.EnergyI.gLog2 t = 4 * (√t * Real.log √t) ^ 2 - 2 * (t * Real.log t) + 2 * t

theorem Zeta32.Analytic.EnergyI.continuous_gLog2 : Continuous gLog2

theorem Zeta32.Analytic.EnergyI.hasDerivAt_gLog2 {t : ℝ} (ht0 : 0 < t) : HasDerivAt gLog2 (Real.log t ^ 2) t

theorem Zeta32.Analytic.EnergyI.integral_log_sq_zero_one : ∫ (v : ℝ) in 0..1, Real.log v ^ 2 = 2

theorem Zeta32.Analytic.EnergyI.integral_log_abs_sq_neg_one_one : ∫ (v : ℝ) in -1..1, Real.log |v| ^ 2 = 4

theorem Zeta32.Analytic.EnergyI.integral_log_div_sq {ε : ℝ} (hε : 0 < ε) (c : ℝ) : ∫ (t : ℝ) in c - ε..c + ε, Real.log (|c - t| / ε) ^ 2 = 4 * ε

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_div_sq {ε : ℝ} (hε : 0 < ε) (c α β : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log (|c - t| / ε) ^ 2) MeasureTheory.volume α β

The truncation error K

noncomputable def Zeta32.Analytic.EnergyI.Kt (ε u : ℝ) : ℝ

K(u) = log ε + log⁺(|u|/ε) − log|u| = log max(ε,|u|) − log|u|.

Equations

• Zeta32.Analytic.EnergyI.Kt ε u = Real.log ε + (ε⁻¹ * |u|).posLog - Real.log |u|

theorem Zeta32.Analytic.EnergyI.measurable_Kt (ε : ℝ) : Measurable (Kt ε)

theorem Zeta32.Analytic.EnergyI.Kt_nonneg {ε u : ℝ} (hε : 0 < ε) (hu : u ≠ 0) : 0 ≤ Kt ε u

noncomputable def Zeta32.Analytic.EnergyI.Kb (ε c t : ℝ) : ℝ

The dominating function of K².

Equations

• Zeta32.Analytic.EnergyI.Kb ε c t = (Set.Icc (c - ε) (c + ε)).indicator (fun (t : ℝ) => Real.log (|c - t| / ε) ^ 2) t

theorem Zeta32.Analytic.EnergyI.Kt_sq_le {ε c t : ℝ} (hε : 0 < ε) (ht : t ≠ c) : Kt ε (c - t) ^ 2 ≤ Kb ε c t

theorem Zeta32.Analytic.EnergyI.Kb_nonneg (ε c t : ℝ) : 0 ≤ Kb ε c t

theorem Zeta32.Analytic.EnergyI.integrable_Kb {ε : ℝ} (hε : 0 < ε) (c : ℝ) : MeasureTheory.Integrable (Kb ε c) MeasureTheory.volume

theorem Zeta32.Analytic.EnergyI.integral_Kb {ε : ℝ} (hε : 0 < ε) (c : ℝ) : ∫ (t : ℝ), Kb ε c t = 4 * ε

Density lemmas for GoodDensity

theorem Zeta32.Analytic.EnergyI.GoodDensity.intervalIntegrable_log_mul {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (x : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log |x - t| * ρ t) MeasureTheory.volume (-a) a

theorem Zeta32.Analytic.EnergyI.GoodDensity.abs_log_mul_le (ρ : ℝ → ℝ) (x t : ℝ) : |Real.log |x - t|| * |ρ t| ≤ (Real.log |x - t| ^ 2 + ρ t ^ 2) / 2

theorem Zeta32.Analytic.EnergyI.GoodDensity.cross_error {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (c : ℝ) {ε : ℝ} (hε : 0 < ε) : IntervalIntegrable (fun (t : ℝ) => ρ t * Kt ε (c - t)) MeasureTheory.volume (-a) a ∧ ∫ (t : ℝ) in -a..a, ρ t * Kt ε (c - t) ≤ √ε * ((∫ (t : ℝ) in -a..a, ρ t ^ 2) / 2 + 2)

∫ ρ K ≤ √ε (N²/2 + 2).

Measures

theorem Zeta32.Analytic.EnergyI.norm_ofReal_sub (s t : ℝ) : ‖↑s - ↑t‖ = |s - t|

noncomputable def Zeta32.Analytic.EnergyI.circB : MeasureTheory.Measure ℝ

Angular measure on (0, 2π] (mass 2π).

Equations

• Zeta32.Analytic.EnergyI.circB = MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))

instance Zeta32.Analytic.EnergyI.instIsFiniteMeasureRealCircB : MeasureTheory.IsFiniteMeasure circB

theorem Zeta32.Analytic.EnergyI.integral_circB (g : ℝ → ℝ) : ∫ (θ : ℝ), g θ ∂circB = ∫ (θ : ℝ) in 0..2 * Real.pi, g θ

theorem Zeta32.Analytic.EnergyI.real_circB : circB.real Set.univ = 2 * Real.pi

noncomputable def Zeta32.Analytic.EnergyI.nuB (ρ : ℝ → ℝ) (a : ℝ) : MeasureTheory.Measure ℝ

The comparison measure ρ(t) dt on (-a, a].

Equations

• Zeta32.Analytic.EnergyI.nuB ρ a = (MeasureTheory.volume.restrict (Set.Ioc (-a) a)).withDensity fun (t : ℝ) => ENNReal.ofReal (ρ t)

instance Zeta32.Analytic.EnergyI.instSFiniteRealNuB (ρ : ℝ → ℝ) (a : ℝ) : MeasureTheory.SFinite (nuB ρ a)

theorem Zeta32.Analytic.EnergyI.GoodDensity.isFiniteMeasure_nuB {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) : MeasureTheory.IsFiniteMeasure (nuB ρ a)

theorem Zeta32.Analytic.EnergyI.GoodDensity.integral_nuB {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (g : ℝ → ℝ) : ∫ (t : ℝ), g t ∂nuB ρ a = ∫ (t : ℝ) in -a..a, ρ t * g t

theorem Zeta32.Analytic.EnergyI.GoodDensity.integrable_nuB {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (g : ℝ → ℝ) : MeasureTheory.Integrable g (nuB ρ a) ↔ IntervalIntegrable (fun (t : ℝ) => ρ t * g t) MeasureTheory.volume (-a) a

theorem Zeta32.Analytic.EnergyI.GoodDensity.ae_nuB {ρ : ℝ → ℝ} {a : ℝ} : ∀ᵐ (t : ℝ) ∂nuB ρ a, t ∈ Set.Ioc (-a) a

theorem Zeta32.Analytic.EnergyI.GoodDensity.real_nuB {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) : (nuB ρ a).real Set.univ = 1

theorem Zeta32.Analytic.EnergyI.nuB_fiber_null (ρ : ℝ → ℝ) (a : ℝ) (w : ℂ) : (nuB ρ a) {t : ℝ | ↑t = w} = 0

Pushforwards to ℂ

theorem Zeta32.Analytic.EnergyI.integral_prod_map {β₁ β₂ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite β₁] [MeasureTheory.SFinite β₂] {γ₁ γ₂ : ℝ → ℂ} (h₁ : Measurable γ₁) (h₂ : Measurable γ₂) {f : ℂ × ℂ → ℝ} (hf : Measurable f) : ∫ (p : ℂ × ℂ), f p ∂(MeasureTheory.Measure.map γ₁ β₁).prod (MeasureTheory.Measure.map γ₂ β₂) = ∫ (q : ℝ × ℝ), f (γ₁ q.1, γ₂ q.2) ∂β₁.prod β₂

theorem Zeta32.Analytic.EnergyI.integrable_prod_map {β₁ β₂ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite β₁] [MeasureTheory.SFinite β₂] {γ₁ γ₂ : ℝ → ℂ} (h₁ : Measurable γ₁) (h₂ : Measurable γ₂) {f : ℂ × ℂ → ℝ} (hf : Measurable f) : MeasureTheory.Integrable f ((MeasureTheory.Measure.map γ₁ β₁).prod (MeasureTheory.Measure.map γ₂ β₂)) ↔ MeasureTheory.Integrable (fun (q : ℝ × ℝ) => f (γ₁ q.1, γ₂ q.2)) (β₁.prod β₂)

theorem Zeta32.Analytic.EnergyI.ae_ne_prod_map {β₁ β₂ : MeasureTheory.Measure ℝ} [MeasureTheory.SFinite β₁] [MeasureTheory.SFinite β₂] {γ₁ γ₂ : ℝ → ℂ} (h₁ : Measurable γ₁) (h₂ : Measurable γ₂) : (∀ᵐ (p : ℂ × ℂ) ∂(MeasureTheory.Measure.map γ₁ β₁).prod (MeasureTheory.Measure.map γ₂ β₂), p.1 ≠ p.2) ↔ ∀ᵐ (q : ℝ × ℝ) ∂β₁.prod β₂, γ₁ q.1 ≠ γ₂ q.2

theorem Zeta32.Analytic.EnergyI.real_map {β : MeasureTheory.Measure ℝ} {γ : ℝ → ℂ} (h : Measurable γ) : (MeasureTheory.Measure.map γ β).real Set.univ = β.real Set.univ

theorem Zeta32.Analytic.EnergyI.measurable_logK : Measurable fun (p : ℂ × ℂ) => Real.log ‖p.1 - p.2‖

Circle–circle

theorem Zeta32.Analytic.EnergyI.integral_cc (c d : ℂ) {ε : ℝ} (hε : 0 < ε) : ∫ (q : ℝ × ℝ), Real.log ‖circleMap c ε q.1 - circleMap d ε q.2‖ ∂circB.prod circB = ∫ (θ : ℝ) (φ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap c ε θ - circleMap d ε φ‖

theorem Zeta32.Analytic.EnergyI.ae_cc (c d : ℂ) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (q : ℝ × ℝ) ∂circB.prod circB, circleMap c ε q.1 ≠ circleMap d ε q.2

Circle–density

theorem Zeta32.Analytic.EnergyI.measurable_cn (c : ℂ) (ε : ℝ) : Measurable fun (q : ℝ × ℝ) => Real.log ‖circleMap c ε q.1 - ↑q.2‖

theorem Zeta32.Analytic.EnergyI.circle_abs_log_le (c : ℂ) {ε : ℝ} (hε : 0 < ε) {a : ℝ} (t : ℝ) (ht : |t| ≤ a) : ∫ (θ : ℝ), ‖Real.log ‖circleMap c ε θ - ↑t‖‖ ∂circB ≤ 4 * Real.pi * (‖c‖ + a + ε) - 2 * Real.pi * Real.log ε

theorem Zeta32.Analytic.EnergyI.GoodDensity.integrable_cn {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (c : ℂ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (fun (q : ℝ × ℝ) => Real.log ‖circleMap c ε q.1 - ↑q.2‖) (circB.prod (nuB ρ a))

theorem Zeta32.Analytic.EnergyI.GoodDensity.integral_cn {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (c : ℂ) {ε : ℝ} (hε : 0 < ε) : ∫ (q : ℝ × ℝ), Real.log ‖circleMap c ε q.1 - ↑q.2‖ ∂circB.prod (nuB ρ a) = ∫ (t : ℝ) in -a..a, ρ t * (2 * Real.pi * (Real.log ε + (ε⁻¹ * ‖c - ↑t‖).posLog))

theorem Zeta32.Analytic.EnergyI.ae_cn (ρ : ℝ → ℝ) (a : ℝ) (c : ℂ) {ε : ℝ} : ∀ᵐ (q : ℝ × ℝ) ∂circB.prod (nuB ρ a), circleMap c ε q.1 ≠ ↑q.2

theorem Zeta32.Analytic.EnergyI.ae_nc (ρ : ℝ → ℝ) (a : ℝ) (c : ℂ) {ε : ℝ} (hε : 0 < ε) : ∀ᵐ (q : ℝ × ℝ) ∂(nuB ρ a).prod circB, ↑q.1 ≠ circleMap c ε q.2

Density–density

theorem Zeta32.Analytic.EnergyI.measurable_nn : Measurable fun (q : ℝ × ℝ) => Real.log ‖↑q.1 - ↑q.2‖

theorem Zeta32.Analytic.EnergyI.integral_log_sq_shift_le {a : ℝ} (ha : 0 < a) {s : ℝ} (hs : |s| ≤ a) : ∫ (t : ℝ) in -a..a, Real.log |s - t| ^ 2 ≤ ∫ (u : ℝ) in -(2 * a)..2 * a, Real.log |u| ^ 2

theorem Zeta32.Analytic.EnergyI.GoodDensity.integrable_nn_slice {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) (s : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => Real.log ‖↑s - ↑t‖) (nuB ρ a)

theorem Zeta32.Analytic.EnergyI.GoodDensity.integrable_nn {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) : MeasureTheory.Integrable (fun (q : ℝ × ℝ) => Real.log ‖↑q.1 - ↑q.2‖) ((nuB ρ a).prod (nuB ρ a))

theorem Zeta32.Analytic.EnergyI.GoodDensity.integral_nn {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) : ∫ (q : ℝ × ℝ), Real.log ‖↑q.1 - ↑q.2‖ ∂(nuB ρ a).prod (nuB ρ a) = ID ρ a

theorem Zeta32.Analytic.EnergyI.ae_nn (ρ : ℝ → ℝ) (a : ℝ) : ∀ᵐ (q : ℝ × ℝ) ∂(nuB ρ a).prod (nuB ρ a), ↑q.1 ≠ ↑q.2

The configuration inequality

noncomputable def Zeta32.Analytic.EnergyI.atom (ρ : ℝ → ℝ) (a : ℝ) {h : ℕ} (x : Fin h → ℝ) (ε : ℝ) : Option (Fin h) → MeasureTheory.Measure ℂ

The atoms: the comparison measure and the h circles.

Equations

• Zeta32.Analytic.EnergyI.atom ρ a x ε none = MeasureTheory.Measure.map (fun (t : ℝ) => ↑t) (Zeta32.Analytic.EnergyI.nuB ρ a)
• Zeta32.Analytic.EnergyI.atom ρ a x ε (some i) = MeasureTheory.Measure.map (circleMap (↑(x i)) ε) Zeta32.Analytic.EnergyI.circB

theorem Zeta32.Analytic.EnergyI.discrete_energy {ρ : ℝ → ℝ} {a : ℝ} (hρ : GoodDensity ρ a) {h : ℕ} (hh : 0 < h) (x : Fin h → ℝ) (hx : Function.Injective x) {ε : ℝ} (hε : 0 < ε) : 2 * ∑ i : Fin h, ∑ j > i, Real.log |x j - x i| ≤ 2 * ↑h * ∑ i : Fin h, potD ρ a (x i) - ↑h ^ 2 * ID ρ a - ↑h * Real.log ε + 2 * ↑h ^ 2 * (√ε * (32 + (∫ (t : ℝ) in -a..a, ρ t ^ 2) / 2))

the proof notes (13′): discretisation by circles of radius ε, zero-mass energy inequality.