OAI/Analysis/LpDimension/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SubpolynomialLp.source_main line 13

   Source documentation

   The universal coordinate dimension bounds and their logarithmic limits.

   Distinct definitions of this name: ComparatorChallenges/SubpolynomialLp.lean:32 (same statement text; different proof or body). Qualify references as OAI.SubpolynomialLp.source_main@path.

   theorem source_main (p : ℝ) (hp : 1 < p) (hp2 : p ≠ 2) :
       (∀ D : ℝ, 1 < D → ∃ C : ℝ, ∀ n : ℕ, 2 ≤ n →
         GoodDimension.{u} p n D (dimension.{u} p n D) ∧
         Real.log (n : ℝ) / Real.log (1 + 2 * D) ≤ (dimension.{u} p n D : ℝ) ∧
         (dimension.{u} p n D : ℝ) ≤ Real.exp (C * Real.log (n : ℝ) ^ gamma p)) ∧
       (∀ n : ℕ, 9 ≤ n →
         GoodDimension.{u} p n 1 (dimension.{u} p n 1) ∧
         ((n - 1) / 4) ^ 2 ≤ dimension.{u} p n 1 ∧
         dimension.{u} p n 1 ≤ n.choose 2) ∧
       (∀ D : ℝ, 1 ≤ D →
         Tendsto (fun n : ℕ => Real.log (dimension.{u} p n D : ℝ) / Real.log (n : ℝ))
           atTop (𝓝 (if 1 < D then 0 else 2))) := by
   …

   Mentions: OAI.SubpolynomialLp.gamma