OAI/NumberTheory/Ostmann/Construction/PrimeBulkInsertion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeBulkValues line 9
2. theorem OAI.Ostmann.primeBulkValues_at line 13
3. theorem OAI.Ostmann.primeBulkValues_off line 17
4. theorem OAI.Ostmann.primeBulkValues_prime line 21
5. theorem OAI.Ostmann.primeBulkValues_injective_iff line 33
6. theorem OAI.Ostmann.primeBulkValues_cross_of_deleted line 45

   Source documentation

   Removing each fixed nonbulk prime from the old cells enforces all cross inequalities, while permitting equal bulk draws until their original gate.

   theorem primeBulkValues_cross_of_deleted {σ J : Type*} {P : Finset ℕ}
       (base : σ → ℕ) (slot : J ↪ σ) (x : J → P) (S deleted : J → Finset ℕ)
       (hx : ∀ j, (x j : ℕ) ∈ S j \ deleted j)
       (hdeleted : ∀ j i, i ∉ Set.range slot → base i ∈ deleted j) :
       ∀ i k, bulkIndexPredicate slot i ≠ bulkIndexPredicate slot k →
         primeBulkValues base slot x i ≠ primeBulkValues base slot x k := by
   …

   Mentions: OAI.Ostmann.bulkIndexPredicate, OAI.Ostmann.primeBulkValues

7. theorem OAI.Ostmann.primeBulkValues_outside_coprime line 65
8. theorem OAI.Ostmann.primeBulkValues_cell_label line 77