OAI/NumberTheory/Ostmann/Arithmetic/MovingSmoothPolynomials.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSmoothPolynomialFactors line 11
2. theorem OAI.Ostmann.movingSmoothPolynomialFactors_value line 20
3. theorem OAI.Ostmann.movingSmoothPolynomialFactors_budget line 34
4. theorem OAI.Ostmann.movingSmoothPolynomialFactors_variation line 57

   Source documentation

   The complete smooth family uses only the Fourier leaves' derivative roots. Logarithmic node cutoffs add no cuts and no large-center factor.

   theorem movingSmoothPolynomialFactors_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)) (φ : ℝ → ℝ)
       (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
       (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|) :
       ∃ S : Finset ℝ, S.card ≤ 2 ^ n ∧ ∀ (u : ℕ → ℝ), Monotone u → ∀ N : ℕ,
         rootCellCode S (u 0) = rootCellCode S (u (N - 1)) →
         discreteVariation (fun j => smoothPolynomialWeight
           (movingSmoothPolynomialFactors value T L R ψ X lo hi hlo hhi φ G B D hB hD hφ hlip) (u j)) N ≤
         movingFourierVariationBudget ψ V lo hi n * (2 * B + D * (Real.exp 2 - 1)) ^ (2 ^ n - 1) := by
   …

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