5.1. 4. The universal cap🔗

Theorem5.1.1

groupuses 0used by 1✓L∃∀N

Tagspartly kernel-verified

Lemma K12 (log-Gamma series and strict midpoint bounds). For 0 < y < 1 and every a > 1, respectively,

\ln\Gamma(1-y)=\gamma_Ey+\sum_{k=2}^\infty\frac{\zeta(k)y^k}{k}, \qquad j(a)=\sum_{k=2}^\infty\frac{\zeta(k)}{k\,a^{k-1}}. \qquad \text{(K32)}

For every real k > 1 and integer N \ge 1, with \zeta(k) = \sum_{n=1}^\infty n^{-k},

\zeta(k)<\sum_{n=1}^N n^{-k} +\frac{1}{(k-1)(N+1/2)^{k-1}}. \qquad \text{(K33)}

Lean code for Theorem5.1.1●6 theorems

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.gamma_hasSum_product_remainder {y : ℝ}
  (hy : y < 1) :
  HasSum (fun m => -Real.log (1 - y / (↑m + 1)) - y / (↑m + 1))
    (Real.log (Real.Gamma (1 - y)) - Real.eulerMascheroniConstant * y)

theorem NaturalLatents.General.gamma_hasSum_product_remainder
  {y : ℝ} (hy : y < 1) :
  HasSum
    (fun m =>
      -Real.log (1 - y / (↑m + 1)) -
        y / (↑m + 1))
    (Real.log (Real.Gamma (1 - y)) -
      Real.eulerMascheroniConstant * y)

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.gammaPriceCap_log_remainder_hasSum {x : ℝ}
  (hx0 : 0 ≤ x) (hx1 : x < 1) :
  HasSum (fun n => x ^ (n + 2) / (↑n + 2)) (-Real.log (1 - x) - x)

theorem NaturalLatents.General.gammaPriceCap_log_remainder_hasSum
  {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) :
  HasSum (fun n => x ^ (n + 2) / (↑n + 2))
    (-Real.log (1 - x) - x)

The part of the logarithm's power series after its linear term.

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_midpoint_three {x : ℝ} (hx : 1 ≤ x) :
  1 / x ^ 3 < 1 / 2 / (x - 1 / 2) ^ 2 - 1 / 2 / (x + 1 / 2) ^ 2

theorem NaturalLatents.General.cap_midpoint_three
  {x : ℝ} (hx : 1 ≤ x) :
  1 / x ^ 3 <
    1 / 2 / (x - 1 / 2) ^ 2 -
      1 / 2 / (x + 1 / 2) ^ 2

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_tail_three :
  (Summable fun n => 1 / (↑n + 3) ^ 3) ∧
    ∑' (n : ℕ), 1 / (↑n + 3) ^ 3 < 2 / 25

theorem NaturalLatents.General.cap_tail_three :
  (Summable fun n => 1 / (↑n + 3) ^ 3) ∧
    ∑' (n : ℕ), 1 / (↑n + 3) ^ 3 < 2 / 25

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_telescope_bound {f q : ℕ → ℝ}
  (hf : ∀ (n : ℕ), 0 ≤ f n) (hq : ∀ (n : ℕ), 0 ≤ q n)
  (hstep : ∀ (n : ℕ), f n ≤ q n - q (n + 1)) :
  Summable f ∧ ∑' (n : ℕ), f n ≤ q 0

theorem NaturalLatents.General.cap_telescope_bound
  {f q : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n)
  (hq : ∀ (n : ℕ), 0 ≤ q n)
  (hstep :
    ∀ (n : ℕ), f n ≤ q n - q (n + 1)) :
  Summable f ∧ ∑' (n : ℕ), f n ≤ q 0

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_telescope_strict {f q : ℕ → ℝ}
  (hf : ∀ (n : ℕ), 0 ≤ f n) (hq : ∀ (n : ℕ), 0 ≤ q n)
  (hstep : ∀ (n : ℕ), f n ≤ q n - q (n + 1))
  (hstrict : f 0 < q 0 - q 1) : Summable f ∧ ∑' (n : ℕ), f n < q 0

theorem NaturalLatents.General.cap_telescope_strict
  {f q : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n)
  (hq : ∀ (n : ℕ), 0 ≤ q n)
  (hstep :
    ∀ (n : ℕ), f n ≤ q n - q (n + 1))
  (hstrict : f 0 < q 0 - q 1) :
  Summable f ∧ ∑' (n : ℕ), f n < q 0

Proof for Theorem 5.1.1

uses 0

Lean proves: \ln\Gamma(1-y)-\gamma_Ey=\sum_{n\ge1}[-\ln(1-y/n)-y/n] for y<1, -\ln(1-x)-x=\sum_{k\ge2}x^k/k for 0\le x<1, x^{-3}<\frac12(x-1/2)^{-2}-\frac12(x+1/2)^{-2} for x\ge1, and \sum_{n\ge3}n^{-3}<2/25.

Expand log Gamma and the logarithm series; strict convexity on midpoint intervals bounds the zeta tail. See the page section.

Lean: Lean states neither (K32) nor (K33) in this form. In place of (K32), gamma_hasSum_product_remainder states \ln\Gamma(1-y)-\gamma_Ey=\sum_{n\ge1}\left[-\ln(1-y/n)-y/n\right] for y<1, obtained from Mathlib's Bohr-Mollerup limit Real.BohrMollerup.tendsto_log_gamma, and gammaPriceCap_log_remainder_hasSum states the logarithm series -\ln(1-x)-x=\sum_{k\ge2}x^k/k for 0\le x<1; expanding each term of the first by the second and summing over n gives (K32), but Lean never forms the coefficients \zeta(k) for k\ge5. The midpoint estimate (K33) is stated only for k=3: cap_midpoint_three is the strict one-interval inequality, and cap_tail_three the tail bound \sum_{n\ge3}n^{-3}<2/25, through the telescoping lemmas cap_telescope_bound and cap_telescope_strict.

Theorem5.1.2

groupuses 1used by 1✓L∃∀N

Tagskernel-verified

Lemma K13 (the cap). For every real a > 1, define the explicit rational function

F(a)=\frac{533}{648a}+\frac{241}{600a^2} +\frac{6503}{24000a^2(a-1)}. \qquad \text{(K36)}

Then j(a) < F(a).

Lean code for Theorem5.1.2●7 theorems

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.racePrice_lt_capC3b (a : ℝ) (ha : 1 < a) :
  NaturalLatents.General.gammaPrice a <
    NaturalLatents.General.gammaPriceCap a

theorem NaturalLatents.General.racePrice_lt_capC3b
  (a : ℝ) (ha : 1 < a) :
  NaturalLatents.General.gammaPrice a <
    NaturalLatents.General.gammaPriceCap a

The Gamma-form race price lies below its three-term cap: `gammaPrice a < gammaPriceCap a` for `a > 1`.

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.gammaPriceCap_assemble_remainders {y : ℝ}
  (hy0 : 0 < y) (hy1 : y < 1)
  (hs :
    HasSum (fun n => -Real.log (1 - y / (↑n + 1)) - y / (↑n + 1))
      (Real.log (Real.Gamma (1 - y)) -
        Real.eulerMascheroniConstant * y)) :
  Real.log (Real.Gamma (1 - y)) - Real.eulerMascheroniConstant * y <
    533 / 648 * y ^ 2 + 241 / 600 * y ^ 3 +
      6503 / 24000 * y ^ 4 / (1 - y)

theorem NaturalLatents.General.gammaPriceCap_assemble_remainders
  {y : ℝ} (hy0 : 0 < y) (hy1 : y < 1)
  (hs :
    HasSum
      (fun n =>
        -Real.log (1 - y / (↑n + 1)) -
          y / (↑n + 1))
      (Real.log (Real.Gamma (1 - y)) -
        Real.eulerMascheroniConstant *
          y)) :
  Real.log (Real.Gamma (1 - y)) -
      Real.eulerMascheroniConstant * y <
    533 / 648 * y ^ 2 +
        241 / 600 * y ^ 3 +
      6503 / 24000 * y ^ 4 / (1 - y)

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.gammaPriceCap_reciprocal_conversion (a : ℝ)
  (ha : 1 < a)
  (h :
    Real.log (Real.Gamma (1 - 1 / a)) -
        Real.eulerMascheroniConstant * (1 / a) <
      533 / 648 * (1 / a) ^ 2 + 241 / 600 * (1 / a) ^ 3 +
        6503 / 24000 * (1 / a) ^ 4 / (1 - 1 / a)) :
  a * Real.log (Real.Gamma (1 - 1 / a)) - Real.eulerMascheroniConstant <
    533 / (648 * a) + 241 / (600 * a ^ 2) +
      6503 / (24000 * a ^ 2 * (a - 1))

theorem NaturalLatents.General.gammaPriceCap_reciprocal_conversion
  (a : ℝ) (ha : 1 < a)
  (h :
    Real.log (Real.Gamma (1 - 1 / a)) -
        Real.eulerMascheroniConstant *
          (1 / a) <
      533 / 648 * (1 / a) ^ 2 +
          241 / 600 * (1 / a) ^ 3 +
        6503 / 24000 * (1 / a) ^ 4 /
          (1 - 1 / a)) :
  a * Real.log (Real.Gamma (1 - 1 / a)) -
      Real.eulerMascheroniConstant <
    533 / (648 * a) +
        241 / (600 * a ^ 2) +
      6503 / (24000 * a ^ 2 * (a - 1))

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_zeta_two :
  (Summable fun n => 1 / (↑n + 1) ^ 2) ∧
    ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 < 533 / 324

theorem NaturalLatents.General.cap_zeta_two :
  (Summable fun n => 1 / (↑n + 1) ^ 2) ∧
    ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 <
      533 / 324

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_zeta_three :
  (Summable fun n => 1 / (↑n + 1) ^ 3) ∧
    ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 < 241 / 200

theorem NaturalLatents.General.cap_zeta_three :
  (Summable fun n => 1 / (↑n + 1) ^ 3) ∧
    ∑' (n : ℕ), 1 / (↑n + 1) ^ 3 <
      241 / 200

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.cap_zeta_four :
  (Summable fun n => 1 / (↑n + 1) ^ 4) ∧
    ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 < 6503 / 6000

theorem NaturalLatents.General.cap_zeta_four :
  (Summable fun n => 1 / (↑n + 1) ^ 4) ∧
    ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 <
      6503 / 6000

theoremdefined in NaturalLatents/General/Cap.lean

complete

theorem NaturalLatents.General.gammaPriceCap_log_remainder_le {x : ℝ}
  (hx0 : 0 ≤ x) (hx1 : x < 1) :
  -Real.log (1 - x) - x ≤ x ^ 2 / 2 + x ^ 3 / 3 + x ^ 4 / (4 * (1 - x))

theorem NaturalLatents.General.gammaPriceCap_log_remainder_le
  {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x < 1) :
  -Real.log (1 - x) - x ≤
    x ^ 2 / 2 + x ^ 3 / 3 +
      x ^ 4 / (4 * (1 - x))

Keep the quadratic and cubic terms, then dominate the tail by a geometric series.

Proof for Theorem 5.1.2

uses 0

Bound the first zeta coefficients rationally and dominate the remaining coefficients by a geometric series. See the page section.

Lean: racePrice_lt_capC3b states j(a)<F(a) for every a>1, with F the function gammaPriceCap (NaturalLatents/General/Definitions.lean). It runs through gammaPriceCap_assemble_remainders (the bound in the variable y=1/a) and gammaPriceCap_reciprocal_conversion (multiplication by a), with the zeta bounds cap_zeta_two (\zeta(2)<533/324), cap_zeta_three (\zeta(3)<241/200, from cap_tail_three) and cap_zeta_four (\zeta(4)<6503/6000). cap_zeta_two proves its bound as this page does, from Mathlib's hasSum_zeta_two (\zeta(2)=\pi^2/6) and Real.pi_lt_d4 (\pi<3.1416). Lean bounds \zeta(4) from Mathlib's hasSum_zeta_four (\zeta(4)=\pi^4/90) and \pi^2<9.87, not by the midpoint sum of (K37). Lean bounds the tail term by term rather than through \zeta(k)\le\zeta(4): with x=y/n, gammaPriceCap_log_remainder_le gives -\ln(1-x)-x\le x^2/2+x^3/3+x^4/(4(1-x)), then 1-x\ge1-y, and summing over n gives the same three terms with \zeta(2), \zeta(3) and \zeta(4) as coefficients.