ChebyshevLowerSharp.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.ChebyshevLowerSharp.floor_kernel_bounds line 13
Source documentation
Chebyshev's periodic floor kernel takes only the values zero and one.
```
lemma floor_kernel_bounds (n : ℕ) :
    n / 2 + n / 3 + n / 5 ≤ n + n / 30 ∧
      n + n / 30 ≤ 1 + n / 2 + n / 3 + n / 5 := by
…
```
lemma OAI.Problem337.ChebyshevLowerSharp.log_factorial_eq_sum_log line 18
lemma OAI.Problem337.ChebyshevLowerSharp.log_factorial_eq_mangoldt_sum line 29
Source documentation
A finite summatory von Mangoldt identity, including the floor weights.
```
lemma log_factorial_eq_mangoldt_sum (n : ℕ) :
    Real.log (n.factorial : ℝ) =
      ∑ d ∈ Ioc 0 n, (n / d : ℕ) * vonMangoldt d := by
…
```

lemma OAI.Problem337.ChebyshevLowerSharp.log_factorial_eq_mangoldt_sum_of_le line 60

Source documentation

The summatory identity may be extended to any larger finite interval.

lemma log_factorial_eq_mangoldt_sum_of_le {n N : ℕ} (hnN : n ≤ N) :
    Real.log (n.factorial : ℝ) =
      ∑ d ∈ Ioc 0 N, (n / d : ℕ) * vonMangoldt d := by
…

theorem OAI.Problem337.ChebyshevLowerSharp.factorial_combination_le_psi line 73

Source documentation

A finite stronger Chebyshev lower bound. The alternating factorial combination is bounded above by the actual von Mangoldt summatory function.

theorem factorial_combination_le_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 := by
…

lemma OAI.Problem337.ChebyshevLowerSharp.log_factorial_error_tendsto_zero line 97

Source documentation

The linear-scale error in the logarithmic factorial estimate vanishes.

lemma log_factorial_error_tendsto_zero :
    Tendsto (fun n : ℕ =>
      (Real.log (n.factorial : ℝ) - (n : ℝ) * Real.log n + n) / n)
      atTop (nhds 0) := by
…

lemma OAI.Problem337.ChebyshevLowerSharp.scaled_log_factorial_tendsto line 120

Source documentation

A scaled version with the common divergent logarithm subtracted.

lemma scaled_log_factorial_tendsto (a : ℕ) (ha : 0 < a) :
    Tendsto (fun n : ℕ =>
      Real.log ((a * n).factorial : ℝ) / n - (a : ℝ) * Real.log n)
      atTop (nhds ((a : ℝ) * Real.log a - a)) := by
…

def OAI.Problem337.ChebyshevLowerSharp.lowerConstant line 139
Source documentation
Chebyshev's classical elementary lower constant, approximately 0.92129.
```
def lowerConstant : ℝ :=
…
```
lemma OAI.Problem337.ChebyshevLowerSharp.lowerConstant_eq line 142
lemma OAI.Problem337.ChebyshevLowerSharp.lowerConstant_gt_921_div_1000 line 151
def OAI.Problem337.ChebyshevLowerSharp.factorialBlock line 162
lemma OAI.Problem337.ChebyshevLowerSharp.factorialBlock_le_psi line 167
lemma OAI.Problem337.ChebyshevLowerSharp.factorialBlock_tendsto line 175
lemma OAI.Problem337.ChebyshevLowerSharp.factorialBlock_div_tendsto line 203
Source documentation
Rescaling the 30-blocks loses only a bounded endpoint discrepancy.
```
lemma factorialBlock_div_tendsto :
    Tendsto (fun N : ℕ => factorialBlock (N / 30) / N)
      atTop (nhds lowerConstant) := by
…
```
Mentions: OAI.Problem337.ChebyshevLowerSharp.factorialBlock, OAI.Problem337.ChebyshevLowerSharp.lowerConstant
theorem OAI.Problem337.ChebyshevLowerSharp.eventually_psi_lower line 236
Source documentation
Every coefficient below the classical Chebyshev constant is an eventual lower coefficient for the actual von Mangoldt summatory function.
```
theorem eventually_psi_lower {c : ℝ} (hc : c < lowerConstant) :
    ∀ᶠ N : ℕ in atTop, c * N ≤ Chebyshev.psi N := by
…
```
Mentions: OAI.Problem337.ChebyshevLowerSharp.lowerConstant
theorem OAI.Problem337.ChebyshevLowerSharp.eventually_primeCounting_lower line 250
Source documentation
An unconditional prime-count lower bound with every coefficient below 0.92129...; no prime number theorem is used.
```
theorem eventually_primeCounting_lower {c : ℝ} (hc : c < lowerConstant) :
    ∀ᶠ N : ℕ in atTop, c * N / Real.log N ≤ (Nat.primeCounting N : ℝ) := by
…
```
Mentions: OAI.Problem337.ChebyshevLowerSharp.lowerConstant
theorem OAI.Problem337.ChebyshevLowerSharp.eventually_primeCounting_lower_092 line 257
def OAI.Problem337.ChebyshevLowerSharp.factorialCombination line 264
Source documentation
The unblocked finite factorial expression.
```
def factorialCombination (N : ℕ) : ℝ :=
…
```
lemma OAI.Problem337.ChebyshevLowerSharp.log_factorial_gap line 269
lemma OAI.Problem337.ChebyshevLowerSharp.factorialCombination_sub_block_abs_le line 300
Source documentation
Passing from a multiple of thirty to an arbitrary endpoint costs only a logarithmic error.
```
lemma factorialCombination_sub_block_abs_le {N : ℕ} (hN : 1 ≤ N) :
    |factorialCombination N - factorialBlock (N / 30)| ≤ 120 * Real.log N := by
…
```
Mentions: OAI.Problem337.ChebyshevLowerSharp.factorialCombination, OAI.Problem337.ChebyshevLowerSharp.factorialBlock
theorem OAI.Problem337.ChebyshevLowerSharp.factorialCombination_div_tendsto line 316
Source documentation
The full, unblocked factorial combination has the same sharp coefficient.
```
theorem factorialCombination_div_tendsto :
    Tendsto (fun N : ℕ => factorialCombination N / N)
      atTop (nhds lowerConstant) := by
…
```
Mentions: OAI.Problem337.ChebyshevLowerSharp.factorialCombination, OAI.Problem337.ChebyshevLowerSharp.lowerConstant