LastActiveEntropy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Small Shannon entropy for the last-active-scale observation

lemma OAI.DukePrimeDegree.countable_observation_distribution line 13

theorem OAI.DukePrimeDegree.exists_lastActiveObservation_entropy_budget line 30

Source documentation

All grid sizes are fixed before the section masses are chosen.

theorem exists_lastActiveObservation_entropy_budget
    {Y : Type*} [MeasurableSpace Y] (K : ℕ → ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℕ → ℝ, (∀ n, 0 < δ n) ∧ Summable δ ∧ (∑' n, δ n) ≤ ε/4 ∧
      ∀ (μ : Measure Y) [IsProbabilityMeasure μ] (S : ℕ → Set Y),
        (∀ n, MeasurableSet (S n)) → (∀ n, μ.real (S n) ≤ δ n) →
        ∀ B : ∀ n, Y → Fin (K n), (∀ n, Measurable (B n)) →
          Summable (fun z => Real.negMulLog (μ.real {x | lastActiveObservation S B x=z})) ∧
          (∑' z, Real.negMulLog (μ.real {x | lastActiveObservation S B x=z})) < ε := by
…

Mentions: OAI.DukePrimeDegree.lastActiveObservation