Theorems · Theorem · combinatorics

SzemerediRegularity.edgeDensity_chunk_uniform

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ∀ (hU : U ∈ P.parts) (hV : V ∈ P.parts),
        ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
          (∑ ab ∈ (SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts,
              ↑(G.edgeDensity ab.1 ab.2) ^ 2) /
            16 ^ P.parts.card

Lower bound on the edge densities between parts of SzemerediRegularity.increment. This is the blanket lower bound used the uniform parts.

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqDecidableRelNonempty