MovingFourierBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-depth cost of the constructed Fourier variation bound

theorem OAI.Ostmann.movingFourierVariationBudget_exp line 13

Source documentation

Frequencies of size exp(O(m)) give a variation cost exp(O(m)). The constant is chosen before the bulk size and both top giant coordinates.

theorem movingFourierVariationBudget_exp (ψ : 𝓢(ℝ, ℂ)) (n : ℕ)
    (A lo hi : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) :
    ∃ C : ℝ, 0 < C ∧ ∀ m : ℝ, 0 ≤ m →
      movingFourierVariationBudget ψ (Real.exp (A * m)) lo hi n ≤ Real.exp (C * (m + 1)) := by
…

Mentions: OAI.Ostmann.movingFourierVariationBudget

theorem OAI.Ostmann.movingFourierVariationBudget_exp_window line 48

Source documentation

Uniform in moving endpoints whose width has the actual exponential scale.

theorem movingFourierVariationBudget_exp_window (ψ : 𝓢(ℝ, ℂ)) (n : ℕ)
    (A H : ℝ) (hA : 0 ≤ A) (hH : 0 ≤ H) :
    ∃ C : ℝ, 0 < C ∧ ∀ m : ℝ, 0 ≤ m → ∀ lo hi : ℝ, lo ≤ hi →
      hi - lo ≤ Real.exp (H * m) →
      movingFourierVariationBudget ψ (Real.exp (A * m)) lo hi n ≤
        Real.exp (C * (m + 1)) := by
…

Mentions: OAI.Ostmann.movingFourierVariationBudget