OAI/Combinatorics/CliqueFree/TriangleBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.of_le line 18
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.neighborMass_bot line 22
3. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleMass_bot line 25
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.splittingConstant_nonneg line 28
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.neighborhood_reduction line 33

   Source documentation

   One reduction step, allowing an arbitrary finite vertex type of copies.

   lemma neighborhood_reduction (G : SimpleGraph V) {w : V → ℝ} (hw : ∀ u, 0 < w u)
       {C x : ℝ} (hC : 1 ≤ C) (hCross : CrossBound G w C) (hx : 32 ≤ x)
       (hε : splittingConstant C * Numerical.lossRatio x ≤ 1)
       (hL : ∀ u, neighborMass G w u ≤ Real.exp x) :
       ∃ (U : Type u) (_ : Fintype U) (J : SimpleGraph U) (π : U → V),
         EdgeProjection J G π ∧ (∀ a, neighborMass J (w ∘ π) a ≤ Real.exp (Real.sqrt x)) ∧
         (1-splittingConstant C * Numerical.lossRatio x) * triangleMass G w - edgeMass G w / x ≤
           triangleMass J (w ∘ π) := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.CrossBound, OAI.CliqueFreeIndependence.WeightedGraph.splittingConstant, OAI.CliqueFreeIndependence.Numerical.lossRatio, OAI.CliqueFreeIndependence.WeightedGraph.neighborMass, OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection, OAI.CliqueFreeIndependence.WeightedGraph.triangleMass, OAI.CliqueFreeIndependence.WeightedGraph.edgeMass

6. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangle_bound_scale line 79

   Source documentation

   Uniform triangle bound at the reverse-squaring scale.

   lemma triangle_bound_scale {C X : ℝ} (hC : 1 ≤ C) (hX : 32 ≤ X)
       (hsmall : splittingConstant C * Numerical.lossRatio X ≤ 1/4) (n : ℕ) :
       ∀ {V : Type u} [Fintype V] (G : SimpleGraph V) (w : V → ℝ),
         (∀ u, 0 < w u) → CrossBound G w C →
         (∀ u, neighborMass G w u ≤ Real.exp (Numerical.scale X n)) →
         triangleMass G w ≤ (1+Real.exp X/3) * (2-(1/2:ℝ)^n) * edgeMass G w := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.splittingConstant, OAI.CliqueFreeIndependence.Numerical.lossRatio, OAI.CliqueFreeIndependence.WeightedGraph.CrossBound, OAI.CliqueFreeIndependence.WeightedGraph.neighborMass, OAI.CliqueFreeIndependence.Numerical.scale, OAI.CliqueFreeIndependence.WeightedGraph.triangleMass, OAI.CliqueFreeIndependence.WeightedGraph.edgeMass

7. theorem OAI.CliqueFreeIndependence.WeightedGraph.weighted_triangles line 141

   Source documentation

   The weighted triangle theorem with a size-independent constant.

   theorem weighted_triangles {C : ℝ} (hC : 1 ≤ C) :
       ∃ B : ℝ, 0 < B ∧ ∀ {V : Type u} [Fintype V] (G : SimpleGraph V) (w : V → ℝ),
         (∀ v, 0 < w v) → CrossBound G w C → triangleMass G w ≤ B * edgeMass G w := by
   …

   Mentions: OAI.CliqueFreeIndependence.WeightedGraph.CrossBound, OAI.CliqueFreeIndependence.WeightedGraph.triangleMass, OAI.CliqueFreeIndependence.WeightedGraph.edgeMass