OAI/NumberTheory/Ostmann/Construction/ConstituentCopiedSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.copiedConstituentAtomValues_left line 14
2. theorem OAI.Ostmann.copiedConstituentAtomValues_right line 23
3. theorem OAI.Ostmann.constituentTransferWeight_copied_support line 35

   Source documentation

   No new support assumption is imposed on the next coefficient. Its coprimality tests follow from nonzero old coefficients and the signed equation; only the explicit numerical and interval cutoffs are needed.

   theorem constituentTransferWeight_copied_support {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (size : I → ℕ) (n : ℕ)
       (p : I) (hp : role p = .pivot n)
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (Q : (Σ i, Fin (size i)) → Finset ℕ)
       (childBound pivotBound : ℕ → ℕ) (ranges : (j : ℕ) → List (ScheduleAtomRange role j))
       (leaf : ScheduleAtomState role → ℤ → ℂ)
       (u : CopyScheduleY (fun i : Σ a, Fin (size a) => role i.1) n → P)
       (l r : CopyScheduleH (fun i : Σ a, Fin (size a) => role i.1) n → P)
       (s : ℤ) (t t' : FrequencyTree ℤ n) (M K V : ℕ)
       (hl : constituentTransferWeight role size n P Q childBound pivotBound ranges leaf id u M (l, t) ≠ 0)
       (hr : constituentTransferWeight role size n P Q childBound pivotBound ranges leaf id u M (r, t') ≠ 0)
       (hs : s ≠ 0) (hMpos : 0 < M) (hMbound : M ≤ pivotBound n)
   …

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