OAI/NumberTheory/Ostmann/Arithmetic/MovingFourierPolynomials.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingLeafIndexEquiv line 12
2. def OAI.Ostmann.MovingSlotData.leafFrequencies line 15
3. theorem OAI.Ostmann.movingPolynomialFourierTree_product line 21
4. def OAI.Ostmann.movingLeafNormalizedPolynomial line 53
5. theorem OAI.Ostmann.movingLeafNormalizedPolynomial_eval line 57
6. def OAI.Ostmann.movingFourierPolynomialFactors line 66

   Source documentation

   Exactly one clipped Fourier polynomial per terminal leaf, with the conjugation imposed by its actual left/right path.

   noncomputable def movingFourierPolynomialFactors {σ : Type*} (value : σ → ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (L R : Polynomial ℝ) (ψ : 𝓢(ℝ, ℂ))
       (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) : Fin (2 ^ n) → ClippedPolynomialFactor :=
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.ClippedPolynomialFactor

7. theorem OAI.Ostmann.movingFourierPolynomialFactors_value line 75
8. theorem OAI.Ostmann.movingFourierPolynomialFactors_degree line 112