Lifting a decomposition after triangle peeling #
The peeled graph has fewer edges. Its fractional triangle weights extend by zero, and weight one on the removed triangle restores exact edge coverage.
theorem
LeanPool.DrossFractionalTriangleDecomposition.peeled_heavy_triangle_fewer_edges
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{u v w : V}
(huv : G.Adj u v)
(huw : G.Adj u w)
(hvw : G.Adj v w)
:
theorem
LeanPool.DrossFractionalTriangleDecomposition.cliqueFinset_deleteEdges_subset
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(S : Finset (Sym2 V))
(n : ℕ)
:
(G.deleteEdges ↑S).cliqueFinset n ⊆ G.cliqueFinset n
theorem
LeanPool.DrossFractionalTriangleDecomposition.sum_truncated_cliques
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(S : Finset (Sym2 V))
(n : ℕ)
(a : Finset V → ℝ)
(e : Sym2 V)
:
(∑ t ∈ G.cliqueFinset n, if e ∈ triEdges t then if t ∈ (G.deleteEdges ↑S).cliqueFinset n then a t else 0 else 0) = ∑ t ∈ (G.deleteEdges ↑S).cliqueFinset n, if e ∈ triEdges t then a t else 0
theorem
LeanPool.DrossFractionalTriangleDecomposition.deleted_edge_not_in_clique
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
(S : Finset (Sym2 V))
{e : Sym2 V}
(heS : e ∈ S)
{n : ℕ}
{t : Finset V}
(ht : t ∈ (G.deleteEdges ↑S).cliqueFinset n)
:
e ∉ triEdges t
theorem
LeanPool.DrossFractionalTriangleDecomposition.triangle_indicator_sum
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{u v w : V}
(huv : G.Adj u v)
(huw : G.Adj u w)
(hvw : G.Adj v w)
(e : Sym2 V)
:
theorem
LeanPool.DrossFractionalTriangleDecomposition.lift_fractional_decomp_triangle
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{u v w : V}
(huv : G.Adj u v)
(huw : G.Adj u w)
(hvw : G.Adj v w)
(hdec : FractionalTriangleDecomp (G.deleteEdges ↑(triEdges {u, v, w})))
: