Circle logarithmic integrals and the finite signed-energy algebra. Everything in this file is copied from the Li₂(1/2) formalization (same toolchain), with namespace changed: -- adapted from Li2Unified/Modular/Base/CircleLogTools.lean, Base/CirclePairLog.lean -- (themselves adapted from -- mo271/Zeta5 Apery/CircleAtoms.lean, Apache-2.0), -- adapted from Li2Unified/Modular/Positive/Packed/P194.lean (circle_fiber_null, -- pair_collision_null), -- adapted from Li2Unified/Modular/Base/FiniteSignedEnergyAlgebra.lean, -- Base/FiniteSignedEnergyBound.lean, -- Positive/Packed/P197.lean (complex_signed_energy_log_bound).

theorem Zeta32.Analytic.EnergyI.circle_log_integrable (c a : ℂ) (R : ℝ) : IntervalIntegrable (fun (θ : ℝ) => Real.log ‖circleMap c R θ - a‖) MeasureTheory.volume 0 (2 * Real.pi)

theorem Zeta32.Analytic.EnergyI.circle_log_integral (c a : ℂ) {R : ℝ} (hR : R ≠ 0) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap c R θ - a‖ = 2 * Real.pi * (Real.log R + (R⁻¹ * ‖c - a‖).posLog)

theorem Zeta32.Analytic.EnergyI.circle_log_integral_rev (c a : ℂ) {R : ℝ} (hR : R ≠ 0) : ∫ (θ : ℝ) in 0..2 * Real.pi, Real.log ‖a - circleMap c R θ‖ = 2 * Real.pi * (Real.log R + (R⁻¹ * ‖c - a‖).posLog)

theorem Zeta32.Analytic.EnergyI.circle_abs_log_eq (x : ℝ) : |Real.log x| = 2 * x.posLog - Real.log x

theorem Zeta32.Analytic.EnergyI.continuous_circle_log_row (c d : ℂ) {ε : ℝ} (hε : 0 < ε) : Continuous fun (θ : ℝ) => ∫ (φ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap c ε θ - circleMap d ε φ‖

theorem Zeta32.Analytic.EnergyI.integrable_circle_pair_log (c d : ℂ) {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => Real.log ‖circleMap c ε p.1 - circleMap d ε p.2‖) ((MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))).prod (MeasureTheory.volume.restrict (Set.Ioc 0 (2 * Real.pi))))

Joint absolute integrability is established before any Fubini use.

theorem Zeta32.Analytic.EnergyI.circle_pair_log_self (c : ℂ) {ε : ℝ} (hε : 0 < ε) : ∫ (θ : ℝ) (φ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap c ε θ - circleMap c ε φ‖ = (2 * Real.pi) ^ 2 * Real.log ε

theorem Zeta32.Analytic.EnergyI.circle_pair_log_lower (c d : ℂ) {ε : ℝ} (hε : 0 < ε) (hne : c ≠ d) : (2 * Real.pi) ^ 2 * Real.log ‖c - d‖ ≤ ∫ (θ : ℝ) (φ : ℝ) in 0..2 * Real.pi, Real.log ‖circleMap c ε θ - circleMap d ε φ‖

theorem Zeta32.Analytic.EnergyI.circle_fiber_null (c w : ℂ) (r a b : ℝ) (hr : r ≠ 0) : (MeasureTheory.volume.restrict (Set.Ioc a b)) {t : ℝ | circleMap c r t = w} = 0

theorem Zeta32.Analytic.EnergyI.pair_collision_null (f g : ℝ → ℂ) (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (hf : Continuous f) (hg : Continuous g) (hnull : ∀ (w : ℂ), ν {t : ℝ | g t = w} = 0) : (μ.prod ν) {p : ℝ × ℝ | f p.1 = g p.2} = 0

theorem Zeta32.Analytic.EnergyI.option_signed_weight_double_sum {h : ℕ} (c : ℝ) (E : Option (Fin h) → Option (Fin h) → ℝ) : have w := fun (k : Option (Fin h)) => match k with | none => -1 | some val => c; ∑ k : Option (Fin h), ∑ l : Option (Fin h), w k * w l * E k l = c ^ 2 * ∑ i : Fin h, ∑ j : Fin h, E (some i) (some j) - c * ∑ i : Fin h, E (some i) none - c * ∑ j : Fin h, E none (some j) + E none none

theorem Zeta32.Analytic.EnergyI.symmetric_double_sum_eq_diag_add_two_Ioi {h : ℕ} (F : Fin h → Fin h → ℝ) (hF : ∀ (i j : Fin h), F i j = F j i) : ∑ i : Fin h, ∑ j : Fin h, F i j = ∑ i : Fin h, F i i + 2 * ∑ i : Fin h, ∑ j > i, F i j

theorem Zeta32.Analytic.EnergyI.finite_signed_energy_cross_sum_upper {h : ℕ} (T M ε : ℝ) (L : Fin h → ℝ) (E : Option (Fin h) → Option (Fin h) → ℝ) (hcross : ∀ (i : Fin h), E (some i) none ≤ T * (L i + 2 * M * ε)) : ∑ i : Fin h, E (some i) none ≤ T * (∑ i : Fin h, L i + 2 * M * ε * ↑h)

theorem Zeta32.Analytic.EnergyI.complex_signed_energy_circle_sum_lower {h : ℕ} (x : Fin h → ℂ) (T ε : ℝ) (E : Option (Fin h) → Option (Fin h) → ℝ) (hEsym : ∀ (k l : Option (Fin h)), E k l = E l k) (hdiag : ∀ (i : Fin h), E (some i) (some i) = T ^ 2 * Real.log ε) (hoff : ∀ (i j : Fin h), i ≠ j → T ^ 2 * Real.log ‖x j - x i‖ ≤ E (some i) (some j)) : ↑h * T ^ 2 * Real.log ε + 2 * T ^ 2 * ∑ i : Fin h, ∑ j > i, Real.log ‖x j - x i‖ ≤ ∑ i : Fin h, ∑ j : Fin h, E (some i) (some j)

theorem Zeta32.Analytic.EnergyI.complex_signed_energy_log_bound {h : ℕ} (hh : 0 < h) (T ε M : ℝ) (hT : 0 < T) (x : Fin h → ℂ) (L : Fin h → ℝ) (I : ℝ) (E : Option (Fin h) → Option (Fin h) → ℝ) (hEsym : ∀ (k l : Option (Fin h)), E k l = E l k) (henergy : have w := fun (k : Option (Fin h)) => match k with | none => -1 | some val => 1 / (↑h * T); ∑ k : Option (Fin h), ∑ l : Option (Fin h), w k * w l * E k l ≤ 0) (h00 : E none none = I) (hcross : ∀ (i : Fin h), E (some i) none ≤ T * (L i + 2 * M * ε)) (hdiag : ∀ (i : Fin h), E (some i) (some i) = T ^ 2 * Real.log ε) (hoff : ∀ (i j : Fin h), i ≠ j → T ^ 2 * Real.log ‖x j - x i‖ ≤ E (some i) (some j)) : 2 * ∑ i : Fin h, ∑ j > i, Real.log ‖x j - x i‖ ≤ 2 * ↑h * ∑ i : Fin h, L i - ↑h ^ 2 * I - ↑h * Real.log ε + 4 * M * ↑h ^ 2 * ε