Factorial bounds for S_n = (5n)!/(n!)⁴ and F_n = ∏_{i<3n} (i!)² (the proof notes (5′), (6′)). -- adapted from Li2Unified/Modular/Base/FactorialLogBounds.lean, Base/SumNatMulLog.lean, -- Base/OriginalFnLogBounds.lean (factorial_log_sum_bounds), Base/OriginalSnLogBounds.lean -- (pattern).

theorem Zeta32.Analytic.EnergyI.factorial_log_error_bounds (n : ℕ) (hn : 1 ≤ n) : 1 / 2 * Real.log ↑n + 11 / 12 ≤ Real.log ↑n.factorial - ↑n * Real.log ↑n + ↑n ∧ Real.log ↑n.factorial - ↑n * Real.log ↑n + ↑n ≤ 1 / 2 * Real.log ↑n + 1

theorem Zeta32.Analytic.EnergyI.integral_mul_log_one {b : ℝ} (hb : 1 ≤ b) : ∫ (x : ℝ) in 1..b, x * Real.log x = b ^ 2 / 2 * Real.log b - b ^ 2 / 4 + 1 / 4

theorem Zeta32.Analytic.EnergyI.sum_nat_mul_log_bounds (h : ℕ) (hh : 1 ≤ h) : ↑h ^ 2 / 2 * Real.log ↑h - ↑h ^ 2 / 4 + 1 / 4 - ↑h * Real.log ↑h ≤ ∑ i ∈ Finset.range h, ↑i * Real.log ↑i ∧ ∑ i ∈ Finset.range h, ↑i * Real.log ↑i ≤ ↑h ^ 2 / 2 * Real.log ↑h - ↑h ^ 2 / 4 + 1 / 4

theorem Zeta32.Analytic.EnergyI.factorial_log_sum_bounds (h : ℕ) (hh : 1 ≤ h) : ↑h ^ 2 * Real.log ↑h - 3 / 2 * ↑h ^ 2 - 2 * ↑h * Real.log ↑h ≤ 2 * ∑ i ∈ Finset.range h, Real.log ↑i.factorial ∧ 2 * ∑ i ∈ Finset.range h, Real.log ↑i.factorial ≤ ↑h ^ 2 * Real.log ↑h - 3 / 2 * ↑h ^ 2 + ↑h * Real.log ↑h + 4 * ↑h

theorem Zeta32.Analytic.EnergyI.Sn_log_upper (n : ℕ) (hn : 1 ≤ n) : Real.log ↑(Sn n) ≤ ↑n * Real.log ↑n + (5 * Real.log 5 - 1) * ↑n + 1

log S_n ≤ n log n + (5 log 5 − 1) n + 1.

theorem Zeta32.Analytic.EnergyI.Fn_log_lower (n : ℕ) (hn : 1 ≤ n) : ↑(3 * n) ^ 2 * Real.log ↑(3 * n) - 3 / 2 * ↑(3 * n) ^ 2 - 2 * ↑(3 * n) * Real.log ↑(3 * n) ≤ Real.log ↑(Fn n)

log F_n ≥ h² log h − (3/2)h² − 2h log h, h = 3n.