some extremal graph theory (max edges until triangles)

Stream: graph theory

[Kyle Miller]

It seemed like we were ready to prove theorem I.2 in Bollobas's "Modern Graph Theory" that every graph with n vertices and more than n^2/4 vertices has a triangle, so here's #13758.

There's a sorry for a consequence of Cauchy-Schwarz I couldn't find in mathlib, but other than that it was fairly straightforward once I thought of organizing the argument using a double sum over vertices and edges in the graph.

It also has an example showing the bound the theorem gives is tight, but there's still a sorry there for the number of edges in a bipartite graph.

[Kyle Miller]

If anyone wants to help finish this up, feel free!

[Kyle Miller]

Hopefully this is orthogonal to what you're doing with triangles, @Yaël Dillies and @Bhavik Mehta.

[Yaël Dillies]

This looks very similar to what we have, in particular triangle_removal_2, but I'm not sure how to connect both statements.

[Yaël Dillies]

@Mantas Baksys has your cauchy on a branch, using the fact that monovary f f.

[Mauricio Collares]

I want to help! Can I get commit access to non-master branches? My GitHub username is collares.

[Mauricio Collares]

I won't push directly to the branch at first, it just feels like a convenient time to ask.

[Riccardo Brasca]

Invitation sent!

[Yaël Dillies]

Bhavik claims it's totally unrelated.

[Bhavik Mehta]

Kyle Miller said:

It seemed like we were ready to prove theorem I.2 in Bollobas's "Modern Graph Theory" that every graph with n vertices and more than n^2/4 vertices has a triangle, so here's #13758.

There's a sorry for a consequence of Cauchy-Schwarz I couldn't find in mathlib, but other than that it was fairly straightforward once I thought of organizing the argument using a double sum over vertices and edges in the graph.

It also has an example showing the bound the theorem gives is tight, but there's still a sorry there for the number of edges in a bipartite graph.

The result is unrelated (though also very cool!) but we also needed a variant of Cauchy-Schwarz just like that one!

[Eric Rodriguez]

both of the division lemmas have almost the same proof:

  rw [nat.add_div two_pos, n.mul_div_cancel_left two_pos],
  norm_num,

[Yaël Dillies]

It's very nice to see our work on cliques being used already!

[Eric Rodriguez]

wow, making a function (complete_bipartite_graph V W).edge_set to V × W with nice definitional properties is borderline impossible

[Vincent Beffara]

Working with darts is always more pleasant in my experience

[Mauricio Collares]

As far as I understand it, three of the four sorries have already been proven in Zulip (either in this thread or in the Cauchy-Schwarz one), so I am trying to prove bipartite_num_edges now

[Eric Rodriguez]

I was also trying that, Mauricio, how are you goijg about it? I wonder if darts are the easier way...

[Eric Rodriguez]

Although there doesn't seem to be a dart set, so you'd have to implement that and related lemmata...not too hard but still

[Mauricio Collares]

Ah, sorry! I didn't want to duplicate work, and I haven't really started, so feel free to keep working on it :) I will take a look at the current clique API to see if doing Turán is feasible. I'd really like to eventually help to get a proof of Turán plus some sort of stability (as in the Szemerédi-less part of https://arxiv.org/abs/1501.03129 for example) into Mathlib.

[Yaël Dillies]

The clique API is a week old so I suspect not :grinning: but feel free to add to it!

[Yaël Dillies]

Note that you can also try the Szemerédi-full part of the paper you just mentioned, because we have Szemerédi's regularity lemma on branch#szemeredi

[Mauricio Collares]

I hope to do the Szemerédi-full part eventually too, but usually with these proofs you prove things for cliques without Szemerédi, then do it for general H by applying Szemerédi to get a reduced graph (a graph with one vertex for each part in the Szemerédi partition of the original graph, and an edge for every "sufficiently dense" and regular pair), using the clique version (for K_{\chi(H)}) in the reduced graph and pulling the result back from the reduced graph.

[Mauricio Collares]

But I will definitely try to do the Szemerédi application when the clique version is ready!

[Mauricio Collares]

@Eric Rodriguez It would probably take me a couple of days to fight lean, but to answer your earlier question I think I'd start with using sum_degrees_eq_twice_card_edges somehow.

[Eric Rodriguez]

The three non-Cauchy-Schwartz sorrys are solved in branch#ericrbg/triangle_free

[Eric Rodriguez]

the equiv complete_bipartite_graph V W).edge_set to V × W is abhorrent

[Eric Rodriguez]

the last proof I did should probably be turned into a calc block

[Vincent Beffara]

Eric Rodriguez said:

the equiv complete_bipartite_graph V W).edge_set to V × W is abhorrent

Why do you need it though? Only in bipartite_num_edges? Because there a simpler proof using docs#simple_graph.dart_card_eq_sum_degrees and docs#simple_graph.dart_card_eq_twice_card_edges seems to be doable.

[Eric Rodriguez]

I mean, it's the right thing to have mathematically regardless. It's just a shame it's so type theoretically awful to write

[Kyle Miller]

Thanks everyone for the help -- #13758 is now sorry-free! (@Eric Rodriguez I merged your branch, so feel free to delete yours if you want.)

[Eric Rodriguez]

awesome, thanks for finding a nice golf!

[Kyle Miller]

I wonder if ∑ v, G.degree v ^ 2 ≤ G.edge_finset.card * fintype.card V when G is triangle-free has an algebraic proof. If these are dimensions of vector spaces, then maybe some algebra structure for the tensor product of the edge space and the vertex space contains a direct sum of matrix algebras, one per vertex, each on a G.degree v-dimensional vector space.

[Vincent Beffara]

Eric Rodriguez said:

I mean, it's the right thing to have mathematically regardless. It's just a shame it's so type theoretically awful to write

Agreed. This equiv on darts is a bit nicer IMO:

def Φ₁ : (complete_bipartite_graph U V).dart → (U × V) ⊕ (V × U) :=
begin
  rintro ⟨⟨x | x, y | y⟩, h⟩; { simp at h, contradiction } <|>
    { exact sum.inl (x, y) } <|> { exact sum.inr (x, y) }
end

def Φ₂ : (U × V) ⊕ (V × U) → (complete_bipartite_graph U V).dart
| (sum.inl (x, y)) := ⟨⟨sum.inl x, sum.inr y⟩, by simp⟩
| (sum.inr (x, y)) := ⟨⟨sum.inr x, sum.inl y⟩, by simp⟩

def toto : (complete_bipartite_graph U V).dart ≃ (U × V) ⊕ (V × U) :=
{
  to_fun := Φ₁,
  inv_fun := Φ₂,
  left_inv := by { rintro ⟨⟨x | x, y | y⟩, h⟩; simp [Φ₁, Φ₂] at h ⊢; cases h },
  right_inv := λ x, by { cases x; cases x; simp [Φ₁, Φ₂] }
}

If edge_set were a quotient of dart as opposed to a set in sym2, one could then use quotient.lift ...