OAI/NumberTheory/Ostmann/Construction/ScheduledGroupedPhase.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduledPrimePhase_factor_pivot line 16

   Source documentation

   The arithmetic factorization uses every actual pivot constituent and all retained slots. Its row and column conditions are proved from the schedule.

   theorem scheduledPrimePhase_factor_pivot {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (κ : I → ℕ → ℂ) (pivot : ℕ → I) (hpivot : ∀ k, role (pivot k) = .pivot k)
       (n : ℕ) (t : FrequencyTree ℤ n)
       (q : {i : CopyScheduleVertex I n // CopyScheduleSurvives role n i} → ℕ)
       [∀ i, Fact (q i).Prime] (center : ∀ p : ℕ, ZMod p)
       (hc : Pairwise (fun i j => (q i).Coprime (q j)))
       (hfreq : ∀ i : CurrentPivotConstituent role n, ∀ s ∈ allFrequencyList n t,
         (s : ZMod (q (scheduledPartitionEquiv role n (.inl i)))) ≠ 0) :
       let e := scheduledPartitionEquiv role n
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleVertex, OAI.Ostmann.CopyScheduleSurvives, OAI.Ostmann.CurrentPivotConstituent, OAI.Ostmann.allFrequencyList, OAI.Ostmann.scheduledPartitionEquiv