OAI/NumberTheory/Ostmann/Construction/GroupedFullCoprime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.groupedUnitRangedFourierWeight_support line 13
2. def OAI.Ostmann.groupedFullCoprimeFourierWeight line 33
3. theorem OAI.Ostmann.groupedFullCoprimeFourierWeight_reduced line 41
4. theorem OAI.Ostmann.groupedFullCoprimeFourierWeight_coefficient line 62

   Source documentation

   The original large-coprimality gates are represented exactly, even on invalid histories, by the explicit top prime tests and reconstructed Y tests.

   theorem groupedFullCoprimeFourierWeight_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 → ℕ)
       (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b) :
       groupedFullCoprimeFourierWeight role n words childBound pivotBound ranges ψ X lo hi t x =
         if ∀ c ∈ atomPairChecks words, c.Holds x then
           (WordFourierParameters.uniform n (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).primeUnitRangedCoefficient
             (expandedSchedulePrimes role n n [] (fun i => (words i).map Sum.inl))
             (expandedRootRanges role n words (totalAtomUnitRanges role))
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.groupedFullCoprimeFourierWeight, OAI.Ostmann.atomPairChecks, OAI.Ostmann.WordFourierParameters.uniform, OAI.Ostmann.expandedSchedulePrimes, OAI.Ostmann.expandedRootRanges, OAI.Ostmann.totalAtomUnitRanges