WordFourierBudgetBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit Fourier variation bounds from the actual frequency range

theorem OAI.Ostmann.WordTransferTemplate.weightedLeaves_frequency_mem line 11
theorem OAI.Ostmann.WordFourierParameters.frequency_abs_le line 28
theorem OAI.Ostmann.WordFourierParameters.budget_le line 38

theorem OAI.Ostmann.WordFourierParameters.budget_le_exp line 70

Source documentation

All variation loss is exponential in the original linear frequency and bin bounds, uniformly in the reconstructed integers and polynomial coefficients.

theorem WordFourierParameters.budget_le_exp {σ : Type*} {n : ℕ}
    (p : WordFourierParameters n) (template : WordTransferTemplate σ n)
    (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
    (S C m : ℝ) (hS : 1 ≤ S) (hC : 0 ≤ C) (hm : 0 ≤ m)
    (hS₀ : SchwartzMap.seminorm ℝ 0 0 p.profile ≤ S)
    (hS₁ : SchwartzMap.seminorm ℝ 0 1 p.profile ≤ S)
    (hf : ∀ s ∈ allFrequencyList n t, |(s : ℝ)| ≤ Real.exp (C * (1 + m)))
    (hr : ∀ i, p.upper i - p.lower i ≤ Real.exp (C * (1 + m))) :
    p.budget template t ht ≤ Real.exp (((4 * S + 2 * C) * (2 ^ n : ℕ)) * (1 + m)) := by
…

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