SmallReturnEntropy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Small sections have small return-partition entropy

The adjustable geometric reference distribution controls the entropy by the section mass and the return-time first moment. This quantitative form allows the transverse-return refinement to have an arbitrarily small entropy cost.

lemma OAI.DukePrimeDegree.return_information_geometric_bound line 18

theorem OAI.DukePrimeDegree.exists_small_mass_return_information_bound line 56

Source documentation

With return-time mean at most one, small section mass makes the whole return partition, including its complement atom, arbitrarily low entropy.

theorem exists_small_mass_return_information_bound {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ p : ℕ → ℝ,
      (∀ n, 0 ≤ p n) → (∀ n, p n ≤ 1) →
      Summable (fun n : ℕ => (n+1:ℝ)*p n) →
      (∑' n : ℕ, (n+1:ℝ)*p n) ≤ 1 →
      ∀ m : ℝ, 0 ≤ m → m ≤ 1 → m ≤ δ → (∑' n, p n) ≤ m →
        Real.negMulLog (1-m)+(∑' n, Real.negMulLog (p n)) < ε := by
…