OAI/NumberTheory/Ostmann/Construction/SelectedFinalInteraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.selectedPairMatching line 11
2. theorem OAI.Ostmann.selected_final_pair_interaction line 16
3. theorem OAI.Ostmann.selectedFinalPerm_inv line 53
4. def OAI.Ostmann.selectedFinalRelativePerm line 61
5. theorem OAI.Ostmann.selectedFinalRelativePerm_matching line 66
6. theorem OAI.Ostmann.selected_final_relative_prime_ranges line 79

   Source documentation

   The long prime is certified to be a selected bulk prime, so no upper prime-range hypothesis is imposed on the top slot.

   theorem selected_final_relative_prime_ranges {I : Type*} (role : I → CopyScheduleRole)
       (pivot : ℕ → I) (n m : ℕ) (bulk : Fin m ↪ I) (hbulk : ∀ i, role (bulk i) = .word)
       (anchor : Fin (n + 1) → I) (ha : ∀ j, role (anchor j) = .anchor j)
       (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
       (Q : I → Finset ℕ) (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p)
       (lower : ℝ) (Bq A E : ℕ)
       (hsquare : ∀ j q, q ∈ Q (anchor j) → χ (anchor j) q ^ 2 ≠ 1)
       (hanchor : ∀ j q, q ∈ Q (anchor j) → lower ≤ (q : ℝ) ∧ q ≤ Bq)
       (hword : ∀ i p, p ∈ Q (bulk i) → 2 * A ≤ p ∧ p ≤ E)
       (e f : FinalParityReassignments n m) (hef : e ≠ f) :
       ∃ a b : CopyScheduleAtoms role (n + 1), a ≠ b ∧
         (∀ q ∈ Q (copyScheduleOrigin (n + 1) a.val), lower ≤ (q : ℝ) ∧ q ≤ Bq) ∧
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.FinalParityReassignments, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.copyScheduleOrigin