OAI/NumberTheory/Ostmann/Construction/SamplePatternCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.samplePatternLabels line 12

   Source documentation

   The class coordinates used by the finite independent-prior comparison.

   noncomputable def samplePatternLabels {I : Type*} [Fintype I]
       (s : Setoid I) {N : ℕ} (hcard : Fintype.card (Quotient s) = N + 1) : I → Fin (N + 1) :=
   …

2. theorem OAI.Ostmann.samplePatternLabels_surjective line 16
3. def OAI.Ostmann.samplePatternRepresentative line 21
4. def OAI.Ostmann.samplePatternValues line 27
5. theorem OAI.Ostmann.samplePatternValues_labels line 32
6. theorem OAI.Ostmann.samplePatternValues_injective line 38
7. theorem OAI.Ostmann.samplePattern_tier_compatible line 46

   Source documentation

   Tier separation of actual primes makes the original tier constant on each realized class. This derives compatibility instead of requiring a new pattern hypothesis.

   theorem samplePattern_tier_compatible {I A : Type*} (p : SampleEqualityPattern I A)
       (tier : I → ℕ) (prime : A → ℕ)
       (hdisjoint : ∀ i j, tier i ≠ tier j → prime (p.evaluate i) ≠ prime (p.evaluate j))
       (i j : I) (hij : p.1 i j) : tier i = tier j := by
   …

   Mentions: OAI.Ostmann.SampleEqualityPattern

8. def OAI.Ostmann.samplePatternTier line 54
9. theorem OAI.Ostmann.samplePatternTier_labels line 59
10. theorem OAI.Ostmann.MovingSlotData.levels_samplePattern line 68