le_sum_distinctPairs_edgeDensity_sq

English

When passing from P to its increment, the energy increases by at least ε^5/4.

Русский

Переходя от P к его приращению, энергия увеличивается не менее чем на ε^5/4.

LaTeX

$$$E(P,G) + \\dfrac{ε^5}{4} \\le E(\\text{increment } hP G ε, G)$$$

Lean4

theorem le_sum_distinctPairs_edgeDensity_sq (x : { i // i ∈ P.parts.offDiag }) (hε₁ : ε ≤ 1)
    (hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPε : ↑100 ≤ ↑4 ^ #P.parts * ε ^ 5) :
    (G.edgeDensity x.1.1 x.1.2 : ℝ) ^ 2 + ((if G.IsUniform ε x.1.1 x.1.2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤
      (∑ i ∈ distinctPairs hP G ε x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ #P.parts :=
  by
  rw [distinctPairs, ← add_sub_assoc, add_sub_right_comm]
  split_ifs with h
  · rw [add_zero]
    exact edgeDensity_chunk_uniform hPα hPε _ _
  · exact edgeDensity_chunk_not_uniform hPα hPε hε₁ (mem_offDiag.1 x.2).2.2 h

Похожие утверждения