OAI/NumberTheory/Ostmann/Construction/PrimeWordCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordFourierParameters.primeUnitRangedCoefficient line 12
2. theorem OAI.Ostmann.WordFourierParameters.primeUnitRangedCoefficient_norm line 22
3. theorem OAI.Ostmann.WordFourierParameters.primeUnitRangedCoefficient_nat line 36

   Source documentation

   This identity also covers invalid histories: both coefficients vanish.

   theorem primeUnitRangedCoefficient_nat {V : Type*} {n : ℕ} (p : WordFourierParameters n)
       (C : WordPrimeDecoration V n)
       (U D : WordRangeDecoration (ExpandedScheduledVariable V n) n)
       (template : WordTransferTemplate (ExpandedScheduledVariable V n) n)
       (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (x : V → ℕ) :
       p.primeUnitRangedCoefficient C U D template t ht x =
         (if C.ValidAt template (expandedPrimeNatValues n x) x t then 1 else 0) *
           p.unitRangedCoefficient U D template t ht (expandedPrimeValues n (fun i => (x i : ℤ))) := by
   …

   Mentions: OAI.Ostmann.WordFourierParameters, OAI.Ostmann.WordPrimeDecoration, OAI.Ostmann.WordRangeDecoration, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.expandedPrimeNatValues, OAI.Ostmann.expandedPrimeValues