OAI/NumberTheory/Ostmann/Construction/ConstituentPrimeGuardedAmplitude.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.constituentPrimeGuardedAmplitude line 13
2. theorem OAI.Ostmann.constituentPrimeGuardedAmplitude_eq_current line 32

   Source documentation

   This identifies the full original-prior expectation, including its actual phase and every history guard, with the amplitude in the proved arithmetic step.

   theorem constituentPrimeGuardedAmplitude_eq_current {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 : I) (hp : role p = .pivot n) (hu : ∀ i, role i = .pivot n → i = p)
       (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)
       (center : ∀ p : ℕ, ZMod p) :
       let ρ := fun i : Σ a, Fin (size a) => role i.1
   …

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

3. theorem OAI.Ostmann.constituentPrimeGuardedAmplitude_eq_transfer line 105

   Source documentation

   The fully guarded original expectation is exactly the amplitude to which the proved arithmetic transfer applies. All prime-support predicates are retained.

   theorem constituentPrimeGuardedAmplitude_eq_transfer {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 : I) (hp : role p = .pivot n) (hu : ∀ i, role i = .pivot n → i = p)
       (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)
       (center : ∀ p : ℕ, ZMod p) :
       let ρ := fun i : Σ a, Fin (size a) => role i.1
   …

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