Regularity of the comparison density rhoA a on (-a, a) (the proof notes (8′), "density near 0"): rhoA a t = fc a |t| − log|t|/(6π) with fc continuous (Fstar/Rho.lean), hence rhoA, rhoA² and log|x − ·| · rhoA are integrable (via log² integrable, AM–GM).

theorem Zeta32.Analytic.EnergyI.rhoA_neg (a t : ℝ) : rhoA a (-t) = rhoA a t

theorem Zeta32.Analytic.EnergyI.measurable_rhoA (a : ℝ) : Measurable (rhoA a)

theorem Zeta32.Analytic.EnergyI.rhoA_abs (a t : ℝ) : rhoA a |t| = rhoA a t

theorem Zeta32.Analytic.EnergyI.rhoA_eq_fc_abs {a t : ℝ} (ht : t ≠ 0) (hta : |t| ≤ a) : rhoA a t = Fstar.fc a |t| - Real.log |t| / (6 * Real.pi)

theorem Zeta32.Analytic.EnergyI.rhoA_nonneg_of_ne {a t : ℝ} (ht : t ≠ 0) (hta : |t| ≤ a) : 0 ≤ rhoA a t

theorem Zeta32.Analytic.EnergyI.ae_ne_zero : ∀ᵐ (t : ℝ), t ≠ 0

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_sq (α β : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log t ^ 2) MeasureTheory.volume α β

log² is interval integrable (antiderivative t log²t − 2t log t + 2t).

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_abs_sq (x α β : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log |x - t| ^ 2) MeasureTheory.volume α β

theorem Zeta32.Analytic.EnergyI.rhoA_ae_eq {a : ℝ} (ha : 0 < a) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.uIoc (-a) a), rhoA a t = Fstar.fc a |t| - Real.log |t| / (6 * Real.pi)

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_rhoA {a : ℝ} (ha : 0 < a) : IntervalIntegrable (rhoA a) MeasureTheory.volume (-a) a

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_rhoA_sq {a : ℝ} (ha : 0 < a) : IntervalIntegrable (fun (t : ℝ) => rhoA a t ^ 2) MeasureTheory.volume (-a) a

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_log_mul_rhoA {a : ℝ} (ha : 0 < a) (x : ℝ) : IntervalIntegrable (fun (t : ℝ) => Real.log |x - t| * rhoA a t) MeasureTheory.volume (-a) a

t ↦ log|x − t| · rhoA a t is integrable on (-a, a) for every x.

theorem Zeta32.Analytic.EnergyI.intervalIntegrable_abs_log_mul_rhoA {a : ℝ} (ha : 0 < a) (x : ℝ) : IntervalIntegrable (fun (t : ℝ) => |Real.log |x - t|| * rhoA a t) MeasureTheory.volume (-a) a