Theorems · Theorem · combinatorics

SzemerediRegularity.add_div_le_sum_sq_div_card

∀ {ι : Type u_2} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s t : Finset ι}
  {x : 𝕜},
  s ⊆ t →
    ∀ (f : ι → 𝕜) (d : 𝕜),
      0 ≤ x →
        x ≤ |(∑ i ∈ s, f i) / ↑s.card - (∑ i ∈ t, f i) / ↑t.card| →
          d ≤ ((∑ i ∈ t, f i) / ↑t.card) ^ 2 → d + ↑s.card / ↑t.card * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑t.card

Defined in

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRing