OAI/NumberTheory/Ostmann/Arithmetic/RangedPairParameterDecay.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.eventual_ranged_pair_decay_from_data line 12

   Source documentation

   Explicit size bounds control all arithmetic costs, so separated prime scales give the required error without a numerical cancellation assumption.

   theorem eventual_ranged_pair_decay_from_data {σ : Type*} (n : ℕ)
       (b d C S H z α β γ c : ℝ)
       (hb : 0 ≤ b) (hd : 0 ≤ d) (hC : 0 ≤ C) (hS : 1 ≤ S) (hH : 0 ≤ H)
       (hz : 0 ≤ z) (hα : 0 < α) (hαβ : α < β) (hγβ : γ < β) (hc : 0 < c) :
       ∀ᶠ L : ℝ in atTop, ∀
         (T T' : WordTransferTemplate σ n) (D D' : WordRangeDecoration σ n)
         (t t' : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
         (ht' : NonzeroInternalFrequencies n t')
         (B V A E : ℕ) (f f' : WordFourierParameters n) (P Q : Finset ℕ)
         (lower : ℝ) (Bq : ℕ) (m : ℝ),
         0 ≤ m → m ≤ z * L →
         (B : ℝ) ≤ b * (1 + m) →
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.WordFourierParameters