OAI/Combinatorics/CliqueFree/MultiplierLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CliqueFreeIndependence.WeightedGraph.restrict line 20

    Source documentation

    A weight vector restricted to a vertex set.

    noncomputable def restrict (A : Finset V) (w : V → ℝ) : V → ℝ := fun v ↦ if v ∈ A then w v else 0
  2. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_smul line 22
  3. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_restrict line 36
  4. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_restrict line 59
  5. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_restrict_le line 62
  6. def OAI.CliqueFreeIndependence.WeightedGraph.BoundedOn line 72

    Source documentation

    Bounded multipliers supported on A, regardless of the lottery weight of the entry.

    def BoundedOn (L : Law (V → ℝ)) (A : Finset V) (b : ℝ) : Prop :=
…
  7. def OAI.CliqueFreeIndependence.WeightedGraph.expectedEdges line 75
  8. lemma OAI.CliqueFreeIndependence.WeightedGraph.expectedEdges_transform line 78
  9. lemma OAI.CliqueFreeIndependence.WeightedGraph.mean_transform line 92
  10. lemma OAI.CliqueFreeIndependence.WeightedGraph.bounded_transform line 100
  11. lemma OAI.CliqueFreeIndependence.WeightedGraph.bounded_append line 110
  12. lemma OAI.CliqueFreeIndependence.WeightedGraph.normalize_subprob line 118