OAI/NumberTheory/Ostmann/Construction/GroupedFullPair.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.grouped_full_pair_mean line 13

   Source documentation

   Both histories and any external-integer tests use the same original sample. No new distribution is assigned to reconstructed pivots.

   theorem grouped_full_pair_mean {I V A : Type*} [Fintype I] [Fintype A]
       (role : I → CopyScheduleRole) (n : ℕ)
       (words 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 t' : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
       (ht' : NonzeroInternalFrequencies n t')
       (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b)
       (extra : List (TopPrimeCondition V)) (x : A → V → ℕ) (weight phase : A → ℂ) :
       (∑ a, weight a * (if ∀ c ∈ extra, c.Holds (x a) then
         phase a * (groupedFullCoprimeFourierWeight role n words childBound pivotBound ranges
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.TopPrimeCondition, OAI.Ostmann.groupedFullCoprimeFourierWeight