OAI/NumberTheory/EgyptianFractions/DensityParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.dense_preparation_ranges line 10

   Source documentation

   Exponential ranges in the elementary passage from density to all numerators. The constants are exactly D_X = D_M + 2 and D_C = 4 D_X.

   theorem dense_preparation_ranges (DM S : ℝ) (hDM : 1 < DM) (hS : 1 ≤ S) :
       1 < Real.exp (4 * (DM + 2) * S) ∧
       Real.exp S < Real.exp (4 * (DM + 2) * S) ∧
       4 < Real.exp ((DM + 2) * S) ∧
       (Real.exp (4 * (DM + 2) * S)) ^ 2 =
         Real.exp (2 * (4 * (DM + 2)) * S) ∧
       (∀ A M : ℝ, 0 ≤ A → A ≤ Real.exp S →
         0 ≤ M → M ≤ Real.exp (DM * S) →
         A * M ≤ Real.exp ((DM + 2) * S)) := by
   …

2. theorem OAI.Problem337.eventually_dense_preparation_ranges line 41

   Source documentation

   A simultaneous eventual cutoff for all elementary density-parameter requirements and a supplied lower threshold on log b.

   theorem eventually_dense_preparation_ranges (DM S0 : ℝ) (hDM : 1 < DM) :
       ∃ b0 : ℕ, ∀ b : ℕ, b0 ≤ b →
         2 ≤ b ∧ S0 ≤ Real.log (b : ℝ) ∧ 1 ≤ Real.log (b : ℝ) ∧
         (b : ℝ) < Real.exp (4 * (DM + 2) * Real.log (b : ℝ)) ∧
         4 < Real.exp ((DM + 2) * Real.log (b : ℝ)) := by
   …