PrescribedAnalysis.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.slope_lower_of_double_exp line 11

Source documentation

Taking two logarithms converts a double exponential lower bound to a slope bound.

theorem slope_lower_of_double_exp {x c : ℝ} {k : ℕ}
    (hk : 0 < k) (h : Real.exp (Real.exp (c * (k : ℝ))) ≤ x) :
    c ≤ Real.log (Real.log x) / (k : ℝ) := by
…

theorem OAI.Problem337.eventually_slope_lower_of_double_exp line 21

Source documentation

Eventual double exponential bounds lead to eventual lower bounds for the slope.

theorem eventually_slope_lower_of_double_exp (f : ℕ → ℝ) (c : ℝ)
    (h : ∀ᶠ k : ℕ in atTop, Real.exp (Real.exp (c * (k : ℝ))) ≤ f k) :
    ∀ᶠ k : ℕ in atTop, c ≤ Real.log (Real.log (f k)) / (k : ℝ) := by
…

theorem OAI.Problem337.liminf_slope_lower_of_double_exp line 29

Source documentation

The lower limiting slope uses only eventual double exponential lower bounds and boundedness above; no Egyptian fraction constructions enter this step.

theorem liminf_slope_lower_of_double_exp (f : ℕ → ℝ) (A : ℝ)
    (hupper : IsBoundedUnder (· ≤ ·) atTop
      (fun k : ℕ => Real.log (Real.log (f k)) / (k : ℝ)))
    (hlower : ∀ c : ℝ, c < A →
      ∀ᶠ k : ℕ in atTop, Real.exp (Real.exp (c * (k : ℝ))) ≤ f k) :
    A ≤ liminf (fun k : ℕ => Real.log (Real.log (f k)) / (k : ℝ)) atTop ∧
    liminf (fun k : ℕ => Real.log (Real.log (f k)) / (k : ℝ)) atTop ≤
      limsup (fun k : ℕ => Real.log (Real.log (f k)) / (k : ℝ)) atTop := by
…

theorem OAI.Problem337.one_div_six_hundred_lt_prescribed_rate line 48
Source documentation
A coarse elementary bound for log 2 is enough for the stated constant 600.
```
theorem one_div_six_hundred_lt_prescribed_rate :
    (1 : ℝ) / 600 < Real.log 2 / 257 := by
…
```

theorem OAI.Problem337.eventually_double_exp_six_hundred line 55

Source documentation

Specialization of the family of rates to the explicit constant in the corollary.

theorem eventually_double_exp_six_hundred (f : ℕ → ℝ)
    (h : ∀ c : ℝ, c < Real.log 2 / 257 →
      ∀ᶠ k : ℕ in atTop, Real.exp (Real.exp (c * (k : ℝ))) ≤ f k) :
    ∀ᶠ k : ℕ in atTop, Real.exp (Real.exp ((k : ℝ) / 600)) ≤ f k := by
…