OAI/NumberTheory/Ostmann/Construction/WordRangePolynomial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordRangeDecoration.rangeAt line 13
2. theorem OAI.Ostmann.WordRangeDecoration.rangeAt_mem line 18
3. theorem OAI.Ostmann.WordRangeDecoration.rangeAt_all line 23
4. def OAI.Ostmann.WordRangeDecoration.polynomials line 36
5. theorem OAI.Ostmann.WordRangeDecoration.polynomials_iff line 44
6. theorem OAI.Ostmann.WordRangeDecoration.polynomials_degree line 54
7. theorem OAI.Ostmann.guardedHistoryAmplitude_extra line 72

   Source documentation

   Adding a finite polynomial support family does not change the smooth factor or any arithmetic residue condition.

   theorem guardedHistoryAmplitude_extra {σ I : Type*} [Fintype I] {n t u : ℕ}
       (N : I → MvPolynomial σ ℤ) (d : I → ℤ) (s : I → ℕ) (a : σ → ℤ) (coord : σ)
       (F : Fin n → ClippedPolynomialFactor) (H : Fin t → Polynomial ℝ) (J : Fin u → Polynomial ℝ)
       (keep : (Fin t → Bool) → Bool) (extra : (Fin u → Bool) → Bool) (z : ℤ) :
       guardedHistoryAmplitude N d s a coord F (Fin.append H J) (pairedPolynomialKeep keep extra) z =
         (if extra (polynomialSupportCode J (z : ℝ)) = true then 1 else 0) *
           guardedHistoryAmplitude N d s a coord F H keep z := by
   …

   Mentions: OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.guardedHistoryAmplitude, OAI.Ostmann.pairedPolynomialKeep, OAI.Ostmann.polynomialSupportCode

8. def OAI.Ostmann.WordFourierParameters.rangedPolynomials line 93
9. def OAI.Ostmann.WordFourierParameters.rangedKeep line 98
10. theorem OAI.Ostmann.WordFourierParameters.rangedCoefficient_local line 103
11. theorem OAI.Ostmann.WordFourierParameters.ranged_complexity_bound line 115