WeightReplacement.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Replacing vertices of zero retained demand

The replacement coupling of Section 7 of OpenAI's Constant-factor hardness of uniform sparsest cut keeps a draw of positive retained demand and replaces every other draw by an independent retained-demand draw. Its color-change probability controls the change in Boolean variance.

def OAI.UniformSparsestCut.FiniteWeights.auxiliaryWeights line 19
Source documentation
The original law restricted to keys with zero retained demand.
```
noncomputable def auxiliaryWeights (w retained : ι → ℝ) : ι → ℝ := by
…
```
def OAI.UniformSparsestCut.FiniteWeights.supportedWeights line 24
Source documentation
The original law restricted to keys with nonzero retained demand.
```
noncomputable def supportedWeights (w retained : ι → ℝ) : ι → ℝ := by
…
```
def OAI.UniformSparsestCut.FiniteWeights.replacementWeights line 29
Source documentation
Retain supported draws and replace all others by an independent retained-demand draw.
```
noncomputable def replacementWeights (w retained : ι → ℝ) : ι → ℝ :=
…
```
theorem OAI.UniformSparsestCut.FiniteWeights.weights_decomposition line 33
theorem OAI.UniformSparsestCut.FiniteWeights.total_decomposition line 38
theorem OAI.UniformSparsestCut.FiniteWeights.mass_decomposition line 45
theorem OAI.UniformSparsestCut.FiniteWeights.auxiliary_nonneg line 53
theorem OAI.UniformSparsestCut.FiniteWeights.supported_nonneg line 63
theorem OAI.UniformSparsestCut.FiniteWeights.auxiliary_le line 73
theorem OAI.UniformSparsestCut.FiniteWeights.auxiliary_total_le_one line 82
theorem OAI.UniformSparsestCut.FiniteWeights.replacement_nonneg line 86
theorem OAI.UniformSparsestCut.FiniteWeights.replacement_total line 92
theorem OAI.UniformSparsestCut.FiniteWeights.replacement_mass line 99
theorem OAI.UniformSparsestCut.FiniteWeights.replacement_le_three line 107
Source documentation
Domination of the replacement law before comparison with the original score law.
```
theorem replacement_le_three {w retained : ι → ℝ} (hw : ∀ i, 0 ≤ w i)
    (hw₁ : total w = 1) (hr : ∀ i, 0 ≤ retained i)
    (hrep : ∀ i, 0 < retained i → w i ≤ 2 * retained i) :
    ∀ i, replacementWeights w retained i ≤ 3 * retained i := by
…
```
Mentions: OAI.UniformSparsestCut.FiniteWeights.total, OAI.UniformSparsestCut.FiniteWeights.replacementWeights
theorem OAI.UniformSparsestCut.FiniteWeights.replacement_mass_change line 124
Source documentation
The actual color-change cost of the replacement experiment bounds both signed changes in the probability of color one.
```
theorem replacement_mass_change {w retained : ι → ℝ} (hw : ∀ i, 0 ≤ w i)
    (hr : ∀ i, 0 ≤ retained i) (hr₁ : total retained = 1) (h : ι → Bool) :
    mass w h - mass (replacementWeights w retained) h ≤
        disagreement (auxiliaryWeights w retained) retained h ∧
    mass (replacementWeights w retained) h - mass w h ≤
        disagreement (auxiliaryWeights w retained) retained h := by
…
```
Mentions: OAI.UniformSparsestCut.FiniteWeights.total, OAI.UniformSparsestCut.FiniteWeights.mass, OAI.UniformSparsestCut.FiniteWeights.replacementWeights, OAI.UniformSparsestCut.FiniteWeights.disagreement, OAI.UniformSparsestCut.FiniteWeights.auxiliaryWeights
theorem OAI.UniformSparsestCut.FiniteWeights.variance_transfer line 146
Source documentation
Variance transfer for the replacement coupling in Section 7 of Constant-factor hardness of uniform sparsest cut.
Here w is the counting law on clusters, μ the original score demand law, and retained the normalized retained demand. Zero retained mass is allowed. The final term is the probability that replacement changes the color, denoted L_aux in the paper.
```
theorem variance_transfer {w μ retained : ι → ℝ}
    (hw : ∀ i, 0 ≤ w i) (hμ : ∀ i, 0 ≤ μ i) (hr : ∀ i, 0 ≤ retained i)
    (hw₁ : total w = 1) (hμ₁ : total μ = 1) (hr₁ : total retained = 1)
    (hret : ∀ i, retained i ≤ 2 * μ i)
    (hrep : ∀ i, 0 < retained i → w i ≤ 2 * retained i) (h : ι → Bool) :
    variance w h ≤ 36 * variance μ h + disagreement (auxiliaryWeights w retained) retained h := by
…
```
Mentions: OAI.UniformSparsestCut.FiniteWeights.total, OAI.UniformSparsestCut.FiniteWeights.variance, OAI.UniformSparsestCut.FiniteWeights.disagreement, OAI.UniformSparsestCut.FiniteWeights.auxiliaryWeights