OAI/NumberTheory/Ostmann/Construction/ScheduledInputPhase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledInputLabels line 12
2. theorem OAI.Ostmann.scheduledInputPrimeFact line 18
3. theorem OAI.Ostmann.scheduledInputLabels_apply line 30
4. theorem OAI.Ostmann.scheduledInputPhase_factor line 40

   Source documentation

   The actual factorization is in the very same finite enumeration as the original harmonic pivot prior and its residue-row transfer.

   theorem scheduledInputPhase_factor {I : Type*} [Fintype I]
       (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) (t : FrequencyTree ℤ n)
       (P : Fin r → ℕ) (L : CopyScheduleH role n → ℕ) (U : CopyScheduleY role n → ℕ)
       [∀ i, Fact (P i).Prime] [∀ i, Fact (L i).Prime] [∀ i, Fact (U i).Prime]
       (center : ∀ p : ℕ, ZMod p)
       (hc : Pairwise (fun i j => (Sum.elim P (Sum.elim L U) i).Coprime
         (Sum.elim P (Sum.elim L U) j)))
       (hfreq : ∀ i, ∀ s ∈ allFrequencyList n t, (s : ZMod (P i)) ≠ 0) :
       letI := scheduledInputPrimeFact role n r e P L U
   …

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

5. theorem OAI.Ostmann.pivot_retained_pairwise line 138

   Source documentation

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

   theorem pivot_retained_pairwise {r : ℕ} {H Y : Type*} [Fintype H] [Fintype Y]
       (P : Fin r → ℕ) (L : H → ℕ) (U : Y → ℕ)
       (hP : Pairwise (fun i j => (P i).Coprime (P j)))
       (hLU : Pairwise (fun i j => (Sum.elim L U i).Coprime (Sum.elim L U j)))
       (hM : (∏ i, P i).Coprime ((∏ h, L h) * ∏ y, U y)) :
       Pairwise (fun i j => (Sum.elim P (Sum.elim L U) i).Coprime
         (Sum.elim P (Sum.elim L U) j)) := by
   …