OAI/NumberTheory/Ostmann/Characters/PolynomialRangeGuards.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.polynomialRangeBounds line 11
2. def OAI.Ostmann.polynomialRangeKeep line 16
3. theorem OAI.Ostmann.polynomialRangeKeep_iff line 19
4. theorem OAI.Ostmann.polynomialAmplitude_range line 28

   Source documentation

   The clipped extension agrees exactly with the original smooth factors multiplied by their sharp argument-range indicator.

   theorem polynomialAmplitude_range {n : ℕ} (F : Fin n → ClippedPolynomialFactor) (x : ℝ) :
       polynomialAmplitude F (polynomialRangeBounds F) (polynomialRangeKeep n) x =
         (if ∀ i, (F i).polynomial.eval x ∈ Set.Icc (F i).lo (F i).hi then (1 : ℂ) else 0) *
           ∏ i, (F i).profile ((F i).polynomial.eval x) := by
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.polynomialAmplitude, OAI.Ostmann.polynomialRangeBounds, OAI.Ostmann.polynomialRangeKeep

5. theorem OAI.Ostmann.polynomialRangeBounds_degree_sum line 40
6. theorem OAI.Ostmann.polynomialRange_complexity line 58