OAI/NumberTheory/Ostmann/Construction/WordRootRange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordRangeDecoration.prependRoot line 12
2. theorem OAI.Ostmann.WordRangeDecoration.prependRoot_count line 17
3. theorem OAI.Ostmann.WordRangeDecoration.prependRoot_bounded line 24
4. theorem OAI.Ostmann.WordRangeDecoration.prependRoot_formulas line 41
5. theorem OAI.Ostmann.WordFourierParameters.primeUnitRangedCoefficient_prependRoot line 48
6. theorem OAI.Ostmann.rangedWordTransferPairBound_root_endpoints line 63

   Source documentation

   The finite correlation bound uses only the number of range tests, not its endpoints. Thus the same bound applies uniformly to every root cutoff.

   theorem rangedWordTransferPairBound_root_endpoints {σ : Type*} {n : ℕ}
       (template template' : WordTransferTemplate σ n) (D D' : WordRangeDecoration σ n)
       (r r' : WordRange σ) (t t' : FrequencyTree ℤ n)
       (ht : NonzeroInternalFrequencies n t) (ht' : NonzeroInternalFrequencies n t')
       (B : ℕ) (f f' : WordFourierParameters n) (A E : ℕ)
       (P Q : Finset ℕ) (lower : ℝ) (Bq : ℕ) :
       rangedWordTransferPairBound template template' (D.prependRoot r) D' t t' ht ht' B f f' A E P Q lower Bq =
         rangedWordTransferPairBound template template' (D.prependRoot r') D' t t' ht ht' B f f' A E P Q lower Bq := by
   …

   Mentions: OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.WordRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.WordFourierParameters, OAI.Ostmann.rangedWordTransferPairBound