FiniteScheduledPhase.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Current phase identities with only the finitely used pivot roles

theorem OAI.Ostmann.scheduledInputPhase_factor_finite line 9

theorem OAI.Ostmann.sampledScheduledPhase_factor_finite line 108

Source documentation

Pairwise support on the retained branch and coprimality with the total pivot already imply all the constituent-level cross checks.

theorem sampledScheduledPhase_factor_finite {I : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
    (κ : I → ℕ → ℂ) (pivot : ℕ → I) (n r : ℕ)
    (hpivot : ∀ k ≤ n, role (pivot k) = .pivot k) (e : Fin r ≃ CurrentPivotConstituent role n) (t : FrequencyTree ℤ n)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (x : Fin r → P) (hx : Function.Injective x)
    (L : CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
    [∀ h, Fact (L h).Prime] [∀ y, Fact (U y).Prime]
    (center : ∀ p : ℕ, ZMod p)
    (hLU : Pairwise (fun i j => (Sum.elim L U i).Coprime (Sum.elim L U j)))
    (hM : (∏ i, (x i : ℕ)).Coprime ((∏ h, L h) * ∏ y, U y))
    (hfreq : ∀ i, ∀ s ∈ allFrequencyList n t, (s : ZMod (x i : ℕ)) ≠ 0) :
    sampledScheduledPhase role χ κ pivot n r e t P hP x L U center =
…

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

theorem OAI.Ostmann.scheduledCurrentAmplitude_eq_grouped_finite line 141