OAI/NumberTheory/JointDickman/Amplification/OmissionEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.subset_count_entropy_of_card_le line 13

   Source documentation

   The bound uses an upper bound for the population size, so it applies uniformly throughout a regularity window.

   theorem subset_count_entropy_of_card_le (P : Finset ℕ) {θ m : ℝ}
       (hθ : 0 < θ) (hθhalf : θ ≤ 1/2) (hcard : (P.card : ℝ) ≤ m) :
       ((P.powerset.filter (fun A => (A.card : ℝ) ≤ θ*m)).card : ℝ) ≤
         Real.exp (m*Real.binEntropy θ) := by
   …

2. theorem OAI.JointDickman.high_omission_count_bound line 44

   Source documentation

   On each endpoint the higher omissions cost an entropy exponent tending to zero with τ. This statement keeps the exact real threshold 4τℓ.

   theorem high_omission_count_bound (P : Finset ℕ) {τ ℓ : ℝ}
       (hτ : 0 < τ) (hτsmall : τ ≤ 1/100) (_hℓ : 0 ≤ ℓ)
       (hcard : (P.card : ℝ) ≤ (1/2+τ)*ℓ) :
       ((P.powerset.filter (fun A => (A.card : ℝ) ≤ 4*τ*ℓ)).card : ℝ) ≤
         Real.exp (((1/2+τ)*Real.binEntropy (4*τ/(1/2+τ)))*ℓ) := by
   …