OAI/NumberTheory/Ostmann/Construction/ConstituentTransferWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.constituentTransferWeight line 14

   Source documentation

   Pairwise prime support is retained inside each grouped atom as well as between atoms. The reconstructed pivot remains a single integer parameter.

   noncomputable def constituentTransferWeight {I D : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (P : Finset ℕ) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (hist : D → FrequencyTree ℤ n)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → P) (M : ℕ)
       (a : (CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → P) × D) : ℂ :=
   …

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

2. theorem OAI.Ostmann.constituentTransferWeight_support line 29

   Source documentation

   Both coprimality clauses of the arithmetic transfer are now consequences of the concrete coefficient's support.

   theorem constituentTransferWeight_support {I D : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ) (p : I) (hp : role p = .pivot n)
       (P : Finset ℕ) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ) (hist : D → FrequencyTree ℤ n)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → P) (M : ℕ)
       (a : (CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → P) × D)
       (hw : constituentTransferWeight role size n P Q childBound pivotBound ranges leaf hist u M a ≠ 0) :
       Pairwise (fun i j =>
         (Sum.elim (fun h => (a.1 h : ℕ)) (fun y => (u y : ℕ)) i).Coprime
           (Sum.elim (fun h => (a.1 h : ℕ)) (fun y => (u y : ℕ)) j)) ∧
         M.Coprime ((∏ h, (a.1 h : ℕ)) * ∏ y, (u y : ℕ)) ∧
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.ScheduleAtomRange, OAI.Ostmann.ScheduleAtomState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.CopyScheduleY, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.constituentTransferWeight