OAI/NumberTheory/Ostmann/Construction/ConstituentInitialAmplitude.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.initial_constituent_word_prod line 11
2. theorem OAI.Ostmann.initial_constituent_pairwise line 18
3. def OAI.Ostmann.sampledTuplePhase line 29
4. theorem OAI.Ostmann.scheduledSamplePhase_zero line 37
5. theorem OAI.Ostmann.constituentPrimeGuardedAmplitude_zero line 52

   Source documentation

   This is the original independent prime law, with the full initial range, unit and prime support kept inside the integrand.

   theorem constituentPrimeGuardedAmplitude_zero {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)))
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (hκ : ∀ i (p : P), κ i p =
         @primitiveGaussPhase p.val ⟨(hP p p.property).ne_zero⟩ (χ i p))
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (hist : D → ℤ)
       (center : ∀ p : ℕ, ZMod p) :
       constituentPrimeGuardedAmplitude role size χ κ pivot 0 P hP Q
         childBound pivotBound ranges leaf hist center =
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.primitiveGaussPhase, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.constituentPrimeGuardedAmplitude