BinNumerics.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TalagrandDiscreteConvexity.half_range_sum line 18
theorem OAI.TalagrandDiscreteConvexity.finite_half_sum_le_two line 26
theorem OAI.TalagrandDiscreteConvexity.finite_small_base_sum_le_two line 40
theorem OAI.TalagrandDiscreteConvexity.finite_quadrant_sum_le_four line 47

theorem OAI.TalagrandDiscreteConvexity.finite_bin_geometric_bound line 69

Source documentation

A finite occupied-bin estimate, with no infinite-series premise.

theorem finite_bin_geometric_bound (B : Finset (ℕ × ℕ))
    (hB : ∀ b ∈ B, 1 ≤ b.1 ∧ 64 * b.1 ≤ b.2) {a : ℝ}
    (ha : 0 ≤ a) (ha' : a ≤ 1 / 2) :
    (∑ b ∈ B, a ^ b.2) ≤ 4 * a ^ 64 := by
…

Mentions: OAI.TalagrandDiscreteConvexity.b

theorem OAI.TalagrandDiscreteConvexity.finite_bin_cost_lt_quarter line 101
Source documentation
The total bin-cover cost is strictly below one quarter.
```
theorem finite_bin_cost_lt_quarter (B : Finset (ℕ × ℕ))
    (hB : ∀ b ∈ B, 1 ≤ b.1 ∧ 64 * b.1 ≤ b.2) :
    (∑ b ∈ B, 3 * (1 / 2 : ℝ) ^ b.2) < 1 / 4 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b
theorem OAI.TalagrandDiscreteConvexity.finite_bin_power_lt_threshold line 111
Source documentation
The total contribution of uncovered bins is below the exceptional threshold.
```
theorem finite_bin_power_lt_threshold (B : Finset (ℕ × ℕ))
    (hB : ∀ b ∈ B, 1 ≤ b.1 ∧ 64 * b.1 ≤ b.2) :
    (∑ b ∈ B, (1 / 2 : ℝ) ^ (4 * b.2)) < (1 / 2 : ℝ) ^ 32 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.b
theorem OAI.TalagrandDiscreteConvexity.outright_weight_le line 123
Source documentation
Large weights can be bought outright at a total factor of at most 1/64.
```
theorem outright_weight_le {r : ℕ} {q w : ℝ} (hr : 1 ≤ r) (hq : 0 ≤ q)
    (hw : (1 / 2 : ℝ) ^ (64 * r) ≤ w) :
    (q / (2 : ℝ) ^ 70) ^ r ≤ (1 / 64 : ℝ) * q ^ r * w := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.w

theorem OAI.TalagrandDiscreteConvexity.bin_card_cost_bound line 143

Source documentation

The lower edge of a bin bounds its cardinality at the reduced density.

theorem bin_card_cost_bound {n r h : ℕ} {q : ℝ} (hq : 0 < q)
    (hw : (n : ℝ) * q ^ r * (1 / 2 : ℝ) ^ (h + 1) ≤ 1) :
    (n : ℝ) * (q / (2 : ℝ) ^ 70) ^ r ≤ (2 : ℝ) ^ (h + 1) := by
…

theorem OAI.TalagrandDiscreteConvexity.bin_power_bound line 163
Source documentation
Fewer than 2^(12h) weights at most 2⁻ʰ have small sixteenth-power sum.
```
theorem bin_power_bound {m h : ℕ} (hm : m ≤ 2 ^ (12 * h)) :
    (m : ℝ) * ((1 / 2 : ℝ) ^ h) ^ 16 ≤ (1 / 2 : ℝ) ^ (4 * h) := by
…
```