Turán's theorem (the "Book" weighting proof)

This file formalizes the weighting/optimization proof of Turán's theorem from Proofs from THE BOOK. Starting from any vertex weight distribution on a p-clique-free simple graph, the weight is concentrated onto a clique and then equalized; the resulting bound on the total edge weight yields the classical upper bound (1/2)(1 - 1/(p-1)) n² on the number of edges.

All declarations live in the Turan3 namespace.

structure Turan3.FunToMax {α : Type u_1} (G : SimpleGraph α) [Fintype α] : Type u_1

Structure FunToMax : Represents weight distribution on the vertex set, all weights sum up to 1.

• w : α → NNReal

  The weight assigned to each vertex.

• h_w : ∑ v : α, self.w v = 1

  The weights sum to one over all vertices.

def Turan3.vp {α : Type u_1} (w : α → NNReal) (e : Sym2 α) : NNReal

Computes the weight contribution of an edge multiplying the edge's vertice's weights

Equations

• Turan3.vp w e = Quot.liftOn e (fun (pair : α × α) => w pair.1 * w pair.2) ⋯

def Turan3.FunToMax.fw {α : Type u_1} [Fintype α] {G : SimpleGraph α} [DecidableRel G.Adj] (W : FunToMax G) : NNReal

computes the total edge weight of the graph with respect to the weight function W by summing vp W.w e over all edges

Equations

• W.fw = ∑ e ∈ G.edgeFinset, Turan3.vp W.w e

Section 1: Concentrating weights on a clique

Starting from any weight function W, we “improve” it without decreasing fw until its support is a clique.

1. We have an better performing wegith distribution Better with • zeros preserved • support size = m • Better.fw ≥ W.fw

2. m finds the minimal support size (for Better) we can achieve without decreasing the total edge weight Better.fw ≥ W.fw.

3. We define the operation Improve which moves all weight from one vertex loose to another gain (non adjacent). • Improve_total_weight_nondec: shoes the total value fw is equal or greater • ImproveReducesSupportSize: support size strictly decreases under Improve

4. By minimality of m, Better_forms_clique shows by contradiction that the final support forms a clique.

theorem Turan3.exists_better_distribution {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : ∃ (num : ℕ) (better : FunToMax G), (∀ (i : α), W.w i = 0 → better.w i = 0) ∧ {i : α | better.w i > 0}.card = num ∧ W.fw ≤ better.fw

States that for any weight function W : FunToMax G, there exists a natural number m and a new weight function (better) such that:

• The support of the new weight function is included in that of W (vertices with weight 0 remain 0 under better),
• The number of vertices with positive weight is exactly m (support size), and
• The total edge weight of the new weight function is equal or greater than that of W.

noncomputable def Turan3.m {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : ℕ

computes the smallest possible "m" satisfying the properties under exists_better_distribution for a weight function W

Equations

• Turan3.m G W = Nat.find ⋯

theorem Turan3.exists_better_distribution_min_support {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : ∃ (better : FunToMax G), (∀ (i : α), W.w i = 0 → better.w i = 0) ∧ {i : α | better.w i > 0}.card = m G W ∧ W.fw ≤ better.fw

Guarantees that for a distribution W, an "improved" one (better) exists where :

• vertices with weight 0 remain 0,
• Support size (vertices with positive weight) is equal to m (smallest possible "m" satisfying exists_better_distribution for a weight function `W)
• Has non decreasing total weight (fw) than the original distribution.

noncomputable def Turan3.Better {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : FunToMax G

Returns an improved weight function under the conditions of exists_better_distribution_min_support

• vertices with weight 0 remain 0,
• Support size (vertices with positive weight) is equal to m (minimal size)
• Has non decreasing total weight (fw) than the original distribution..

Equations

• Turan3.Better G W = Classical.choose ⋯

theorem Turan3.Better_support_included {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (i : α) (hi : W.w i = 0) : (Better G W).w i = 0

Ensures that vertices with weght 0 remain 0 under Better

theorem Turan3.Better_support_size {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : {i : α | (Better G W).w i > 0}.card = m G W

Ensures that the support is size m under Better

theorem Turan3.Better_non_decr {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : W.fw ≤ (Better G W).fw

Ensures that the total edge weight computed by Better is equal or larger as that of W.

def Turan3.Improve {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : FunToMax G

Constructs a new weight function by redistributing weight from one vertex (loose) to another (gain) (distinct vertices). The new function zeros out the weight at loose and adds it to gain (thus preserving the total weight).

Equations

• Turan3.Improve G W loose gain h_neq = { w := fun (i : α) => if i = loose then 0 else if i = gain then W.w gain + W.w loose else W.w i, h_w := ⋯ }

theorem Turan3.helper_gain_mem {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {gain : α} (e : Sym2 α) (he : e ∈ G.incidenceFinset gain) : gain ∈ e

Helper lemma: Given that an edge e is part of gain's incidence set, this lemma proves that gain is in e.

theorem Turan3.gain_edge_decomp {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (gain : α) (e : Sym2 α) (he : e ∈ G.incidenceFinset gain) : vp W.w e = W.w gain * W.w (Sym2.Mem.other ⋯)

Helper lemma : Calculates the value (vp) of an edge e, where gain is one of the vertices in e, as the product of gain and the other vertex v, in e.

theorem Turan3.gain_edge_sum {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (gain : α) : ∑ e ∈ G.incidenceFinset gain, vp W.w e = W.w gain * ∑ e ∈ (G.incidenceFinset gain).attach, W.w (Sym2.Mem.other ⋯)

Helper lemma : Shows that the sum of values of the edges incident to gain is equal to the product of the weight of gain and the sum of the other vertices incident to gain.

theorem Turan3.loose_edge_sum {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose : α) : ∑ e ∈ G.incidenceFinset loose, vp W.w e = W.w loose * ∑ e ∈ (G.incidenceFinset loose).attach, W.w (Sym2.Mem.other ⋯)

Helper lemma : Shows that the sum of values of the edges incident to loose is equal to the product of the weight of loose and the sum of the other vertices incident to loose.

theorem Turan3.edge_mem_iff {α : Type u_1} (G : SimpleGraph α) {v w : α} : G.Adj v w ↔ ∃ e ∈ G.edgeSet, e = s(v, w)

Helper lemma : Shows that two vertices are adjacent if and only if there exists an edge in the edge set corresponding to them.

theorem Turan3.incidenceFinset_subset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (v : α) : G.incidenceFinset v ⊆ G.edgeFinset

Helper lemma : States that the incidence set of any vertex is a subset of the entire edge set.

@[simp]

theorem Turan3.Improve_w_eq {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : (Improve G W loose gain h_neq).w = fun (i : α) => if i = loose then 0 else if i = gain then W.w gain + W.w loose else W.w i

Helper lemma: shows that the weight function created by Improve W loose gain h_neq is equal to its "lambda-if function"

@[simp]

theorem Turan3.vp_sym2_mk {α : Type u_1} (w : α → NNReal) (a b : α) : vp w s(a, b) = w a * w b

Helper lemma : shows that the value computed by the function vp is exactly w(a) * w(b)

theorem Turan3.Improve_loose_weight_zero {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : (Improve G W loose gain h_neq).w loose = 0

Helper lemma: Shows that the weight at the vertex “loose” is 0 after Improve.

theorem Turan3.Improve_gain_loose_disjoint {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {loose gain : α} (h_neq : gain ≠ loose) (h_adj : ¬G.Adj gain loose) : Disjoint (G.incidenceFinset gain) (G.incidenceFinset loose)

Helper lemma: Shows that the incidence sets of gain and loose are disjoint (Assuming they are not adjacent).

theorem Turan3.Improve_partition_sum_split {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) (h_adj : ¬G.Adj gain loose) : have affectedEdges := (G.incidenceFinset gain).disjUnion (G.incidenceFinset loose) ⋯; ∑ e ∈ G.edgeFinset, vp W.w e = ∑ e ∈ G.incidenceFinset gain, vp W.w e + ∑ e ∈ G.incidenceFinset loose, vp W.w e + ∑ e ∈ G.edgeFinset \ affectedEdges, vp W.w e

Using the same definition affectedEdges, translates the partition into an equality of Sums. Shows that the toal edge weight is equal to

• The sum over the edges incident to gain
• The sum over the edges incident to loose
• The sum over the remaining edges (the ones in G\affectedEdges)

theorem Turan3.Improve_gain_contribution_increase {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) (h_adj : ¬G.Adj gain loose) : ∑ e ∈ G.incidenceFinset gain, vp (Improve G W loose gain h_neq).w e = ∑ e ∈ G.incidenceFinset gain, vp W.w e + W.w loose * ∑ e ∈ (G.incidenceFinset gain).attach, W.w (Sym2.Mem.other ⋯)

Shows that after Improve the total edge value over the edges incident to gain increases exactly by the weight of loose multiplied by the sum of the ("other") vertex weights incident to gain.

theorem Turan3.Improve_loose_contribution_zero {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : ∑ e ∈ G.incidenceFinset loose, vp (Improve G W loose gain h_neq).w e = 0

Shows that after Improve, the sum of edge values over the incidence set of loose is zero.

theorem Turan3.Improve_unchanged_edge_sum {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) (h_adj : ¬G.Adj gain loose) : have affectedEdges := (G.incidenceFinset gain).disjUnion (G.incidenceFinset loose) ⋯; ∑ e ∈ G.edgeFinset \ affectedEdges, vp (Improve G W loose gain h_neq).w e = ∑ e ∈ G.edgeFinset \ affectedEdges, vp W.w e

Shows that the edges not incident to gain or loose (not in affectedEdges) have the same weightw under the Improve operation

theorem Turan3.Improve_total_weight_nondec {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h : ∑ e ∈ (G.incidenceFinset gain).attach, W.w (Sym2.Mem.other ⋯) ≥ ∑ e ∈ (G.incidenceFinset loose).attach, W.w (Sym2.Mem.other ⋯)) (h_neq : gain ≠ loose) (h_adj : ¬G.Adj gain loose) : (Improve G W loose gain h_neq).fw ≥ W.fw

Assumption h mirrors the assumption s_1 ≤ s_2 in the informal proof. This lemma shows that the total edge weight does not decrease under Improve, using the previous lemmas:

• Improve_partition_sum_split: splits the edge set into the sum of : edges incident to gain, edges incident to loose, the remaining edges
• Improve_unchanged_edge_sum: shows all edges not incident to "loose" or "gain" remain unchanged.
• Improve_gain_contribution_increase: shows that gain’s contribution increases by the weight of loose times the other values incident to "gain"
• Improve_loose_contribution_zero: shows that loose’s new contribution is zero

theorem Turan3.Improve_support_remains_zero {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) (h_supp : 0 < W.w gain) (i : α) : W.w i = 0 → (Improve G W loose gain h_neq).w i = 0

Shows that if a vertex has weight 0 , then the weight remains 0 under the Improved function.

theorem Turan3.Improve_support_strictly_reduced {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) (h_supp1 : 0 < W.w gain) (h_supp2 : 0 < W.w loose) : {i : α | (Improve G W loose gain h_neq).w i > 0}.card < {i : α | W.w i > 0}.card

Using Improve_support_remains_zero, shows that the support under Improve is strictly smaller than that of the original weight function W

theorem Turan3.Better_forms_clique {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : G.IsClique ↑{i : α | (Better G W).w i > 0}

Proves that the support of Better is a clique. If two support vertices (gain,loose) were non‑adjacent, shows wlog that loose has at least as large a neighbor‐sum as gain, then applies Improve to move all the weight from loose to gain. By

• Improve_total_weight_nondec: fw does not decrease, and
• Improve_support_strictly_reduced: the support strictly shrinks,

this contradicts the minimality of Better’s support size m. Therefore no such non‑adjacent pair exists.

Section 2:

We aim to show that any non‑uniform weight distribution on a clique can be further improved by a small transfer:

1. Define Enhance to move a tiny ε (with 0 < ε < W.w loose – W.w gain) from loose to gain.

2. Proves with Enhance_total_weightstricinc that under Enhance:

   • the support remains the same clique,
   • only loose and gain change weight,
   • the total edge‐weight fw is strictly increasing.

noncomputable def Turan3.Enhance {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) : FunToMax G

Constructs a new weight function by moving a small amount of weight ε < W(loose) - W(gain) from vertex loose to vertex gain assuming W.w gain < W.w loose. It preservers the total weight improving the weight function

Equations

• Turan3.Enhance G W loose gain h_lt ε epos elt = { w := fun (i : α) => if i = loose then W.w loose - ε else if i = gain then W.w gain + ε else W.w i, h_w := ⋯ }

theorem Turan3.neq_of_W_lt {α : Type u_1} (G : SimpleGraph α) [Fintype α] {W : FunToMax G} {loose gain : α} (h_neq : W.w gain < W.w loose) : gain ≠ loose

Helper lemma: deduces that if gain and loose have different weights then gain and loose arent the same vertex

theorem Turan3.NNReal.eq_zero_of_ne_pos {x : NNReal} (h : ¬x > 0) : x = 0

Helper lemma: if (NNReal) is not positive it must be 0

theorem Turan3.Enhance_nsupport_unchanged {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ah : 0 < W.w gain) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (i : α) : W.w i = 0 ↔ (Enhance G W loose gain h_lt ε epos elt).w i = 0

Shows that after applying Enhance, vertices that had weight 0, remain with the same weight 0 (Support is preserved).

theorem Turan3.Enhance_support_unchanged {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ah : 0 < W.w gain) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (i : α) : W.w i > 0 ↔ (Enhance G W loose gain h_lt ε epos elt).w i > 0

Complement of Enhance_support_zero: shows that a vertex has positive weight in W if and only if it has positive weight in the Enhanced function (Support is preserved).

theorem Turan3.Enhance_clique {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ah : 0 < W.w gain) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) : G.IsClique ↑{i : α | (Enhance G W loose gain h_lt ε epos elt).w i > 0}

Proves that after applying Enhance the support still forms a clique

def Turan3.inSupport {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (e : Sym2 α) : Prop

Helper definition: Defines that an edge (element of the structur Sym2 α) is "Supported" if both of its vertices have positive weight (according to a weight function W)

Equations

• Turan3.inSupport G W e = Quot.lift (fun (x : α × α) => W.w x.1 > 0 ∧ W.w x.2 > 0) ⋯ e

theorem Turan3.inSupport_explicit {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) {x y : α} : inSupport G W s(x, y) ↔ W.w x > 0 ∧ W.w y > 0

Helper lemma : states the explicit characterization of an edge being in the Support, meaning both vertices must have positive weights.

theorem Turan3.notinSupport {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) {e : Sym2 α} (h : ¬inSupport G W e) : vp W.w e = 0

Helper lemma: If an edge e is not in the support, then the value of e (using vp) is 0.

theorem Turan3.inSupport_mem {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) {x : α} {e : Sym2 α} (hm : x ∈ e) (hs : inSupport G W e) : W.w x > 0

Helper lemma: Shows that if an edge e is in support and a vertex x belongs to e, then x has positive weight

theorem Turan3.inSupport_other {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) {x : α} {e : Sym2 α} (hm : x ∈ e) (hs : inSupport G W e) : W.w (Sym2.Mem.other hm) > 0

Helper lemma: Shows that if an edge e is in support and x is part of e, then the weight of the other vertice in e is positive.

theorem Turan3.inSupport_rec {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) {e : Sym2 α} (h : ∀ x ∈ e, W.w x > 0) : inSupport G W e

Helper lemma: Proves that if all vertices in an edge e have positives weights, then e is in the support.

@[implicit_reducible]

noncomputable instance Turan3.instDecidablePredInSupport {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : DecidablePred (inSupport G W)

Decidability of inSupport, used to filter edge finsets by it.

Equations

• Turan3.instDecidablePredInSupport G W = Classical.decPred (Turan3.inSupport G W)

noncomputable def Turan3.supIncidenceFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (v : α) : Finset (Sym2 α)

definition: Defines the subset of a vertex's incident set, that consists of supported edges

Equations

• Turan3.supIncidenceFinset G W v = Finset.filter (Turan3.inSupport G W) (G.incidenceFinset v)

noncomputable def Turan3.supEdgeFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : Finset (Sym2 α)

definition: Defines the subset of the whole edge set, where the edges are supported

Equations

• Turan3.supEdgeFinset G W = Finset.filter (Turan3.inSupport G W) G.edgeFinset

theorem Turan3.mem_supIncidenceFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {W : FunToMax G} {v : α} {e : Sym2 α} : e ∈ supIncidenceFinset G W v ↔ e ∈ G.incidenceFinset v ∧ inSupport G W e

Helper lemma: Explicitly characterizes the definition of supIncidenceFinset:

• edges are incident to the vertex
• edges are supported

theorem Turan3.mem_supEdgeFinset {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] {W : FunToMax G} {e : Sym2 α} : e ∈ supEdgeFinset G W ↔ e ∈ G.edgeFinset ∧ inSupport G W e

Helper lemma: Explicitly caracterizes the definition of supEdgeFinset :

• edges are in the edge set of the graph
• edges are supported

theorem Turan3.small_helpI {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] {W : FunToMax G} {v : α} {e : Sym2 α} (h : e ∈ supIncidenceFinset G W v) : e ∈ G.incidenceFinset v

Helper lemma: Shows that any edge part of an supported incident set of a vertex, is also part of whole incident set of v.

theorem Turan3.in_sdiff_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∈ s \ t) : a ∈ s

Helper lemma : extracts from the fact that an element a belongs to the set difference s \ t that a is indeed in s.

theorem Turan3.disjoint_supported_incidence {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : Disjoint (supIncidenceFinset G W gain \ {s(loose, gain)}) (supIncidenceFinset G W loose \ {s(loose, gain)})

Shows that for a weight function W (and distinct loose and gain), the supported incidence sets of gain and loose (without the edge (gain,loose) are disjoint)

noncomputable def Turan3.incidenceLooseGain {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : Finset (Sym2 α)

Using disjoint_supported_incidence defines the disjoint union of the supported incidence sets of gain (without edge (gain,loose)) and that of loose (without edge (gain, loose)).

Equations

• Turan3.incidenceLooseGain G W loose gain h_neq = (Turan3.supIncidenceFinset G W gain \ {s(loose, gain)}).disjUnion (Turan3.supIncidenceFinset G W loose \ {s(loose, gain)}) ⋯

theorem Turan3.disjoint_inci_singleton {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : Disjoint (incidenceLooseGain G W loose gain h_neq) {s(loose, gain)}

shows that the set incidenceLooseGain is disjoint from the singleton s(loose, gain)

noncomputable def Turan3.inciLooseGainFull {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_neq : gain ≠ loose) : Finset (Sym2 α)

Extends incidenceLooseGain by taking its disjoint union with s(loose,gain) (using disjoint_inci_singleton)

Equations

• Turan3.inciLooseGainFull G W loose gain h_neq = (Turan3.incidenceLooseGain G W loose gain h_neq).disjUnion {s(loose, gain)} ⋯

theorem Turan3.supported_edge_partition {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_adj : G.Adj gain loose) (h_supp : W.w loose > 0 ∧ W.w gain > 0) : supEdgeFinset G W = (inciLooseGainFull G W loose gain ⋯).disjUnion (supEdgeFinset G W \ inciLooseGainFull G W loose gain ⋯) ⋯

Shows that if vertices in the support gain and loose are adjacent, then the supported edge set can be decomposed as a disjoint union of inciLooseGainFull and its complement

theorem Turan3.sum_over_support {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : ∑ e ∈ G.edgeFinset, vp W.w e = ∑ e ∈ supEdgeFinset G W, vp W.w e

Helper lemma: Shows that the total edge value obtained by summing vp W.w e over the whole edge set is the same as the sum taken only over the supported edges, (those in supEdgeFinset).

theorem Turan3.Enhance_gain_sum {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) : ∑ e ∈ supIncidenceFinset G W gain \ {s(loose, gain)}, vp (Enhance G W loose gain h_lt ε epos elt).w e = ∑ e ∈ supIncidenceFinset G W gain \ {s(loose, gain)}, vp W.w e + ε * ∑ e ∈ (supIncidenceFinset G W gain \ {s(loose, gain)}).attach, W.w (Sym2.Mem.other ⋯)

Shows that the sum over the supported incidence set of gain (without s(loose,gain)) after Enhance transformation, equals the original sum plus ε times the sum over the gain-attached incident set

theorem Turan3.epsilon_weight_bound {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (_epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (e : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) : e ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach → ε * W.w (Sym2.Mem.other ⋯) ≤ vp W.w ↑e

Helper: provides a bound: for any edge in the supported incidence set of loose (without s(loose,gain)), the product of ε and the weight of the "other" vertex is bounded by the edge's value

theorem Turan3.Enhance_loose_sum {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) : ∑ e ∈ supIncidenceFinset G W loose \ {s(loose, gain)}, vp (Enhance G W loose gain h_lt ε epos elt).w e = ∑ e ∈ supIncidenceFinset G W loose \ {s(loose, gain)}, vp W.w e - ε * ∑ e ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach, W.w (Sym2.Mem.other ⋯)

Shows that the sum over the supported incidence set of loose (without s(loose,gain)) after Enhance transformation, equals the original sum minus ε times the sum over the attached incident set of loose.

noncomputable def Turan3.theBij {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) (h_supp : W.w loose > 0 ∧ W.w gain > 0) (e : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) : e ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach → ↥(supIncidenceFinset G W gain \ {s(loose, gain)})

Provides a bijection between the supported incidence edges at loose (without s(loose, gain)) and the supported incidence edges at gain (without s(loose, gain)).

Equations

• Turan3.theBij G W loose gain h_lt ε epos elt hc h_supp e h = ⟨s(gain, Sym2.Mem.other ⋯), ⋯⟩

theorem Turan3.the_bij_maps {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) (h_supp : W.w loose > 0 ∧ W.w gain > 0) (e : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) (he : e ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach) : theBij G W loose gain h_lt ε epos elt hc h_supp e he ∈ (supIncidenceFinset G W gain \ {s(loose, gain)}).attach

For every element e in the incidence set of loose (excluding s(loose, gain)), theBij maps e into the attached part of the incidence finset of gain.

theorem Turan3.the_bij_inj {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) (h_supp : W.w loose > 0 ∧ W.w gain > 0) (a₁ : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) (ha₁ : a₁ ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach) (a₂ : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) (ha₂ : a₂ ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach) : theBij G W loose gain h_lt ε epos elt hc h_supp a₁ ha₁ = theBij G W loose gain h_lt ε epos elt hc h_supp a₂ ha₂ → a₁ = a₂

Injetcitivy of theBij

theorem Turan3.the_bij_surj {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) (h_supp : W.w loose > 0 ∧ W.w gain > 0) (b : ↥(supIncidenceFinset G W gain \ {s(loose, gain)})) : b ∈ (supIncidenceFinset G W gain \ {s(loose, gain)}).attach → ∃ (a : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) (ha : a ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach), theBij G W loose gain h_lt ε epos elt hc h_supp a ha = b

Surjectivity of theBij

theorem Turan3.the_bij_same {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) (h_supp : W.w loose > 0 ∧ W.w gain > 0) (e : ↥(supIncidenceFinset G W loose \ {s(loose, gain)})) (he : e ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach) : W.w (Sym2.Mem.other ⋯) = (fun (e : ↥(supIncidenceFinset G W gain \ {s(loose, gain)})) => W.w (Sym2.Mem.other ⋯)) (theBij G W loose gain h_lt ε epos elt hc h_supp e he)

Shows that theBij preserves the "other" weight: for any edge from the supported incidence set of loose, the weight at the "other" vertex equals that in its image uneder the bijection

theorem Turan3.Enhance_sum_loose_gain_equal {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) (h_supp : W.w loose > 0 ∧ W.w gain > 0) : ∑ e ∈ (supIncidenceFinset G W loose \ {s(loose, gain)}).attach, W.w (Sym2.Mem.other ⋯) = ∑ e ∈ (supIncidenceFinset G W gain \ {s(loose, gain)}).attach, W.w (Sym2.Mem.other ⋯)

Uses theBij to show that the total sum of the weights, on the "other" vertices in the supported incidence set, is preserved when switching fom loose to gain

theorem Turan3.Enhance_sum_complement_unchanged {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) : ∑ e ∈ supEdgeFinset G W \ inciLooseGainFull G W loose gain ⋯, vp (Enhance G W loose gain h_lt ε epos elt).w e = ∑ e ∈ supEdgeFinset G W \ inciLooseGainFull G W loose gain ⋯, vp W.w e

Shows that, for the edges in the graph's support outside the set inciLooseGainFull, the total sum of edge values remains unchanged under Enhance.

theorem Turan3.Enhance_edge_gainloose_increase {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (h_neq : gain ≠ loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (_h_supp : W.w loose > 0 ∧ W.w gain > 0) : vp (Enhance G W loose gain h_lt ε epos elt).w s(loose, gain) > vp W.w s(loose, gain)

Proves that after Enhance, the value of the edge connecting loose and gain is strictly increased in comparisson to that under the original weight function.

theorem Turan3.Enhance_support_edges_same {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (h_supp : W.w loose > 0 ∧ W.w gain > 0) : supEdgeFinset G W = supEdgeFinset G (Enhance G W loose gain h_lt ε epos elt)

States that the subset of supported edges in the Graph, remains the same subset under Enhance.

theorem Turan3.Enhance_total_weight_stricinc {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] [DecidableRel G.Adj] (W : FunToMax G) (loose gain : α) (h_lt : W.w gain < W.w loose) (h_adj : G.Adj gain loose) (h_supp : W.w loose > 0 ∧ W.w gain > 0) (ε : NNReal) (epos : 0 < ε) (elt : ε < W.w loose - W.w gain) (hc : G.IsClique ↑{i : α | W.w i > 0}) : W.fw < (Enhance G W loose gain h_lt ε epos elt).fw

Combining previous lemmas, shows that the total edge weight increases or remains the same under Enhance.

Notes:

• sum_over_support : Assures that the total whole edge value of the Graph is the same as the total edge value of the edges in the support
• Enhance_support_edges_same : assures the supported subset of edges is the same under Enhance
• supported_edge_partition : Partitions the total edge contribution of the clique (and whole Graph) into:
  • inciLooseGainFull (edged incident to loose, edges incident to gain and {gain,loose})
  • inciLooseGainFull's complement

Now we show the change for each:

• with Enhance_sum_complement_unchanged we show that edges in the support but not in inciLooseGainFull remain with unchanged weights

• with Enhance_gain_sum, Enhance_loose_sum the lemma quantifies the gain from edges incident to gain and the loss from edges incident to loose, then with Enhance_sum_loose_gain_equal, since the support is a clique and there is a bijection between edged inci. to loose to edges incid. to gain, we show that the change is 0.

• with Enhance_edge_gainloose_increase we show that the only change comes from the edge gain-loose Therefore concluding that Enhance forms an strictly greater weight distribution

Section 3 : Equalizing weights on the clique

Given any weight function W whose support is a clique here we:

1. define

   • W.maxWeight and W.minWeight as the extremal vertex weights,
   • W.argmax and W.argmin as vertices attaining them;

2. prove inequalities relating these to the average weight 1 / |support|:

   • avg ≤ max, min ≤ avg,
   • strictly showing min < max ↔ avg < max and min < avg

3. set theEps := maxWeight − (1/|support|) > 0 (when min < max), and define another improved weight function Enhanced that moves this defined ε from argmax to argmin.

4. show Enhanced preserves total weight, support, and clique structure AND strictly increases the number of vertices with weight exactly 1/|support|

5. Shows UniformBetter has constant support

theorem Turan3.supp_size_pos {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : {i : α | W.w i > 0}.card ≠ 0

Helper lemma Shows that the support of a weight distribution is nonempty

@[reducible]

def Turan3.existsUniformClique {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (m : ℕ) : Prop

There exists an improved weight function with: weights that were 0 remain 0 (support included) support forms a clique an has exactly m vertices with 1/m weight each, and that the total edge weight does not decrease.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Turan3.maxUniformSupport {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) : ℕ

Using existsUniformClique, computes the largest number m for which there exists a weight function (with support contained in that of W) whose support forms a clique, has improved total edge weight, and has exactly m vertices with weight 1/k (support size).

Equations

• Turan3.maxUniformSupport G W = Nat.findGreatest (Turan3.existsUniformClique G W) {i : α | W.w i > 0}.card

theorem Turan3.exists_best_uniform {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) : (fun (m : ℕ) => ∃ (better : FunToMax G), (∀ (i : α), W.w i = 0 ↔ better.w i = 0) ∧ G.IsClique ↑{i : α | better.w i > 0} ∧ {i : α | better.w i = 1 / ↑{i : α | W.w i > 0}.card}.card = m ∧ W.fw ≤ better.fw) (maxUniformSupport G W)

Provides the specification for the Nat.findGreates in maxUniformSupport. Shows that for any weight function whose support forms a clique There is an improved weight function (with the specified support and uniform weights) with non decreaseing total edge weight value having exactly m vertices with 1/m support size

noncomputable def Turan3.UniformBetter {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) : FunToMax G

UniformBetter gives a new weight function (via exists_best_uniform) with the same support, clique structure, and improved edge weight. In later lemmas (UniformBetter_constant_support), we prove that this distribution is in fact uniform on the support.

Equations

• Turan3.UniformBetter G W hW = Classical.choose ⋯

theorem Turan3.UniformBetter_support_zero {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) (i : α) : W.w i = 0 ↔ (UniformBetter G W hW).w i = 0

zeros preserved : Ensures if a vertex is zero in W if and only if it is zero in UniformBetter W

theorem Turan3.UniformBetter_support_size {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) : {i : α | (UniformBetter G W hW).w i = 1 / ↑{i : α | W.w i > 0}.card}.card = maxUniformSupport G W

States that the number of vertices with weight 1/m (m being support size) in UniformBetter W is exactly m

theorem Turan3.UniformBetter_fw_ge {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) : W.fw ≤ (UniformBetter G W hW).fw

States that the total edge weight of UniformBetter is equal or greater than that of W

theorem Turan3.UniformBetter_clique {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) : G.IsClique ↑{i : α | (UniformBetter G W hW).w i > 0}

Confirms that the support of UniformBetter forms a clique in the Graph

theorem Turan3.FunToMax.supp_nonempty {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : {i : α | W.w i > 0}.Nonempty

Assures the support of a weight function is non empty

noncomputable def Turan3.FunToMax.maxWeight {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : NNReal

Defines the maximun weight value among vertices

Equations

• Turan3.FunToMax.maxWeight G W = (Finset.image W.w {i : α | W.w i > 0}).max' ⋯

theorem Turan3.FunToMax.argmax_pre {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : ∃ v ∈ {i : α | W.w i > 0}, W.w v = maxWeight G W

Specifies that there exists a vertex in the support attaining the maximum weight

noncomputable def Turan3.FunToMax.argmax {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : α

Chooses a vertex attaining the maximun weight (later used as the loose vertex)

Equations

• Turan3.FunToMax.argmax G W = Classical.choose ⋯

theorem Turan3.FunToMax.argmax_mem {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : argmax G W ∈ {i : α | W.w i > 0}

Proves that the chosen argmax vertex lies in the support (has positive weight)

theorem Turan3.FunToMax.argmax_weight {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : W.w (argmax G W) = maxWeight G W

Confirms that the weigth of the chosen argmax vertex equals the maximun weight.

noncomputable def Turan3.FunToMax.minWeight {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : NNReal

Defines the min. weight among vertices with positive weight

Equations

• Turan3.FunToMax.minWeight G W = (Finset.image W.w {i : α | W.w i > 0}).min' ⋯

theorem Turan3.FunToMax.argmin_pre {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : ∃ v ∈ {i : α | W.w i > 0}, W.w v = minWeight G W

Specifies that there exists a vertex in the support that attains the minimun weight.

noncomputable def Turan3.FunToMax.argmin {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : α

Chooses a vertex attaining the min weight (later used as the gain vertex)

Equations

• Turan3.FunToMax.argmin G W = Classical.choose ⋯

theorem Turan3.FunToMax.argmin_mem {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : argmin G W ∈ {i : α | W.w i > 0}

Proves that the chosen argmin vertex lies in the support.

theorem Turan3.FunToMax.argmin_weight {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : W.w (argmin G W) = minWeight G W

Confirms that the weight of the chosen argmin vertex equals the min. weight.

theorem Turan3.FunToMax.max_weight_max {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (v : α) : W.w v ≤ maxWeight G W

Shows that every vertex's weight is at most the maximun weight

theorem Turan3.FunToMax.min_weight_min {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (v : α) : v ∈ {i : α | W.w i > 0} → minWeight G W ≤ W.w v

Shows that every vertex's weight is at least the minimun weight

theorem Turan3.FunToMax.argmin_le_argmax {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : W.w (argmin G W) ≤ W.w (argmax G W)

Shows that the weight of the argmin vertex is at most that of the argmax vertex

theorem Turan3.FunToMax.min_weight_le_max_weight {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : minWeight G W ≤ maxWeight G W

Using the lemma above, assures that minimum weight is at most the maximum weight

theorem Turan3.FunToMax.sum_eq_sum_supp {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : ∑ v : α, W.w v = ∑ v : α with W.w v > 0, W.w v

Shows that the sum of weights over all vertices equals the sum of weights over the support.

theorem Turan3.FunToMax.sum_supp_eq_one {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : ∑ v : α with W.w v > 0, W.w v = 1

Proves that the sum of weights on the support is exactly 1

theorem Turan3.FunToMax.avg_le_max {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : maxWeight G W ≥ 1 / ↑{i : α | W.w i > 0}.card

States that the maximum weight is at least the average support weight (1/|support|)

theorem Turan3.FunToMax.min_le_avg {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : minWeight G W ≤ 1 / ↑{i : α | W.w i > 0}.card

marked: States that the minimun weight is at most the average support weight (1/|support|).

theorem Turan3.FunToMax.sum_supp_lt_max {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : minWeight G W < maxWeight G W) : ∑ v : α with W.w v > 0, W.w v < ↑{i : α | W.w i > 0}.card * maxWeight G W

Shows that if the minimun weight is strictily less that the maximum weight, then the sum of weights over the support is strictly less than the support size times the maximun weight

theorem Turan3.FunToMax.min_lt_sum_supp {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : minWeight G W < maxWeight G W) : ∑ v : α with W.w v > 0, W.w v > ↑{i : α | W.w i > 0}.card * minWeight G W

Shows that if the minimun weight is strictily less that the maximum weight, then the sum over the support is strictly greater than the support size times the minimum weight

theorem Turan3.FunToMax.avg_lt_max {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : minWeight G W < maxWeight G W) : maxWeight G W > 1 / ↑{i : α | W.w i > 0}.card

Shows that if the minimun weight is strictily less that the maximum weight, then the maximum weight is strictly greater than (1/|support|)

theorem Turan3.FunToMax.min_lt_avg {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : minWeight G W < maxWeight G W) : minWeight G W < 1 / ↑{i : α | W.w i > 0}.card

Shows that if the minimun weight is strictily less than the maximum weight, then the minimum weight is strictly less than (1/|support|)

theorem Turan3.FunToMax.min_eq_max {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : minWeight G W = maxWeight G W) (v : α) : v ∈ {i : α | W.w i > 0} → W.w v = 1 / ↑{i : α | W.w i > 0}.card

sanity check : Show that if the min. and max. weight are equal, then every vertex in the support hast weight 1/|support|.

noncomputable def Turan3.theEps {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) : NNReal

Defines ε (theEps) as the difference between maximum weight and the average weight 1/|support|

Equations

• Turan3.theEps G W = Turan3.FunToMax.maxWeight G W - 1 / ↑{i : α | W.w i > 0}.card

theorem Turan3.the_eps_pos {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : FunToMax.minWeight G W < FunToMax.maxWeight G W) : 0 < theEps G W

Shows that ε is positive if the min. and max. weight are distinct

theorem Turan3.the_eps_lt {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (h : FunToMax.minWeight G W < FunToMax.maxWeight G W) : theEps G W < W.w (FunToMax.argmax G W) - W.w (FunToMax.argmin G W)

Shows that ε is less than the difference between the weights between argmax argmin vertices

theorem Turan3.arg_help {α : Type u_1} (G : SimpleGraph α) [Fintype α] {W : FunToMax G} (h_con : W.w (FunToMax.argmin G W) < W.w (FunToMax.argmax G W)) : FunToMax.minWeight G W < FunToMax.maxWeight G W

Helper lemma: confirms if the weight at the argmin is less than that in argmax vertex, then the minimum weight is strictly less than the maximum weight

noncomputable def Turan3.Enhanced {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (h_con : W.w (FunToMax.argmin G W) < W.w (FunToMax.argmax G W)) : FunToMax G

Defines Enhanced weight function : transfering weight from the argmax vertex loose to the argmin vertex gain, using the previous in Section 2 defined function Enhance by the amount defined the_.

Equations

• Turan3.Enhanced G W h_con = Turan3.Enhance G W (Turan3.FunToMax.argmax G W) (Turan3.FunToMax.argmin G W) h_con (Turan3.theEps G W) ⋯ ⋯

theorem Turan3.Enhanced_unaffected {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (h_con : W.w (FunToMax.argmin G W) < W.w (FunToMax.argmax G W)) (v : α) : v ∈ {i : α | W.w i = 1 / ↑{i : α | W.w i > 0}.card} → (Enhanced G W h_con).w v = 1 / ↑{i : α | W.w i > 0}.card

Shows that under Enhanced every vertex that originally had weight 1/|support|, remains with the same weight

theorem Turan3.Enhanced_effect_argmax {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (h_con : W.w (FunToMax.argmin G W) < W.w (FunToMax.argmax G W)) : (Enhanced G W h_con).w (FunToMax.argmax G W) = 1 / ↑{i : α | W.w i > 0}.card

Proves that under the Enhanced weight function, the weight of the argmax vertex becomes 1/|support|

theorem Turan3.Enhanced_inc_uniform_count {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableEq α] (W : FunToMax G) (h_con : W.w (FunToMax.argmin G W) < W.w (FunToMax.argmax G W)) : have OneOverKSize := fun (X : FunToMax G) => {i : α | X.w i = 1 / ↑{i : α | W.w i > 0}.card}.card; OneOverKSize (Enhanced G W h_con) > OneOverKSize W

Shows that the number of vertices with weight equal to 1/|support| increases after Enhanced

theorem Turan3.UniformBetter_support_equiv {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) (i : α) : W.w i > 0 ↔ (UniformBetter G W hW).w i > 0

Helper lemma: Relates the support of the UniformBetter weight distribution to that of the original weight function W. That is having W, whose support forms a clique, UniformBetter support also forms a clique

theorem Turan3.clique_support_adjacent {α : Type u_1} (G : SimpleGraph α) [Fintype α] (W : FunToMax G) (hc : G.IsClique ↑{i : α | W.w i > 0}) (x y : α) (hx : W.w x > 0) (hy : W.w y > 0) (lol : x ≠ y) : G.Adj x y

Helper lemma: Shows that if two vertices in the support of W are distinct then they are adjacent (since they are in a clique). Proves that the support forms a clique

theorem Turan3.UniformBetter_constant_support {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) (v : α) : v ∈ {i : α | W.w i > 0} → (UniformBetter G W hW).w v = 1 / ↑{i : α | W.w i > 0}.card

Shows that under the UniformBetter distribution, every vertex in the support has an equal weight of 1/|support|.

theorem Turan3.UniformBetter_edges_value {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) (e : Sym2 α) : e ∈ supEdgeFinset G W → vp (UniformBetter G W hW).w e = (1 / ↑{i : α | W.w i > 0}.card) ^ 2

Shows that after UniformBetter every supported edge has value equal to the square of the uniform weight.

theorem Turan3.clique_size {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] (W : FunToMax G) (hW : G.IsClique ↑{i : α | W.w i > 0}) : have k := {i : α | W.w i > 0}.card; (supEdgeFinset G W).card = k * (k - 1) / 2

Computes the number of edges in a k clique

theorem Turan3.computation (k : ℕ) (hk : 0 < k) : ↑k * (↑k - 1) / 2 * (1 / ↑k) ^ 2 = 1 / 2 * (1 - 1 / ↑k)

Computation.

theorem Turan3.bound (k q : ℕ) (hk : 0 < k) (h : k ≤ q) : 1 / 2 * (1 - 1 / ↑k) ≤ 1 / 2 * (1 - 1 / ↑q)

Bound

theorem Turan3.bound_real (k p : ℕ) (hk : 0 < k) (hkp : k ≤ p) : 1 / 2 * (1 - 1 / ↑k) ≤ 1 / 2 * (1 - 1 / ↑p)

theorem Turan3.cast_help : Nat.cast = fun (x : ℕ) => ↑↑x

theorem Turan3.finale_bound {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] {p : ℕ} (h0 : p ≥ 2) (h1 : G.CliqueFree p) (W : FunToMax G) : W.fw ≤ (↑p - 1) * (↑p - 1 - 1) / 2 * (1 / (↑p - 1)) ^ 2

noncomputable def Turan3.UnivFun {α : Type u_1} (G : SimpleGraph α) [Fintype α] [Nonempty α] : FunToMax G

Defines the uniform vertex weight function that asisngs all vertices the same weight 1 /|V|

Equations

• Turan3.UnivFun G = { w := fun (x : α) => 1 / ↑Finset.univ.card, h_w := ⋯ }

theorem Turan3.UnivFun_weight {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] [Nonempty α] : (UnivFun G).fw = ↑G.edgeFinset.card * (1 / ↑Finset.univ.card) ^ 2

Computes the total edge weight of the un weight function. Shows that the total edge weight is equal to the number of edges times the square of the uniform vertex weight.

theorem Turan3.turans_of_nonempty {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] [Nonempty α] {p : ℕ} (h0 : p ≥ 2) (h1 : G.CliqueFree p) : ↑G.edgeFinset.card ≤ 1 / 2 * (1 - 1 / (↑p - 1)) * ↑Finset.univ.card ^ 2

Turán's theorem on a nonempty vertex set: for p ≥ 2 and G a p-clique-free graph, the desired upper bound on the number of edges holds.

theorem Turan3.turans {α : Type u_1} (G : SimpleGraph α) [Fintype α] [DecidableRel G.Adj] {p : ℕ} (h0 : p ≥ 2) (h1 : G.CliqueFree p) : ↑G.edgeFinset.card ≤ 1 / 2 * (1 - 1 / (↑p - 1)) * ↑Finset.univ.card ^ 2

The final theorem. Let p ≥ 2, and G be a p-Clique free Graph then we find the desired upper bound on the number of edges. The empty graph is covered: both sides vanish.