WeightNormalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Normalization of finite weights

A lower approximation to a probability law retains coordinatewise domination and setwise lower bounds after normalization. These are the retained-demand estimates in Section 7 of OpenAI's Constant-factor hardness of uniform sparsest cut.

def OAI.UniformSparsestCut.FiniteWeights.normalized line 24
theorem OAI.UniformSparsestCut.FiniteWeights.normalized_nonneg line 26
theorem OAI.UniformSparsestCut.FiniteWeights.normalized_total line 30
theorem OAI.UniformSparsestCut.FiniteWeights.normalized_mass line 35
theorem OAI.UniformSparsestCut.FiniteWeights.normalized_le_twice line 44
Source documentation
Normalization of a sufficiently large lower approximation increases each weight by at most a factor of two.
```
theorem normalized_le_twice {μ l : ι → ℝ} {ε : ℝ}
    (hμ : ∀ i, 0 ≤ μ i) (hle : ∀ i, l i ≤ μ i)
    (hε : ε ≤ 1 / 2) (hL : 1 - ε ≤ total l) :
    ∀ i, normalized l i ≤ 2 * μ i := by
…
```
Mentions: OAI.UniformSparsestCut.FiniteWeights.total, OAI.UniformSparsestCut.FiniteWeights.normalized

theorem OAI.UniformSparsestCut.FiniteWeights.normalized_event_lower line 55

Source documentation

Every finite event loses at most the discarded mass after normalization.

theorem normalized_event_lower {μ l : ι → ℝ} {ε : ℝ}
    (hl : ∀ i, 0 ≤ l i) (hle : ∀ i, l i ≤ μ i) (hμ₁ : total μ = 1)
    (hε : ε ≤ 1 / 2) (hL : 1 - ε ≤ total l) (E : Finset ι) :
    (∑ i ∈ E, μ i) - ε ≤ ∑ i ∈ E, normalized l i := by
…

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