OAI/NumberTheory/Ostmann/Construction/GroupedUnitCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.groupedUnitRangedFourierWeight line 12
2. theorem OAI.Ostmann.groupedUnitRangedFourierWeight_coefficient line 22

   Source documentation

   Each actual atom is a unit modulo the frequency of every state in which it occurs. These conditions remain inside the exact polynomial coefficient.

   theorem groupedUnitRangedFourierWeight_coefficient {I V : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (n : ℕ) (words : CopyScheduleAtoms role n → List V)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y)
       (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (x : V → ℕ) :
       groupedUnitRangedFourierWeight role n words childBound pivotBound ranges ψ X lo hi t x =
         (WordFourierParameters.uniform n (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).unitRangedCoefficient
           (expandedRootRanges role n words (totalAtomUnitRanges role))
           (expandedRootRanges role n words ranges) (expandedRootTemplate role n words childBound pivotBound)
           t ht (expandedPrimeValues n (fun i => (x i : ℤ))) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.groupedUnitRangedFourierWeight, OAI.Ostmann.WordFourierParameters.uniform, OAI.Ostmann.expandedRootRanges, OAI.Ostmann.totalAtomUnitRanges, OAI.Ostmann.expandedRootTemplate, OAI.Ostmann.expandedPrimeValues