The integrals over c ∈ (0, ∞) with the weight g = (1/3, 5/3, 4/3) (the proof notes (8′), the proof notes, Lemma 12):

∫ g ρ_c(t) dc = rhoA a t,   ∫ g (1 − c/u_c)/2 dc = massA a,   ∫ g w_c(x) dc = Wt |x|,
∫ g kC a c dc = ellA a + 2 log(a/2)(massA a − 1).

Each by one generic statement (integral_gtil): g = 1/3 + (4/3)1_{c≥1} − (1/3)1_{c≥5} and ∫_{(α,∞)} Φ' = L − Φ(α). The antiderivatives are −G/(4π), (c − u_c)/2, (c/2)log(1 + x²/c²) + |x| atan(c/|x|) and −J (FstarDefs).

theorem Zeta32.Analytic.EnergyI.gtil_eq (c : ℝ) : gtil c = 1 / 3 + 4 / 3 * (Set.Ici 1).indicator 1 c - 1 / 3 * (Set.Ici 5).indicator 1 c

theorem Zeta32.Analytic.EnergyI.gtil_pos (c : ℝ) : 0 < gtil c

theorem Zeta32.Analytic.EnergyI.measurable_gtil : Measurable gtil

theorem Zeta32.Analytic.EnergyI.setIntegral_Ioi_indicator {F : ℝ → ℝ} {α : ℝ} (hα : 0 ≤ α) : ∫ (c : ℝ) in Set.Ioi 0, (Set.Ici α).indicator 1 c * F c = ∫ (c : ℝ) in Set.Ioi α, F c

theorem Zeta32.Analytic.EnergyI.integral_gtil {F Φ : ℝ → ℝ} {L : ℝ} (hcont : ContinuousWithinAt Φ (Set.Ici 0) 0) (hderiv : ∀ c ∈ Set.Ioi 0, HasDerivAt Φ (F c) c) (hint : MeasureTheory.IntegrableOn F (Set.Ioi 0) MeasureTheory.volume) (hlim : Filter.Tendsto Φ Filter.atTop (nhds L)) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * F c) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (c : ℝ) in Set.Ioi 0, gtil c * F c = 4 / 3 * L - 1 / 3 * Φ 0 - 4 / 3 * Φ 1 + 1 / 3 * Φ 5

The generic g-integral.

theorem Zeta32.Analytic.EnergyI.hasDerivAt_uC {a : ℝ} (ha : 0 < a) (c : ℝ) : HasDerivAt (fun (c : ℝ) => uC a c) (c / uC a c) c

theorem Zeta32.Analytic.EnergyI.continuous_uC (a : ℝ) : Continuous fun (c : ℝ) => uC a c

theorem Zeta32.Analytic.EnergyI.uC_zero {a : ℝ} (ha : 0 < a) : uC a 0 = a

theorem Zeta32.Analytic.EnergyI.tendsto_uC_sub {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (c : ℝ) => uC a c - c) Filter.atTop (nhds 0)

theorem Zeta32.Analytic.EnergyI.tendsto_uC_atTop {a : ℝ} (ha : 0 < a) : Filter.Tendsto (fun (c : ℝ) => uC a c) Filter.atTop Filter.atTop

theorem Zeta32.Analytic.EnergyI.integral_gtil_mass {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * ((1 - c / uC a c) / 2)) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (c : ℝ) in Set.Ioi 0, gtil c * ((1 - c / uC a c) / 2) = massA a

∫ g (1 − c/u_c)/2 dc = massA a.

theorem Zeta32.Analytic.EnergyI.hasDerivAt_Gfun {a t : ℝ} (ha : 0 < a) (ht0 : t ≠ 0) (hta : |t| < a) (c : ℝ) : HasDerivAt (fun (c : ℝ) => -Gfun a c t / (4 * Real.pi)) (rhoC a c t) c

theorem Zeta32.Analytic.EnergyI.tendsto_Gfun {a : ℝ} (ha : 0 < a) (t : ℝ) : Filter.Tendsto (fun (c : ℝ) => -Gfun a c t / (4 * Real.pi)) Filter.atTop (nhds 0)

theorem Zeta32.Analytic.EnergyI.integral_gtil_rhoC {a t : ℝ} (ha : 0 < a) (ht0 : t ≠ 0) (hta : |t| < a) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * rhoC a c t) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (c : ℝ) in Set.Ioi 0, gtil c * rhoC a c t = rhoA a t

rhoA a t = ∫ g ρ_c(t) dc for 0 < |t| < a.

noncomputable def Zeta32.Analytic.EnergyI.PhiW (y c : ℝ) : ℝ

Antiderivative of wC · x in c (y = |x| > 0).

Equations

• Zeta32.Analytic.EnergyI.PhiW y c = c / 2 * Real.log (c ^ 2 + y ^ 2) - c * Real.log c + y * Real.arctan (c / y)

theorem Zeta32.Analytic.EnergyI.hasDerivAt_PhiW {y : ℝ} (hy : 0 < y) {c : ℝ} (hc : 0 < c) : HasDerivAt (PhiW y) (Real.log (1 + y ^ 2 / c ^ 2) / 2) c

theorem Zeta32.Analytic.EnergyI.continuous_PhiW {y : ℝ} (hy : 0 < y) : Continuous (PhiW y)

theorem Zeta32.Analytic.EnergyI.tendsto_PhiW {y : ℝ} (hy : 0 < y) : Filter.Tendsto (PhiW y) Filter.atTop (nhds (y * (Real.pi / 2)))

theorem Zeta32.Analytic.EnergyI.integral_gtil_wC (x : ℝ) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * wC c x) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (c : ℝ) in Set.Ioi 0, gtil c * wC c x = Wt |x|

Wt |x| = ∫ g w_c(x) dc.

noncomputable def Zeta32.Analytic.EnergyI.PhiJ (a c : ℝ) : ℝ

Antiderivative of log(2c/(c + u_c)): −J.

Equations

• Zeta32.Analytic.EnergyI.PhiJ a c = c * Real.log 2 + c * Real.log c - c * Real.log (c + Zeta32.Analytic.EnergyI.uC a c) + Zeta32.Analytic.EnergyI.uC a c - c

theorem Zeta32.Analytic.EnergyI.PhiJ_eq_neg_Jfun {a : ℝ} (ha : 0 < a) {c : ℝ} (hc : 0 ≤ c) : PhiJ a c = -Jfun a c

theorem Zeta32.Analytic.EnergyI.hasDerivAt_PhiJ {a : ℝ} (ha : 0 < a) {c : ℝ} (hc : 0 < c) : HasDerivAt (PhiJ a) (Real.log (2 * c / (uC a c + c))) c

theorem Zeta32.Analytic.EnergyI.continuous_PhiJ {a : ℝ} (ha : 0 < a) : Continuous (PhiJ a)

theorem Zeta32.Analytic.EnergyI.tendsto_PhiJ {a : ℝ} (ha : 0 < a) : Filter.Tendsto (PhiJ a) Filter.atTop (nhds 0)

theorem Zeta32.Analytic.EnergyI.integral_gtil_kC {a : ℝ} (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (c : ℝ) => gtil c * kC a c) (Set.Ioi 0) MeasureTheory.volume ∧ ∫ (c : ℝ) in Set.Ioi 0, gtil c * kC a c = ellA a + 2 * Real.log (a / 2) * (massA a - 1)

∫ g kC dc = ellA a + 2 log(a/2)(massA a − 1).