WeightReplication.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Replication of finite weights

Ceilings produce integer cluster sizes while giving one copy to every key of zero weight. The resulting counting law satisfies the multiplicative and auxiliary-mass estimates from Section 7 of OpenAI's Constant-factor hardness of uniform sparsest cut.

def OAI.UniformSparsestCut.FiniteWeights.copies line 26
def OAI.UniformSparsestCut.FiniteWeights.population line 28
def OAI.UniformSparsestCut.FiniteWeights.countingWeights line 30
theorem OAI.UniformSparsestCut.FiniteWeights.copies_zero line 34
theorem OAI.UniformSparsestCut.FiniteWeights.copies_pos line 37
theorem OAI.UniformSparsestCut.FiniteWeights.copies_lower line 43
theorem OAI.UniformSparsestCut.FiniteWeights.copies_upper line 50
theorem OAI.UniformSparsestCut.FiniteWeights.population_eq_total line 56
theorem OAI.UniformSparsestCut.FiniteWeights.population_bounds line 60
theorem OAI.UniformSparsestCut.FiniteWeights.population_pos line 72
theorem OAI.UniformSparsestCut.FiniteWeights.counting_nonneg line 76
theorem OAI.UniformSparsestCut.FiniteWeights.counting_total line 80

theorem OAI.UniformSparsestCut.FiniteWeights.counting_bounds line 90

Source documentation

On a key of positive weight, the counting law lies within a factor of two of the original probability law.

theorem counting_bounds (K : ℕ) (hK : 0 < K) {p : ι → ℝ}
    (hp : ∀ i, 0 ≤ p i) (hp₁ : total p = 1) (hKm : Fintype.card ι ≤ K)
    (hKp : ∀ i, 0 < p i → 1 ≤ (K : ℝ) * p i) (i : ι) (hpi : 0 < p i) :
    p i / 2 ≤ countingWeights K p i ∧ countingWeights K p i ≤ 2 * p i := by
…

Mentions: OAI.UniformSparsestCut.FiniteWeights.total, OAI.UniformSparsestCut.FiniteWeights.countingWeights

theorem OAI.UniformSparsestCut.FiniteWeights.auxiliary_counting_bound line 110
Source documentation
The total counting mass of auxiliary (zero-retained-demand) vertices.
```
theorem auxiliary_counting_bound (K : ℕ) (hK : 0 < K) {p : ι → ℝ} {κ : ℝ}
    (hp : ∀ i, 0 ≤ p i) (hp₁ : total p = 1) (hκ : 0 < κ)
    (hKlarge : 4 * κ * Fintype.card ι ≤ K) :
    total (auxiliaryWeights (countingWeights K p) p) ≤ 1 / (4 * κ) := by
…
```
Mentions: OAI.UniformSparsestCut.FiniteWeights.total, OAI.UniformSparsestCut.FiniteWeights.auxiliaryWeights, OAI.UniformSparsestCut.FiniteWeights.countingWeights