OAI/NumberTheory/Ostmann/Construction/ScheduledNonanchorWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.scheduled_nonanchor_matching_witness line 10
2. theorem OAI.Ostmann.scheduled_nonanchor_prime_ranges line 40

   Source documentation

   The prime ranges in either parity case come from the actual changed leaf.

   theorem scheduled_nonanchor_prime_ranges {I : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (pivot : ℕ → I) (n m : ℕ)
       (word : Fin m ≃ {i : I // role i = .word})
       (e : Equiv.Perm (CopyScheduleH role (n + 1)))
       (he : e ∈ cellPreservingMatchings (scheduledBulkLabel role (n + 1)) \
         scheduledAnchorMatchingSet role (n + 1) m word)
       (small large : Fin (n + 1) → I)
       (hsmall : ∀ j, role (small j) = .anchor j) (hlarge : ∀ j, role (large j) = .anchor j)
       (hp : ∀ k < n + 1, role (pivot k) = .pivot k)
       (χ : I → ∀ p : ℕ, DirichletCharacter ℂ p) (Q₀ : I → Finset ℕ)
       (hχsmall : ∀ j q, q ∈ Q₀ (small j) → χ (small j) q ^ 2 ≠ 1)
       (hχword : ∀ v, role v = .word → ∀ q ∈ Q₀ v, χ v q ^ 2 ≠ 1)
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleH, OAI.Ostmann.cellPreservingMatchings, OAI.Ostmann.scheduledBulkLabel, OAI.Ostmann.scheduledAnchorMatchingSet