OAI/NumberTheory/Ostmann/Construction/ExpandedRangedWeight.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.expanded_schedule_ranged_weight_eq line 12
2. def OAI.Ostmann.expandedRootRanges line 32
3. def OAI.Ostmann.groupedRangedFourierWeight line 38
4. theorem OAI.Ostmann.groupedRangedFourierWeight_coefficient line 47

   Source documentation

   The actual grouped-atom weight with all intermediate product and word bins is the coefficient used by the ranged one-sided bound.

   theorem groupedRangedFourierWeight_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 → ℕ) :
       groupedRangedFourierWeight role n words childBound pivotBound ranges ψ X lo hi t x =
         (WordFourierParameters.uniform n (𝓕 ψ : 𝓢(ℝ, ℂ)) X lo hi hlo hhi).rangedCoefficient
           (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.groupedRangedFourierWeight, OAI.Ostmann.WordFourierParameters.uniform, OAI.Ostmann.expandedRootRanges, OAI.Ostmann.expandedRootTemplate, OAI.Ostmann.expandedPrimeValues