OAI/NumberTheory/Ostmann/Arithmetic/MovingSamplePairPatterns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Equality patterns of the two actual internal sample trees

  1. def OAI.Ostmann.movingSamplePairCoordinates line 11
  2. theorem OAI.Ostmann.movingSamplePairCoordinates_left line 25
  3. theorem OAI.Ostmann.movingSamplePairCoordinates_right line 30
  4. theorem OAI.Ostmann.sum_movingSamplePair line 35
  5. theorem OAI.Ostmann.card_movingSamplePairIndex line 47

    Source documentation

    The two histories have exactly 4*n*2^n independent internal draws, irrespective of the number of protected bulk positions.

    theorem card_movingSamplePairIndex (n : ℕ) :
    Fintype.card (Bool × MovingSampleIndex n) = 4 * n * 2 ^ n := by
…

    Mentions: OAI.Ostmann.MovingSampleIndex

  6. theorem OAI.Ostmann.movingSamplePair_compensated_prior line 52
  7. theorem OAI.Ostmann.sum_movingSamplePair_patterns line 67

    Source documentation

    Exact decomposition of the original pair of sample trees by its equality pattern. No restriction on coincidences between descendants is inserted, and no factor depending on the bulk length appears.

    theorem sum_movingSamplePair_patterns {A M : Type*} [Fintype A] [AddCommMonoid M]
    (n : ℕ) (F : MovingSampleSlots A n → MovingSampleSlots A n → M) :
    letI := sampleSetoidFintype (Bool × MovingSampleIndex n)
…

    Mentions: OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.sampleSetoidFintype, OAI.Ostmann.MovingSampleIndex