RangedPairNumericBudget.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit numerical costs of the two actual ranged word histories

def OAI.Ostmann.rangedPairExponent line 14
theorem OAI.Ostmann.rangedPairExponent_nonneg line 19

theorem OAI.Ostmann.ranged_pair_numeric_costs line 27

Source documentation

The period, Boolean partition, Fourier variation and harmonic normalizers all have a common explicit polynomial exponent.

theorem ranged_pair_numeric_costs {σ : Type*} {n : ℕ}
    (T T' : WordTransferTemplate σ n) (D D' : WordRangeDecoration σ n)
    (t t' : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
    (ht' : NonzeroInternalFrequencies n t')
    (B V E : ℕ) (f f' : WordFourierParameters n) (P Q : Finset ℕ)
    (b d C S H m : ℝ) (hb : 0 ≤ b) (hd : 0 ≤ d) (hC : 0 ≤ C)
    (hS : 1 ≤ S) (hH : 0 ≤ H) (hm : 0 ≤ m)
    (hB : (B : ℝ) ≤ b * (1 + m))
    (hD : (D.count : ℝ) ≤ d * (1 + m)) (hD' : (D'.count : ℝ) ≤ d * (1 + m))
    (hV : (V : ℝ) ≤ Real.exp (C * (1 + m)))
    (hf : ∀ s ∈ allFrequencyList n t, s.natAbs ≤ V)
    (hf' : ∀ s ∈ allFrequencyList n t', s.natAbs ≤ V)
…

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

theorem OAI.Ostmann.dyadic_shell_linear_exponential line 134

Source documentation

The dyadic shell count uses only a double-exponential endpoint bound; its own cost is singly exponential in the word length.

theorem dyadic_shell_linear_exponential (E : ℕ) (C m : ℝ)
    (hC : 0 ≤ C) (hm : 0 ≤ m)
    (hE : (E : ℝ) ≤ Real.exp (Real.exp (C * (1 + m)))) :
    ((Nat.log 2 E + 1 : ℕ) : ℝ) ≤
      Real.exp ((2 + 1 / Real.log 2 + C) * (1 + m)) := by
…