OAI/NumberTheory/Ostmann/Construction/ConstituentCopiedAmplitude.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledCopiedAssignment_map line 11
2. theorem OAI.Ostmann.constituentOriginalAmplitude_copied line 25

   Source documentation

   The next global amplitude has exactly the two H priors and one Y prior appearing after arithmetic transfer. All Fourier and arithmetic support stays inside the same full coefficient.

   theorem constituentOriginalAmplitude_copied {I D : Type*} [Fintype I] [Fintype D]
       (role : I → CopyScheduleRole) (size : I → ℕ)
       (χ : (Σ i, Fin (size i)) → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : (Σ i, Fin (size i)) → ℕ → ℂ) (pivot : ℕ → (Σ i, Fin (size i)))
       (n : ℕ) (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (hist : D → FrequencyTree ℤ (n + 1))
       (center : ∀ p : ℕ, ZMod p) :
       constituentOriginalAmplitude role size χ κ pivot (n + 1) P hP Q
         childBound pivotBound ranges leaf hist center =
       let ρ := fun i : Σ a, Fin (size a) => role i.1
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.constituentOriginalAmplitude