MovingOccurrenceNumerator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Identifying the occurrence lines with the actual integer numerators

theorem OAI.Ostmann.movingSlotLine_integer_numerator line 11

theorem OAI.Ostmann.sampled_occurrence_numerator line 55

Source documentation

All prerequisites of the numerator identity now follow from the original numeric tree support and the actual type-separated sampled primes.

theorem sampled_occurrence_numerator {σ : Type*}
    (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
    (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
    (n : ℕ) (t : FrequencyTree ℤ n) (small bulk : TreeLeafTuple (List σ) n)
    (samples : MovingSampleSlots σ n) (XL XR : ℕ)
    (hsmall : ∀ i ∈ flattenMovingSlots n small, n ≤ tier i)
    (hbulk : ∀ i ∈ flattenMovingSlots n bulk, n ≤ tier i)
    (hsamples : samples.Levels tier)
    (hI : (buildMovingGiantTree n t (movingSlotValues value n small) (samples.values value)).Integral
      XL XR (movingSlotValues value n bulk))
    (o : MovingSlotOccurrence σ) (ho : o ∈ (buildMovingSlotData n t small bulk samples).occurrences)
    (rep : σ) (hrep : tier rep < o.level)
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleSlots, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.buildMovingGiantTree, OAI.Ostmann.movingSlotValues, OAI.Ostmann.MovingSlotOccurrence, OAI.Ostmann.buildMovingSlotData