OAI/Combinatorics/SparsestCut/FiniteWeights.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Finite Boolean weights and variances

Finite weighted laws support Boolean event masses, complementary masses, and the disagreement of independent draws. The variance estimates give scalar ingredients for the finite graph construction in Section 7 of Constant-factor hardness of uniform sparsest cut.

  1. def OAI.UniformSparsestCut.FiniteWeights.indicator line 25
  2. def OAI.UniformSparsestCut.FiniteWeights.disagree line 27
  3. def OAI.UniformSparsestCut.FiniteWeights.total line 29
  4. def OAI.UniformSparsestCut.FiniteWeights.mass line 31
  5. def OAI.UniformSparsestCut.FiniteWeights.variance line 33
  6. def OAI.UniformSparsestCut.FiniteWeights.disagreement line 36

    Source documentation

    The weight of a disagreement for two independent draws (not necessarily normalized).

    def disagreement (w u : ι → ℝ) (h : ι → Bool) : ℝ :=
…
  7. theorem OAI.UniformSparsestCut.FiniteWeights.indicator_nonneg line 39
  8. theorem OAI.UniformSparsestCut.FiniteWeights.indicator_le_one line 42
  9. theorem OAI.UniformSparsestCut.FiniteWeights.indicator_not line 45
  10. theorem OAI.UniformSparsestCut.FiniteWeights.disagree_nonneg line 48
  11. theorem OAI.UniformSparsestCut.FiniteWeights.disagree_eq line 51
  12. theorem OAI.UniformSparsestCut.FiniteWeights.total_nonneg line 55
  13. theorem OAI.UniformSparsestCut.FiniteWeights.total_mono line 58
  14. theorem OAI.UniformSparsestCut.FiniteWeights.total_add line 61
  15. theorem OAI.UniformSparsestCut.FiniteWeights.total_smul line 64
  16. theorem OAI.UniformSparsestCut.FiniteWeights.mass_nonneg line 67
  17. theorem OAI.UniformSparsestCut.FiniteWeights.mass_le_total line 70
  18. theorem OAI.UniformSparsestCut.FiniteWeights.mass_mono line 76
  19. theorem OAI.UniformSparsestCut.FiniteWeights.mass_add line 81
  20. theorem OAI.UniformSparsestCut.FiniteWeights.mass_smul line 85
  21. theorem OAI.UniformSparsestCut.FiniteWeights.mass_compl line 89
  22. theorem OAI.UniformSparsestCut.FiniteWeights.variance_nonneg line 93
  23. theorem OAI.UniformSparsestCut.FiniteWeights.inner_disagreement line 97
  24. theorem OAI.UniformSparsestCut.FiniteWeights.disagreement_eq line 111
  25. theorem OAI.UniformSparsestCut.FiniteWeights.disagreement_self line 126
  26. theorem OAI.UniformSparsestCut.FiniteWeights.disagreement_nonneg line 132
  27. theorem OAI.UniformSparsestCut.FiniteWeights.variance_domination line 139

    Source documentation

    Product domination: the constant is squared, since the two draws are independent.

    theorem variance_domination {w u : ι → ℝ} {A : ℝ}
    (hw : ∀ i, 0 ≤ w i) (hu : ∀ i, 0 ≤ u i)
    (hw₁ : total w = 1) (hu₁ : total u = 1) (hA : 0 ≤ A)
    (hdom : ∀ i, w i ≤ A * u i) (h : ι → Bool) :
    variance w h ≤ A ^ 2 * variance u h := by
…

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

  28. theorem OAI.UniformSparsestCut.FiniteWeights.variance_change line 157

    Source documentation

    A change of color with probability at most L changes Boolean variance by at most L. This scalar estimate also follows by coupling two independent draws and a union bound.

    theorem variance_change {z r L : ℝ} (hz₀ : 0 ≤ z) (hz₁ : z ≤ 1)
    (hr₀ : 0 ≤ r) (hr₁ : r ≤ 1) (h₁ : z - r ≤ L) (h₂ : r - z ≤ L) :
    z * (1 - z) ≤ r * (1 - r) + L := by
…