ScheduledArithmeticTransfer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic transfer of the actual original-prior scheduled amplitude

theorem OAI.Ostmann.scheduled_arithmetic_transfer line 14

Source documentation

One genuine step of the schedule, including the original harmonic loss, actual diagonal, all inherited support, and the next copied amplitude.

theorem scheduled_arithmetic_transfer {I A Z : Type*}
    [Fintype I] [Fintype A] [Fintype Z]
    (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
    (κ : I → ℕ → ℂ) (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
    (n r : ℕ) (e : Fin r ≃ CurrentPivotConstituent role n) (hist : A → FrequencyTree ℤ n)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (hκ : ∀ i p, p ∈ P → ‖κ i p‖ ≤ 1)
    (Q : Fin r → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
    (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
    (S : Finset (Fin r → P)) (hS : ∀ x ∈ S, Function.Injective x)
    (T : Finset ℕ) (hT : ∀ M ∈ T, 0 < M) (hST : ∀ x ∈ S, (∏ i, (x i : ℕ)) ∈ T)
    (L : A → CopyScheduleH role n → ℕ) (U : Z → CopyScheduleY role n → ℕ)
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CurrentPivotConstituent, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.CopyScheduleY