OAI/NumberTheory/EgyptianFractions/FejerExponentialBudget.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.FejerParameters.exp_neg_cube line 10
2. lemma OAI.Problem337.FejerParameters.exp_neg_inv_fourth line 15
3. lemma OAI.Problem337.FejerParameters.eventually_fejer_exponential_parameters line 22

   Source documentation

   The purely exponential input to automatic-modulus Fejer localization. There is no restriction on a modulus or on the upper size of the frequency range.

   lemma eventually_fejer_exponential_parameters (η : ℝ) (hη : 0 < η) :
       ∀ᶠ w : ℝ in atTop,
         0 < Real.exp (-η * w) ∧
         Real.exp (-η * w) ≤ 1 / 65536 ∧
         Real.exp (-η * w) ^ 3 = Real.exp (-3 * η * w) ∧
         1 / Real.exp (-η * w) ^ 4 = Real.exp (4 * η * w) := by
   …

4. lemma OAI.Problem337.FejerParameters.eventually_fejer_budget_general line 46

   Source documentation

   A small exponential arc has enough residue points and its Fejer smoothing degree fits below the modulus, uniformly when w ≤ log q.

   lemma eventually_fejer_budget_general (η : ℝ) (hη : 0 < η) (hη3 : η ≤ 1 / 3) :
       ∀ᶠ w : ℝ in atTop, ∀ q : ℕ, w ≤ Real.log (q : ℝ) →
         Real.exp (-η * w) ≤ 1 / 65536 ∧
         128 ≤ Real.exp (-η * w) * (q : ℝ) ∧
         ⌊1 / (64 * Real.exp (-η * w) ^ 3)⌋₊ ≤ q := by
   …

5. lemma OAI.Problem337.FejerParameters.eventually_fejer_budget line 102

   Source documentation

   The precise exponential budget for the paper's value η = 1/10000.

   lemma eventually_fejer_budget :
       ∀ᶠ w : ℝ in atTop, ∀ q : ℕ, w ≤ Real.log (q : ℝ) →
         Real.exp (-(1 / 10000 : ℝ) * w) ≤ 1 / 65536 ∧
         128 ≤ Real.exp (-(1 / 10000 : ℝ) * w) * (q : ℝ) ∧
         ⌊1 / (64 * Real.exp (-(1 / 10000 : ℝ) * w) ^ 3)⌋₊ ≤ q := by
   …