OAI/NumberTheory/Ostmann/Construction/FullHistoryGuards.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.fullHistoryPolynomials line 12
2. def OAI.Ostmann.fullHistoryKeep line 16
3. theorem OAI.Ostmann.fullHistoryAmplitude_factor line 20
4. theorem OAI.Ostmann.fullHistoryAmplitude_exact line 38

   Source documentation

   The extension agrees with every original range/bin restriction, including boundary points, before the one-sided cancellation estimate is invoked.

   theorem fullHistoryAmplitude_exact {n t : ℕ} (F : Fin n → ClippedPolynomialFactor)
       (H : Fin t → Polynomial ℝ) (keep : (Fin t → Bool) → Bool) (x : ℝ) :
       polynomialAmplitude F (fullHistoryPolynomials F H) (fullHistoryKeep keep) x =
         (if keep (polynomialSupportCode H x) = true ∧
           ∀ 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.fullHistoryPolynomials, OAI.Ostmann.fullHistoryKeep, OAI.Ostmann.polynomialSupportCode

5. theorem OAI.Ostmann.fullHistoryPolynomials_complexity line 47
6. theorem OAI.Ostmann.guardedHistoryAmplitude_norm line 56