Entropy.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Binary entropy estimates used by the subset-sum algorithm

The paper measures entropy in bits, whereas Mathlib's Real.binEntropy uses natural logarithms. Normalization gives the elementary estimates in the paper's preliminary section.

def OAI.LowSpaceSubsetSum.binaryEntropy line 20
Source documentation
Binary entropy measured in bits.
```
noncomputable def binaryEntropy (p : ℝ) : ℝ := Real.binEntropy p / Real.log 2
```
theorem OAI.LowSpaceSubsetSum.log_two_pos line 22
theorem OAI.LowSpaceSubsetSum.binaryEntropy_eq_logb line 24
theorem OAI.LowSpaceSubsetSum.binaryEntropy_zero line 29
theorem OAI.LowSpaceSubsetSum.binaryEntropy_one line 32
theorem OAI.LowSpaceSubsetSum.binaryEntropy_half line 35
theorem OAI.LowSpaceSubsetSum.binaryEntropy_one_sub line 40
theorem OAI.LowSpaceSubsetSum.binaryEntropy_nonneg line 44
theorem OAI.LowSpaceSubsetSum.binaryEntropy_le_one line 48
theorem OAI.LowSpaceSubsetSum.binaryEntropy_concaveOn line 51
theorem OAI.LowSpaceSubsetSum.binaryEntropy_strictMonoOn line 57
theorem OAI.LowSpaceSubsetSum.binaryEntropy_monoOn line 64
theorem OAI.LowSpaceSubsetSum.logb_two_self line 67
theorem OAI.LowSpaceSubsetSum.logb_two_four line 70
theorem OAI.LowSpaceSubsetSum.binaryEntropy_quarter line 75
theorem OAI.LowSpaceSubsetSum.binaryEntropy_third line 84
theorem OAI.LowSpaceSubsetSum.binaryEntropy_quarter_complement line 93
theorem OAI.LowSpaceSubsetSum.binaryEntropy_sixth line 98
theorem OAI.LowSpaceSubsetSum.binaryEntropy_quarter_lt line 105
Source documentation
The integer power comparison certifying the paper's decimal entropy bound.
```
theorem binaryEntropy_quarter_lt : binaryEntropy (1 / 4) < 4057 / 5000 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.binaryEntropy
theorem OAI.LowSpaceSubsetSum.binaryEntropy_third_lt line 114
theorem OAI.LowSpaceSubsetSum.binaryEntropy_sixth_gt line 123
theorem OAI.LowSpaceSubsetSum.binaryEntropy_pair_le_quarter line 138
Source documentation
The paired entropy budget in the representation tree is maximized when the two cardinality densities coincide.
```
theorem binaryEntropy_pair_le_quarter {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1 / 2) :
    (binaryEntropy p + binaryEntropy (1 / 2 - p)) / 2 ≤ binaryEntropy (1 / 4) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.binaryEntropy
theorem OAI.LowSpaceSubsetSum.binaryEntropy_abs_sub_lt line 150
Source documentation
The two child entropy values differ by less than the paper's 3/8 margin throughout the allowed density interval.
```
theorem binaryEntropy_abs_sub_lt {p q : ℝ} (hp : p ∈ Set.Icc (1 / 6) (1 / 3))
    (hq : q ∈ Set.Icc (1 / 6) (1 / 3)) :
    |binaryEntropy p - binaryEntropy q| < 3 / 8 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.binomialMass_mean_bounds line 166

Source documentation

The binomial mass at its integral mean lies between 1/(n+1) and 1.

theorem binomialMass_mean_bounds (n k : ℕ) {p : ℝ} (hp : p ∈ Set.Ioo 0 1)
    (hk : k ≤ n) (hmean : (n : ℝ) * p = k) :
    1 ≤ ((n : ℝ) + 1) * TraceReconstruction.binomialMass n p k ∧
      TraceReconstruction.binomialMass n p k ≤ 1 := by
…

Mentions: OAI.TraceReconstruction.binomialMass

theorem OAI.LowSpaceSubsetSum.binomialMass_eq_choose_div_entropy line 183
Source documentation
The inverse of the entropy power is the probability of an individual binary string with k successes, when the Bernoulli parameter is k/n.
```
theorem binomialMass_eq_choose_div_entropy (n k : ℕ) (hk0 : 0 < k) (hkn : k < n) :
    TraceReconstruction.binomialMass n ((k : ℝ) / n) k =
      (n.choose k : ℝ) / (2 : ℝ) ^ ((n : ℝ) * binaryEntropy ((k : ℝ) / n)) := by
…
```
Mentions: OAI.TraceReconstruction.binomialMass, OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.choose_entropy_bounds line 214

Source documentation

Exact entropy bounds for binomial coefficients, including both endpoints.

theorem choose_entropy_bounds (n k : ℕ) (hk : k ≤ n) :
    (2 : ℝ) ^ ((n : ℝ) * binaryEntropy ((k : ℝ) / n)) / ((n : ℝ) + 1) ≤
        (n.choose k : ℝ) ∧
      (n.choose k : ℝ) ≤ (2 : ℝ) ^ ((n : ℝ) * binaryEntropy ((k : ℝ) / n)) := by
…

Mentions: OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.logb_choose_bounds line 247

Source documentation

Logarithmic form used in the background allocation formulas.

theorem logb_choose_bounds (n k : ℕ) (hk : k ≤ n) :
    (n : ℝ) * binaryEntropy ((k : ℝ) / n) - Real.logb 2 ((n : ℝ) + 1) ≤
        Real.logb 2 (n.choose k) ∧
      Real.logb 2 (n.choose k) ≤ (n : ℝ) * binaryEntropy ((k : ℝ) / n) := by
…

Mentions: OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.floor_logb_choose_error line 266

Source documentation

Rounding the binomial logarithm costs less than log₂(n+1)+1 bits.

theorem floor_logb_choose_error (n k : ℕ) (hk : k ≤ n) :
    |((⌊Real.logb 2 (n.choose k)⌋ : ℤ) : ℝ) -
      (n : ℝ) * binaryEntropy ((k : ℝ) / n)| < Real.logb 2 ((n : ℝ) + 1) + 1 := by
…

Mentions: OAI.LowSpaceSubsetSum.binaryEntropy