# Zulip Chat Archive

## Stream: graph theory

### Topic: some extremal graph theory (max edges until triangles)

#### Kyle Miller (Apr 28 2022 at 02:22):

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 (Apr 28 2022 at 02:22):

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

#### Kyle Miller (Apr 28 2022 at 02:23):

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

#### Yaël Dillies (Apr 28 2022 at 07:44):

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 (Apr 28 2022 at 07:45):

@Mantas Baksys has your `cauchy`

on a branch, using the fact that `monovary f f`

.

#### Mauricio Collares (Apr 28 2022 at 08:05):

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

.

#### Mauricio Collares (Apr 28 2022 at 08:05):

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

#### Riccardo Brasca (Apr 28 2022 at 08:41):

Invitation sent!

#### Yaël Dillies (Apr 28 2022 at 09:03):

Bhavik claims it's totally unrelated.

#### Bhavik Mehta (Apr 28 2022 at 09:38):

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 (Apr 28 2022 at 09:55):

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 (Apr 28 2022 at 10:39):

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

#### Eric Rodriguez (Apr 28 2022 at 11:01):

wow, making a function `(complete_bipartite_graph V W).edge_set`

to `V × W`

with nice definitional properties is borderline impossible

#### Vincent Beffara (Apr 28 2022 at 12:06):

Working with darts is always more pleasant in my experience

#### Mauricio Collares (Apr 28 2022 at 13:33):

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 (Apr 28 2022 at 13:37):

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

#### Eric Rodriguez (Apr 28 2022 at 13:39):

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 (Apr 28 2022 at 13:43):

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 (Apr 28 2022 at 13:43):

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

#### Yaël Dillies (Apr 28 2022 at 13:45):

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 (Apr 28 2022 at 13:47):

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 (Apr 28 2022 at 13:48):

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

#### Mauricio Collares (Apr 28 2022 at 14:17):

@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 (Apr 28 2022 at 14:43):

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

#### Eric Rodriguez (Apr 28 2022 at 14:43):

the equiv `complete_bipartite_graph V W).edge_set`

to `V × W`

is abhorrent

#### Eric Rodriguez (Apr 28 2022 at 14:44):

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

block

#### Vincent Beffara (Apr 28 2022 at 15:57):

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 (Apr 28 2022 at 16:17):

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 (Apr 28 2022 at 17:38):

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 (Apr 28 2022 at 17:44):

awesome, thanks for finding a nice golf!

#### Kyle Miller (Apr 28 2022 at 18:16):

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 (Apr 28 2022 at 22:05):

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`

...

Last updated: Aug 03 2023 at 10:10 UTC