OAI/NumberTheory/Ostmann/Arithmetic/MovingFourierVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingSlotData.leafFrequencies_bound line 10
2. def OAI.Ostmann.movingFourierVariationBudget line 20
3. theorem OAI.Ostmann.movingFourierPolynomialFactors_budget line 25
4. theorem OAI.Ostmann.movingFourierPolynomialFactors_variation line 52

   Source documentation

   At most one derivative root per terminal quadratic is needed. Both the root cut set and the variation bound are built from the actual history.

   theorem movingFourierPolynomialFactors_variation {σ : Type*} (value : σ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
       (X lo hi V : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (hL : L.natDegree ≤ 1) (hR : R.natDegree ≤ 1)
       (hV : T.Frequencies (fun s => |(s : ℝ)| ≤ V)) :
       ∃ S : Finset ℝ, S.card ≤ 2 ^ n ∧
         ∀ (u : ℕ → ℝ), Monotone u → ∀ N : ℕ,
           rootCellCode S (u 0) = rootCellCode S (u (N - 1)) →
           discreteVariation (fun j => smoothPolynomialWeight
             (movingFourierPolynomialFactors value T L R ψ X lo hi hlo hhi) (u j)) N ≤
               movingFourierVariationBudget ψ V lo hi n := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.rootCellCode, OAI.Ostmann.discreteVariation, OAI.Ostmann.smoothPolynomialWeight, OAI.Ostmann.movingFourierPolynomialFactors, OAI.Ostmann.movingFourierVariationBudget