SeparatorIncidence.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Rounded separator incidence estimates

The sharp entropy estimate remains useful after the integer cardinalities are rounded. We use a fixed compact interval and explicit constant error, so that rounding introduces a constant factor rather than exponential slack.

theorem OAI.LowSpaceSubsetSum.logb_two_eight line 16
theorem OAI.LowSpaceSubsetSum.hasDerivAt_binaryEntropy_compact line 21
theorem OAI.LowSpaceSubsetSum.binaryEntropy_deriv_bound line 31
theorem OAI.LowSpaceSubsetSum.binaryEntropy_lipschitz_compact line 47
Source documentation
A fixed constant suffices for every density used by the rounded separator.
```
theorem binaryEntropy_lipschitz_compact {p q : ℝ}
    (hp : p ∈ Set.Icc (1 / 8) (7 / 8)) (hq : q ∈ Set.Icc (1 / 8) (7 / 8)) :
    |binaryEntropy p - binaryEntropy q| ≤ 3 * |p - q| := by
…
```
Mentions: OAI.LowSpaceSubsetSum.binaryEntropy
def OAI.LowSpaceSubsetSum.separatorRationalAlpha line 57
Source documentation
The floor-computed rational slope used in the sampling rule.
```
noncomputable def separatorRationalAlpha (m : ℕ) : ℝ :=
…
```
theorem OAI.LowSpaceSubsetSum.separatorRationalAlpha_error line 60
theorem OAI.LowSpaceSubsetSum.separatorRationalAlpha_eq_log_power line 78
theorem OAI.LowSpaceSubsetSum.separatorRationalAlpha_sample_error line 85
Source documentation
Approximating the slope by its integer-log version costs at most one in the prescribed sample size whenever the block fits inside the mixer.
```
theorem separatorRationalAlpha_sample_error {g m : ℕ} (hm : 0 < m) (hgm : g ≤ m)
    {k : ℝ} (hk : k ∈ Set.Icc (1 / 6) (1 / 3)) :
    |(g : ℝ) * (1 / 2 + separatorRationalAlpha m * (k - 1 / 4)) -
      (g : ℝ) * (k + separatorY k)| ≤ 1 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.separatorRationalAlpha, OAI.LowSpaceSubsetSum.separatorY
theorem OAI.LowSpaceSubsetSum.separator_sample_floor_error line 110
Source documentation
The actual outer floor plus the rational-slope approximation satisfies the two-unit error used in the incidence theorem.
```
theorem separator_sample_floor_error {g m e : ℕ} (hm : 0 < m) (hgm : g ≤ m)
    {k : ℝ} (hk : k ∈ Set.Icc (1 / 6) (1 / 3))
    (he : (e : ℤ) = ⌊(g : ℝ) * (1 / 2 + separatorRationalAlpha m * (k - 1 / 4))⌋) :
    |(e : ℝ) - (g : ℝ) * (k + separatorY k)| ≤ 2 := by
…
```
Mentions: OAI.LowSpaceSubsetSum.separatorRationalAlpha, OAI.LowSpaceSubsetSum.separatorY
theorem OAI.LowSpaceSubsetSum.separator_density_bounds line 125

theorem OAI.LowSpaceSubsetSum.weighted_binaryEntropy_error line 138

Source documentation

A weighted form avoids dividing a rounding error by a small block size.

theorem weighted_binaryEntropy_error {a b p q : ℝ} (ha : 0 ≤ a)
    (hp : p ∈ Set.Icc (1 / 8) (7 / 8)) (hq : q ∈ Set.Icc (1 / 8) (7 / 8)) :
    |a * binaryEntropy p - b * binaryEntropy q| ≤
      3 * |a * p - b * q| + 4 * |a - b| := by
…

Mentions: OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.choose_ratio_le_of_entropy_gap line 170

Source documentation

The binomial entropy bounds turn an exponent gap into a ratio bound.

theorem choose_ratio_le_of_entropy_gap (n d j : ℕ) (hjn : j ≤ n) (hjd : j ≤ d)
    {T : ℝ} (hT : (n : ℝ) * binaryEntropy ((j : ℝ) / n) -
      (d : ℝ) * binaryEntropy ((j : ℝ) / d) ≤ T) :
    (n.choose j : ℝ) / (d.choose j : ℝ) ≤
      ((d : ℝ) + 1) * (2 : ℝ) ^ T := by
…

Mentions: OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.rounded_separator_entropy_gap line 195

Source documentation

Bounded rounding changes the difference of the two entropy exponents by at most 22, uniformly over the entire allowed density interval.

theorem rounded_separator_entropy_gap (g c e : ℕ) (hg : 64 ≤ g) (heven : 2 ∣ g)
    (hce : c ≤ e) (heg : e ≤ g) {k : ℝ} (hk : k ∈ Set.Icc (1 / 6) (1 / 3))
    (hc : |(c : ℝ) - (g : ℝ) * k| ≤ 1)
    (he : |(e : ℝ) - (g : ℝ) * (k + separatorY k)| ≤ 2) :
    ((g - c : ℕ) : ℝ) * binaryEntropy (((e - c : ℕ) : ℝ) / (g - c : ℕ)) -
      ((g / 2 : ℕ) : ℝ) * binaryEntropy (((e - c : ℕ) : ℝ) / (g / 2 : ℕ)) ≤
      (g : ℝ) * (1 - binaryEntropy (1 / 4)) + 22 := by
…

Mentions: OAI.LowSpaceSubsetSum.separatorY, OAI.LowSpaceSubsetSum.binaryEntropy

theorem OAI.LowSpaceSubsetSum.rounded_separator_incidence_bound line 284

Source documentation

The rounded separator incidence bound has only a linear polynomial factor. The constant is 11 * 2^22 = 46,137,344.

theorem rounded_separator_incidence_bound (g c e : ℕ) (hg : 64 ≤ g) (heven : 2 ∣ g)
    (hce : c ≤ e) (heg : e ≤ g) (hjd : e - c ≤ g / 2)
    {k : ℝ} (hk : k ∈ Set.Icc (1 / 6) (1 / 3))
    (hc : |(c : ℝ) - (g : ℝ) * k| ≤ 1)
    (he : |(e : ℝ) - (g : ℝ) * (k + separatorY k)| ≤ 2) :
    11 * ((Nat.choose (g - c) (e - c) : ℝ) / Nat.choose (g / 2) (e - c)) ≤
      (11 * 2 ^ 22 : ℝ) * ((g : ℝ) + 1) *
        (2 : ℝ) ^ ((g : ℝ) * (1 - binaryEntropy (1 / 4))) := by
…

Mentions: OAI.LowSpaceSubsetSum.separatorY, OAI.LowSpaceSubsetSum.binaryEntropy