OAI/NumberTheory/Ostmann/Construction/GroupedScheduleCoefficient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.expandedPrimeNatValues line 11
2. theorem OAI.Ostmann.expandedPrimeNatValues_cast line 15
3. def OAI.Ostmann.groupedScheduleFourierWeight line 21
4. theorem OAI.Ostmann.groupedScheduleFourierWeight_coefficient line 30
5. theorem OAI.Ostmann.groupedScheduleFourierWeight_pair_mean line 51

   Source documentation

   The entire original expectation is preserved; no tuple normalization or probability law is introduced for the reconstructed pivot coordinates.

   theorem groupedScheduleFourierWeight_pair_mean {I V A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (n : ℕ) (words words' : CopyScheduleAtoms role n → List V)
       (childBound pivotBound : ℕ → ℕ) (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y)
       (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (t t' : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (ht' : NonzeroInternalFrequencies n t')
       (x : A → V → ℕ) (weight phase : A → ℂ) :
       (∑ a, weight a * (phase a *
         (groupedScheduleFourierWeight role n words childBound pivotBound ψ X lo hi t (x a) *
           conj (groupedScheduleFourierWeight role n words' childBound pivotBound ψ X lo hi t' (x a))))) =
       ∑ a, weight a * (phase a *
         ((WordFourierParameters.uniform n (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).coefficient
           (expandedRootTemplate role n words childBound pivotBound) t ht
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.groupedScheduleFourierWeight, OAI.Ostmann.WordFourierParameters.uniform, OAI.Ostmann.expandedRootTemplate