DyadicBins.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Dyadic bins for positive weights

The exponent of a weight is determined by the first power of 1 / 2 strictly below it. In particular, a weight equal to a dyadic endpoint belongs to the bin whose upper endpoint it equals.

def OAI.TalagrandDiscreteConvexity.binExponent line 20
Source documentation
The dyadic exponent of a positive weight. Its value at a nonpositive weight is irrelevant to the bin partition and is fixed to zero.
```
noncomputable def binExponent (w : ℝ) : ℕ := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w
theorem OAI.TalagrandDiscreteConvexity.binExponent_spec line 27
Source documentation
Every positive weight at most one lies in its specified dyadic bin.
```
theorem binExponent_spec {w : ℝ} (hwpos : 0 < w) (hwle : w ≤ 1) :
    (1 / 2 : ℝ) ^ (binExponent w + 1) < w ∧
      w ≤ (1 / 2 : ℝ) ^ binExponent w := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.binExponent
theorem OAI.TalagrandDiscreteConvexity.binExponent_lower line 45
theorem OAI.TalagrandDiscreteConvexity.binExponent_upper line 49
theorem OAI.TalagrandDiscreteConvexity.le_binExponent_of_le_pow line 54
Source documentation
A dyadic upper bound on a weight gives a lower bound on its bin index.
```
theorem le_binExponent_of_le_pow {w : ℝ} {n : ℕ} (hwpos : 0 < w)
    (hwn : w ≤ (1 / 2 : ℝ) ^ n) : n ≤ binExponent w := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.binExponent
theorem OAI.TalagrandDiscreteConvexity.le_binExponent_of_lt_pow line 65
theorem OAI.TalagrandDiscreteConvexity.binExponent_eq_of_bounds line 70
Source documentation
The half-open bins are disjoint, including at their dyadic endpoints.
```
theorem binExponent_eq_of_bounds {w : ℝ} {h : ℕ}
    (hlo : (1 / 2 : ℝ) ^ (h + 1) < w)
    (hhi : w ≤ (1 / 2 : ℝ) ^ h) : binExponent w = h := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w, OAI.TalagrandDiscreteConvexity.binExponent
theorem OAI.TalagrandDiscreteConvexity.exists_dyadic_bin line 85
Source documentation
The form used when assigning all residual weights to bins of index at least their support size.
```
theorem exists_dyadic_bin {w : ℝ} {n : ℕ} (hwpos : 0 < w)
    (hwn : w < (1 / 2 : ℝ) ^ n) :
    ∃ h : ℕ, n ≤ h ∧ (1 / 2 : ℝ) ^ (h + 1) < w ∧ w ≤ (1 / 2 : ℝ) ^ h := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w