OAI/Combinatorics/CliqueFree/WeightedGraph.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CliqueFreeIndependence.WeightedGraph.mass line 18
2. def OAI.CliqueFreeIndependence.WeightedGraph.neighbors line 20
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.mem_neighbors line 24
4. def OAI.CliqueFreeIndependence.WeightedGraph.crossMass line 29
5. def OAI.CliqueFreeIndependence.WeightedGraph.edgeMass line 34

   Source documentation

   Unordered edge mass, written as half the directed edge mass.

   noncomputable def edgeMass (G : SimpleGraph V) (w : V → ℝ) : ℝ :=
   …

6. def OAI.CliqueFreeIndependence.WeightedGraph.neighborMass line 37
7. def OAI.CliqueFreeIndependence.WeightedGraph.commonMass line 40
8. def OAI.CliqueFreeIndependence.WeightedGraph.triangleAt line 45

   Source documentation

   Twice the triangle mass in the weighted neighborhood of u.

   noncomputable def triangleAt (G : SimpleGraph V) (w : V → ℝ) (u : V) : ℝ :=
   …

9. def OAI.CliqueFreeIndependence.WeightedGraph.triangleMass line 49

   Source documentation

   Unordered triangle mass, written as one sixth of the ordered triangle mass.

   noncomputable def triangleMass (G : SimpleGraph V) (w : V → ℝ) : ℝ :=
   …

10. def OAI.CliqueFreeIndependence.WeightedGraph.growth line 53

    Source documentation

    The growth function g_x, including its zero convention. Only nonnegative s are used.

    noncomputable def growth (x s : ℝ) : ℝ := s * (x + max 0 (Real.log (1 / s)))

11. def OAI.CliqueFreeIndependence.WeightedGraph.CrossBound line 56

    Source documentation

    The full cross-mass property; sets may overlap.

    def CrossBound (G : SimpleGraph V) (w : V → ℝ) (C : ℝ) : Prop :=
    …

12. lemma OAI.CliqueFreeIndependence.WeightedGraph.mass_nonneg line 62
13. lemma OAI.CliqueFreeIndependence.WeightedGraph.mass_mono line 66
14. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_symm line 70
15. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_nonneg line 78
16. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_le_product line 87
17. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_factor line 97
18. lemma OAI.CliqueFreeIndependence.WeightedGraph.commonMass_comm line 106
19. lemma OAI.CliqueFreeIndependence.WeightedGraph.commonMass_nonneg line 111
20. lemma OAI.CliqueFreeIndependence.WeightedGraph.neighborMass_nonneg line 114
21. lemma OAI.CliqueFreeIndependence.WeightedGraph.commonMass_le_neighborMass line 117
22. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_nonneg line 122
23. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleAt_nonneg line 125
24. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleMass_nonneg line 129
25. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_eq_sum line 133
26. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleMass_eq_sum line 140
27. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleAt_le line 145
28. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleMass_le_of_neighborMass line 153
29. lemma OAI.CliqueFreeIndependence.WeightedGraph.neighborMass_ge_of_commonMass line 163
30. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleAt_ge_of_commonMass line 169
31. lemma OAI.CliqueFreeIndependence.WeightedGraph.commonMass_eq_sum line 177
32. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_all_right line 184
33. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_all_left line 190
34. lemma OAI.CliqueFreeIndependence.WeightedGraph.crossMass_neighbors line 194