OAI/NumberTheory/DukePrimeDegree/Entropy/LastActiveObservation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Countable observations at the last active scale

Summably small sections overlap only finitely often almost everywhere. Recording the largest active scale therefore preserves arbitrarily fine visits while keeping the observation alphabet countable.

  1. def OAI.DukePrimeDegree.lastActiveSection line 18
  2. lemma OAI.DukePrimeDegree.measurableSet_lastActiveSection line 21
  3. lemma OAI.DukePrimeDegree.lastActiveSection_unique line 30
  4. lemma OAI.DukePrimeDegree.exists_lastActiveSection_of_finite line 37
  5. def OAI.DukePrimeDegree.lastActiveObservationAtom line 49
  6. lemma OAI.DukePrimeDegree.lastActiveObservation_covers line 54
  7. lemma OAI.DukePrimeDegree.lastActiveObservationAtom_unique line 63
  8. def OAI.DukePrimeDegree.lastActiveObservation line 86
  9. lemma OAI.DukePrimeDegree.lastActiveObservation_fiber line 90
  10. lemma OAI.DukePrimeDegree.measurable_lastActiveObservation line 102
  11. lemma OAI.DukePrimeDegree.lastActiveObservation_scale_ge line 119

    Source documentation

    A visit to scale n is recorded at some scale at least n whenever only finitely many sections contain the current point.

    lemma lastActiveObservation_scale_ge {Y : Type*} (S : ℕ → Set Y)
    {K : ℕ → ℕ} (B : ∀ n, Y → Fin (K n)) {x : Y}
    (hfin : {n | x ∈ S n}.Finite) {n : ℕ} (hn : x ∈ S n) :
    ∃ m, n ≤ m ∧ lastActiveObservation S B x=some ⟨m,B m x⟩ := by
…

    Mentions: OAI.DukePrimeDegree.lastActiveObservation