SparseObservationEntropy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Entropy budgets for observations on sparse sections

lemma OAI.DukePrimeDegree.summable_option_of_summable_some line 14

theorem OAI.DukePrimeDegree.sparse_distribution_information_le line 24

Source documentation

A row-wise budget controls both the rare-label mass and its entropy.

theorem sparse_distribution_information_le (K : ℕ → ℕ)
    (p : Option (Σ n : ℕ, Fin (K n)) → ℝ)
    (hp : ∀ z, 0 ≤ p z) (hp1 : ∀ z, p z ≤ 1)
    (hs : Summable p) (hsum : ∑' z, p z=1)
    (w : ℕ → ℝ) (hw : ∀ n, 0 ≤ w n) (hws : Summable w)
    (hsmall : ∀ n (i : Fin (K n)), p (some ⟨n,i⟩) ≤ w n/(K n+1:ℝ))
    (hinfo : ∀ n (i : Fin (K n)),
      Real.negMulLog (p (some ⟨n,i⟩)) ≤ w n/(K n+1:ℝ)) :
    Summable (fun z => Real.negMulLog (p z)) ∧
      (∑' z, Real.negMulLog (p z)) ≤ 2*∑' n, w n := by
…

lemma OAI.DukePrimeDegree.exists_small_mass_information_budget line 79

theorem OAI.DukePrimeDegree.exists_sparse_distribution_budget line 99

Source documentation

The finite label cardinalities may grow arbitrarily fast: their section masses can be chosen afterwards to absorb their Shannon cost.

theorem exists_sparse_distribution_budget (K : ℕ → ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℕ → ℝ, (∀ n, 0 < δ n) ∧ Summable δ ∧
      (∑' n, δ n) ≤ ε/4 ∧
      ∀ p : Option (Σ n : ℕ, Fin (K n)) → ℝ,
        (∀ z, 0 ≤ p z) → (∀ z, p z ≤ 1) → Summable p → (∑' z, p z)=1 →
        (∀ n (i : Fin (K n)), p (some ⟨n,i⟩) ≤ δ n) →
        Summable (fun z => Real.negMulLog (p z)) ∧
          (∑' z, Real.negMulLog (p z)) < ε := by
…