OAI/NumberTheory/Ostmann/Characters/CharacterConstructedTargetCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_exp_linear_allowance line 11
2. theorem OAI.Ostmann.eventual_constructed_character_target_cutoff line 45

   Source documentation

   The cutoff is uniform over the selected anchors, bin and original floor length.

   theorem eventual_constructed_character_target_cutoff (k : ℕ) (hk : 0 < k)
       (B z α β βg c : ℝ) (hB : 0 ≤ B) (hz : 1 ≤ z) (hα : 0 < α)
       (hβ : 0 ≤ β) (hβg : β < βg) (hc : 0 ≤ c) :
       ∀ᶠ L : ℝ in atTop, ∀ (U τ J : ℝ) (m : ℕ) (a : Fin k → Bool → ℕ),
         α * L ≤ U → U ≤ β * L → U ≤ Real.log τ →
         Real.log τ ≤ U + 2 * (k : ℝ) / 10000 → 0 < τ →
         (m : ℝ) ≤ z * L → τ / 2 ≤ J → J ≤ 4 * τ →
         (∀ j, (a j false : ℝ) + a j true ≤ 4 * τ) →
         ∀ j, characterPivotTarget k J (fun j => (a j false : ℝ) + a j true)
           (fun j => characterPivotGap B z m j.val) j + c ≤ Real.exp (βg * L) := by
   …

   Mentions: OAI.Ostmann.characterPivotTarget, OAI.Ostmann.characterPivotGap