OAI/NumberTheory/Ostmann/Construction/ConstituentFourierBridge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.constituentExpandedTemplate_size line 12
2. theorem OAI.Ostmann.constituent_top_checks line 22
3. theorem OAI.Ostmann.constituent_full_weight_coefficient line 33

   Source documentation

   The top support of the original constituent assignment is exactly the support used by the grouped Fourier development. No independent atom sample or replacement distribution is introduced.

   theorem constituent_full_weight_coefficient {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (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)
       (q : SurvivingConstituent role size n → ℕ)
       (hq : Pairwise (fun i j => (q i).Coprime (q j)))
       (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b) :
       groupedFullCoprimeFourierWeight role n (scheduleConstituentWord role size n)
         childBound pivotBound ranges ψ X lo hi t q =
       (WordFourierParameters.uniform n (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).primeUnitRangedCoefficient
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.groupedFullCoprimeFourierWeight, OAI.Ostmann.scheduleConstituentWord, OAI.Ostmann.WordFourierParameters.uniform