the proof notes, 5.4 (Lemma 12), the density ρ_a. For 0 < x ≤ a: G(c,x) = 2·arsinh(√(a²−x²)/√(c²+x²)), so ρ_a(x) is a nondecreasing function of s = √(a²−x²) with coefficients x ↦ √(c²+x²) independent of a; this gives ρ_a ≥ 0 and monotonicity in a. Monotonicity in x uses the log form with U_c = √(c²+a²) fixed and the identity (U₁+s)(U₂+t)(U₁−t)(U₂−s) − (U₁+t)(U₂+s)(U₁−s)(U₂−t) = 2(s−t)(U₂−U₁)(U₁U₂+st). Integrability: ρ_a = fc − log x/(6π) on (0, a] with fc continuous. Written from scratch.

theorem Zeta32.Fstar.Gfun_eq_arsinh {a c x : ℝ} (hx : 0 < x) (hxa : x ≤ a) : Gfun a c x = 2 * Real.arsinh (√(a ^ 2 - x ^ 2) / √(c ^ 2 + x ^ 2))

theorem Zeta32.Fstar.hasDerivAt_arsinh_div {k : ℝ} (hk : 0 < k) (s : ℝ) : HasDerivAt (fun (s : ℝ) => Real.arsinh (s / k)) (1 / √(k ^ 2 + s ^ 2)) s

theorem Zeta32.Fstar.arsinh_div_sub_monotone {k₁ k₂ : ℝ} (hk₁ : 0 < k₁) (h₁₂ : k₁ ≤ k₂) : Monotone fun (s : ℝ) => Real.arsinh (s / k₁) - Real.arsinh (s / k₂)

noncomputable def Zeta32.Fstar.Rs (x s : ℝ) : ℝ

ρ_a(x) written through s = √(a² − x²) (arsinh form, valid for 0 < x ≤ a).

Equations

• One or more equations did not get rendered due to their size.

theorem Zeta32.Fstar.rhoA_eq_Rs {a x : ℝ} (hx : 0 < x) (hxa : x ≤ a) : rhoA a x = Rs x √(a ^ 2 - x ^ 2)

theorem Zeta32.Fstar.Rs_monotone {x : ℝ} (hx : 0 < x) : Monotone (Rs x)

theorem Zeta32.Fstar.Rs_zero (x : ℝ) : Rs x 0 = 0

theorem Zeta32.Fstar.rhoA_nonneg {a x : ℝ} (hx : 0 < x) (hxa : x ≤ a) : 0 ≤ rhoA a x

theorem Zeta32.Fstar.rhoA_mono_a {a b x : ℝ} (hx : 0 < x) (hxb : x ≤ b) (hba : b ≤ a) : rhoA b x ≤ rhoA a x

ρ_a(x) is nondecreasing in a for fixed x.

theorem Zeta32.Fstar.log_ratio_mono {U t s : ℝ} (ht : 0 ≤ t) (hts : t ≤ s) (hsU : s < U) : Real.log ((U + t) / (U - t)) ≤ Real.log ((U + s) / (U - s))

theorem Zeta32.Fstar.log_ratio_sub_mono {U₁ U₂ t s : ℝ} (ht : 0 ≤ t) (hts : t ≤ s) (hsU : s < U₁) (hU : U₁ ≤ U₂) : Real.log ((U₁ + t) / (U₁ - t)) - Real.log ((U₂ + t) / (U₂ - t)) ≤ Real.log ((U₁ + s) / (U₁ - s)) - Real.log ((U₂ + s) / (U₂ - s))

theorem Zeta32.Fstar.rhoA_anti_x {a x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) (hya : y ≤ a) : rhoA a y ≤ rhoA a x

ρ_a(x) is nonincreasing in x on (0, a].

theorem Zeta32.Fstar.Gfun_zero_eq {a x : ℝ} (hx : 0 < x) (hxa : x ≤ a) : Gfun a 0 x = 2 * Real.log (a + √(a ^ 2 - x ^ 2)) - 2 * Real.log x

theorem Zeta32.Fstar.continuous_Gfun {a c : ℝ} (ha : 0 < a) (hc : 0 < c) : Continuous fun (x : ℝ) => Gfun a c x

noncomputable def Zeta32.Fstar.fc (a x : ℝ) : ℝ

The continuous part of ρ_a on (0, a].

Equations

• Zeta32.Fstar.fc a x = (1 / 3 * (2 * Real.log (a + √(a ^ 2 - x ^ 2)) - Zeta32.Gfun a 1 x) + 5 / 3 * (Zeta32.Gfun a 1 x - Zeta32.Gfun a 5 x) + 4 / 3 * Zeta32.Gfun a 5 x) / (4 * Real.pi)

theorem Zeta32.Fstar.rhoA_eq_fc {a x : ℝ} (hx : 0 < x) (hxa : x ≤ a) : rhoA a x = fc a x - Real.log x / (6 * Real.pi)

theorem Zeta32.Fstar.continuous_fc {a : ℝ} (ha : 0 < a) : Continuous (fc a)

theorem Zeta32.Fstar.intervalIntegrable_Wt_rhoA {a : ℝ} (ha : 0 < a) : IntervalIntegrable (fun (x : ℝ) => Wt x * rhoA a x) MeasureTheory.volume 0 a

theorem Zeta32.Fstar.Wt_mul_rhoA_nonneg {a x : ℝ} (hx : 0 ≤ x) (hxa : x ≤ a) : 0 ≤ Wt x * rhoA a x