GreedyPivots.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

A bounded greedy family of pivots

At each step, choose a set whose mass outside the current union exceeds the threshold if such a set exists. Otherwise choose a fixed padding center. Padding still enlarges the union, so it cannot increase any residual mass. If the residual bound failed after s steps, all preceding steps would have made a strict gain greater than the threshold, contradicting total mass at most one and 1 ≤ s * θ.

def OAI.MetricEntropyDuality.GreedyPivots.mass line 32
Source documentation
The mass of a finite set of columns.
```
def mass (μ : Y → ℝ) (U : Finset Y) : ℝ := ∑ y ∈ U, μ y
```
theorem OAI.MetricEntropyDuality.GreedyPivots.mass_mono line 34
def OAI.MetricEntropyDuality.GreedyPivots.choosePivot line 41
Source documentation
An active greedy pivot, or a fixed center when every residual is small.
```
def choosePivot (μ : Y → ℝ) (I : X → Finset Y) (θ : ℝ) (U : Finset Y) : X := by
…
```
theorem OAI.MetricEntropyDuality.GreedyPivots.choosePivot_spec line 45
def OAI.MetricEntropyDuality.GreedyPivots.covered line 52
Source documentation
The union after exactly n selections, including any padding selections.
```
def covered (μ : Y → ℝ) (I : X → Finset Y) (θ : ℝ) : ℕ → Finset Y
  | 0 => ∅
  | n + 1 => covered μ I θ n ∪ I (choosePivot μ I θ (covered μ I θ n))
```
Mentions: OAI.MetricEntropyDuality.GreedyPivots.choosePivot
theorem OAI.MetricEntropyDuality.GreedyPivots.covered_zero line 56
theorem OAI.MetricEntropyDuality.GreedyPivots.covered_succ line 59
theorem OAI.MetricEntropyDuality.GreedyPivots.covered_subset_succ line 63
theorem OAI.MetricEntropyDuality.GreedyPivots.covered_mono line 66
theorem OAI.MetricEntropyDuality.GreedyPivots.bad_of_subset line 71
theorem OAI.MetricEntropyDuality.GreedyPivots.mass_union line 80
theorem OAI.MetricEntropyDuality.GreedyPivots.mass_covered_succ line 87
theorem OAI.MetricEntropyDuality.GreedyPivots.mass_lt_of_bad line 94
Source documentation
A residual violation at a positive stage forces strict total mass growth at every earlier stage, including the last one.
```
theorem mass_lt_of_bad (μ : Y → ℝ) (I : X → Finset Y) (θ : ℝ)
    (hμ : ∀ y, 0 ≤ μ y) (n : ℕ) :
    (∃ x, θ < mass μ (I x \ covered μ I θ n)) →
      n = 0 ∨ (n : ℝ) * θ < mass μ (covered μ I θ n) := by
…
```
Mentions: OAI.MetricEntropyDuality.GreedyPivots.mass, OAI.MetricEntropyDuality.GreedyPivots.covered
theorem OAI.MetricEntropyDuality.GreedyPivots.residual_le line 120
theorem OAI.MetricEntropyDuality.GreedyPivots.mem_covered_iff line 138
Source documentation
The recursive union consists exactly of the sets of its selected slots.
```
theorem mem_covered_iff (μ : Y → ℝ) (I : X → Finset Y) (θ : ℝ) (n : ℕ) (y : Y) :
    y ∈ covered μ I θ n ↔
      ∃ k < n, y ∈ I (choosePivot μ I θ (covered μ I θ k)) := by
…
```
Mentions: OAI.MetricEntropyDuality.GreedyPivots.covered, OAI.MetricEntropyDuality.GreedyPivots.choosePivot

theorem OAI.MetricEntropyDuality.exists_greedy_pivots line 159

Source documentation

A finite family has a bounded number of pivots whose uncovered mass is uniformly small. The assignment is supported exactly on the union of their sets, and assigns a column only to a set containing it.

theorem exists_greedy_pivots {X : Type uX} {Y : Type uY} [Fintype X] [Nonempty X] [Fintype Y]
    (μ : Y → ℝ) (I : X → Finset Y) (hμ : ∀ y, 0 ≤ μ y)
    (hmass : ∑ y, μ y ≤ 1) (θ : ℝ) (_hθ : 0 < θ) (s : ℕ)
    (hs : 1 ≤ (s : ℝ) * θ) :
    ∃ centers : Fin s → X, ∃ assigned : Y → Option (Fin s),
      (∀ y k, assigned y = some k → y ∈ I (centers k)) ∧
      (∀ y, (∃ k, y ∈ I (centers k)) ↔ assigned y ≠ none) ∧
      (∀ x, ∑ y ∈ (I x).filter (fun y => assigned y = none), μ y ≤ θ) := by
…