OAI/NumberTheory/JointDickman/Amplification/SubsetCardEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Entropy bound for subsets of a prescribed size

  1. theorem OAI.JointDickman.subset_exact_count_exp_bound line 10
  2. theorem OAI.JointDickman.subset_exact_count_entropy line 32

    Source documentation

    No rounding loss occurs for an exact cardinality.

    theorem subset_exact_count_entropy (P : Finset ℕ) {k : ℕ} (hk : k ≤ P.card) :
    ((P.powerset.filter (fun A => A.card = k)).card : ℝ) ≤
      Real.exp ((P.card : ℝ)*Real.binEntropy ((k : ℝ)/P.card)) := by
…