ChebyshevImprovedLower.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.chebyshev_thirty_weight_bounds line 11

Source documentation

Chebyshev's thirty-periodic floor combination takes only the values zero and one. This is the finite arithmetic behind the improved lower constant.

theorem chebyshev_thirty_weight_bounds (n : ℕ) :
    0 ≤ (n : ℤ) - (n / 2 : ℕ) - (n / 3 : ℕ) - (n / 5 : ℕ) + (n / 30 : ℕ) ∧
    (n : ℤ) - (n / 2 : ℕ) - (n / 3 : ℕ) - (n / 5 : ℕ) + (n / 30 : ℕ) ≤ 1 := by
…

theorem OAI.Problem337.log_factorial_eq_sum_mangoldt_div line 18
Source documentation
The factorial logarithm is a finite Mangoldt sum with floor weights; the outer range may be any larger initial interval.
```
theorem log_factorial_eq_sum_mangoldt_div {m N : ℕ} (hm : m ≤ N) :
    Real.log (m.factorial : ℝ) =
      ∑ d ∈ Finset.range (N + 1), Λ d * ((m / d : ℕ) : ℝ) := by
…
```

theorem OAI.Problem337.chebyshev_psi_ge_factorial_combination line 51

Source documentation

An explicit elementary lower bound for ψ, stronger asymptotically than the single central-binomial-coefficient bound.

theorem chebyshev_psi_ge_factorial_combination (N : ℕ) :
    Real.log (N.factorial : ℝ) - Real.log ((N / 2).factorial : ℝ) -
      Real.log ((N / 3).factorial : ℝ) - Real.log ((N / 5).factorial : ℝ) +
      Real.log ((N / 30).factorial : ℝ) ≤ Chebyshev.psi N := by
…

theorem OAI.Problem337.chebyshev_psi_ge_floor_factorial_combination line 80

Source documentation

The same factorial lower bound at real endpoints, ready for asymptotic use without any rounding or integrality hypothesis.

theorem chebyshev_psi_ge_floor_factorial_combination (x : ℝ) :
    Real.log (⌊x⌋₊.factorial : ℝ) - Real.log (⌊x / 2⌋₊.factorial : ℝ) -
      Real.log (⌊x / 3⌋₊.factorial : ℝ) - Real.log (⌊x / 5⌋₊.factorial : ℝ) +
      Real.log (⌊x / 30⌋₊.factorial : ℝ) ≤ Chebyshev.psi x := by
…

theorem OAI.Problem337.chebyshev_psi_nat_sum_indicator line 89

Source documentation

Extending a Mangoldt prefix to a larger range by an indicator.

theorem chebyshev_psi_nat_sum_indicator {m N : ℕ} (hm : m ≤ N) :
    Chebyshev.psi m = ∑ d ∈ Finset.range (N + 1), if d ≤ m then Λ d else 0 := by
…

theorem OAI.Problem337.chebyshev_psi_le_factorial_combination_add line 102

Source documentation

The complementary upper recurrence from the same thirty-periodic kernel. Iteration gives the classical upper Chebyshev constant 6C/5.

theorem chebyshev_psi_le_factorial_combination_add (N : ℕ) :
    Chebyshev.psi N ≤
      Real.log (N.factorial : ℝ) - Real.log ((N / 2).factorial : ℝ) -
        Real.log ((N / 3).factorial : ℝ) - Real.log ((N / 5).factorial : ℝ) +
        Real.log ((N / 30).factorial : ℝ) + Chebyshev.psi (N / 6 : ℕ) := by
…

theorem OAI.Problem337.chebyshev_psi_le_floor_factorial_combination_add line 145

Source documentation

Real-endpoint form of the complementary upper recurrence.

theorem chebyshev_psi_le_floor_factorial_combination_add (x : ℝ) :
    Chebyshev.psi x ≤
      Real.log (⌊x⌋₊.factorial : ℝ) - Real.log (⌊x / 2⌋₊.factorial : ℝ) -
        Real.log (⌊x / 3⌋₊.factorial : ℝ) - Real.log (⌊x / 5⌋₊.factorial : ℝ) +
        Real.log (⌊x / 30⌋₊.factorial : ℝ) + Chebyshev.psi (x / 6) := by
…