Bins.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TalagrandDiscreteConvexity.largeWeightFamily line 15
Source documentation
The generators whose weights pay directly for their cost.
```
noncomputable def largeWeightFamily (W : Finset α → ℝ) : Family α := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.smallWeightFamily line 20
Source documentation
The remaining nonzero weights; this finite family is partitioned into bins.
```
noncomputable def smallWeightFamily (W : Finset α → ℝ) : Family α := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.Family
def OAI.TalagrandDiscreteConvexity.weightBinKey line 25
def OAI.TalagrandDiscreteConvexity.occupiedWeightBins line 28
def OAI.TalagrandDiscreteConvexity.weightBin line 31
theorem OAI.TalagrandDiscreteConvexity.mem_largeWeightFamily line 34
theorem OAI.TalagrandDiscreteConvexity.mem_smallWeightFamily line 40
theorem OAI.TalagrandDiscreteConvexity.mem_weightBin line 46
theorem OAI.TalagrandDiscreteConvexity.weightBin_card line 51
theorem OAI.TalagrandDiscreteConvexity.weightBin_bounds line 55
theorem OAI.TalagrandDiscreteConvexity.occupiedWeightBins_bounds line 65
theorem OAI.TalagrandDiscreteConvexity.subfamily_weight_sum_le line 74

theorem OAI.TalagrandDiscreteConvexity.weightBin_cost_bound line 82

Source documentation

Each occupied bin satisfies the size hypothesis of the covering lemma.

theorem weightBin_cost_bound {q : ℝ} {W : Finset α → ℝ}
    (hq : 0 < q) (hW : ∀ U, 0 ≤ W U)
    (hglobal : (∑ U : Finset α, q ^ U.card * W U) ≤ 1) (b : ℕ × ℕ) :
    ((weightBin W b).card : ℝ) * (q / (2 : ℝ) ^ 70) ^ b.1 ≤
      (2 : ℝ) ^ (b.2 + 1) := by
…

Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.weightBin

theorem OAI.TalagrandDiscreteConvexity.largeWeightFamily_cost_le line 101
Source documentation
All large weights together have cost at most one sixty-fourth.
```
theorem largeWeightFamily_cost_le {q : ℝ} {W : Finset α → ℝ}
    (hq : 0 ≤ q) (hW : ∀ U, 0 ≤ W U)
    (hglobal : (∑ U : Finset α, q ^ U.card * W U) ≤ 1) :
    cost (q / (2 : ℝ) ^ 70) (largeWeightFamily W) ≤ 1 / 64 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.cost, OAI.TalagrandDiscreteConvexity.largeWeightFamily

theorem OAI.TalagrandDiscreteConvexity.weightBin_power_sum_le line 119

Source documentation

In an uncovered bin, the sixteenth powers have the required geometric bound.

theorem weightBin_power_sum_le {W : Finset α → ℝ} (hW : ∀ U, 0 ≤ W U)
    (S : Finset α) (b : ℕ × ℕ)
    (hcount : ((weightBin W b).filter (fun U => U ⊆ S)).card ≤ 2 ^ (12 * b.2)) :
    (∑ U ∈ (weightBin W b).filter (fun U => U ⊆ S), (W U) ^ 16) ≤
      (1 / 2 : ℝ) ^ (4 * b.2) := by
…

Mentions: OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.weightBin

theorem OAI.TalagrandDiscreteConvexity.subset_power_sum_le_bins line 135
Source documentation
Removing zero weights and partitioning the remainder is a finite identity.
```
theorem subset_power_sum_le_bins {W : Finset α → ℝ} (hW : ∀ U, 0 ≤ W U)
    (S : Finset α) (hlarge : ∀ U ∈ largeWeightFamily W, ¬ U ⊆ S) :
    (∑ U ∈ S.powerset.erase ∅, (W U) ^ 16) ≤
      ∑ b ∈ occupiedWeightBins W,
        ∑ U ∈ (weightBin W b).filter (fun U => U ⊆ S), (W U) ^ 16 := by
…
```
Mentions: OAI.TalagrandDiscreteConvexity.largeWeightFamily, OAI.TalagrandDiscreteConvexity.b, OAI.TalagrandDiscreteConvexity.occupiedWeightBins, OAI.TalagrandDiscreteConvexity.weightBin