OAI/NumberTheory/Ostmann/Construction/InsertedConstituentFourier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.inserted_full_fourier_eq_grouped line 11
2. theorem OAI.Ostmann.inserted_full_fourier_permuted line 30
3. theorem OAI.Ostmann.constituentUnweighted_fourier_eq_grouped line 53
4. theorem OAI.Ostmann.constituentUnweighted_permuted_fourier_eq_grouped line 73
5. theorem OAI.Ostmann.insertedExpandedTemplate_size line 111
6. theorem OAI.Ostmann.inserted_full_fourier_coefficient line 121

   Source documentation

   The fixed pivot is a constant coordinate of the exact word formula; it receives no prime marginal. All inherited coprimality and interval tests remain.

   theorem inserted_full_fourier_coefficient {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, starRingEnd ℂ (ψ y) = ψ y)
       (X lo hi : ℝ) (hlo : 1 ≤ lo) (hhi : lo ≤ hi)
       (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t) (M : ℕ)
       (l : CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → ℕ)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → ℕ)
       (hu : ∀ j < n, ∀ a b, role a = .pivot j → role b = .pivot j → a = b) :
       let words := insertedConstituentWord role size n
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.insertedConstituentWord