Documentation

TauCeti.Combinatorics.Regularity.Graph.StrongRegularity

Strong graph regularity #

A strong regularity witness for a finite graph G is a pair of equipartitions Q ≤ P (so Q refines P) such that the coarse partition P is ε-uniform, the fine partition Q is uniform at the scale F #P.parts prescribed by a positive schedule F : ℕ → ℝ, and passing from P to Q raises the size-weighted energy SimpleGraph.weightedEnergy by at most ε. Choosing F sufficiently small makes the fine partition as regular as a counting argument requires. The energy gap controls how far the fine densities deviate from the coarse ones (SimpleGraph.weightedDensityDeviation_abs_le), so counts computed on the fine partition transfer to the coarse partition, where the number of parts is small. This is the input of the induced counting lemma for strong regularity.

The existence theorem iterates SimpleGraph.exists_regular_exact_refining_equipartition. Starting from an ε-uniform equipartition P given by SimpleGraph.exists_regular_almostRefines_le_card, refine it exactly to an equipartition Q that is uniform at min ε (F #P.parts). If the energy rises by at most ε, then (P, Q) is a witness. Otherwise replace P by Q and repeat. The weighted energy lies in [0, 1] and every unsuccessful round raises it by more than ε, so the iteration stops within ⌊1 / ε⌋₊ + 1 rounds. Since every round refines exactly, the coarse partition keeps almost refining the starting partition, and its number of parts never drops below the requested minimum.

A strong regularity witness predicts every labelled induced three-vertex pattern from the densities of its coarse partition (SimpleGraph.StrongRegular.inducedGraphCount3_estimate). With τ = F #P.parts, the error is at most (15 τ + 3 √ε) (card α) ^ 3 + 6 m (card α) ^ 2 when every coarse part has at most m vertices. The fine partition counts the copies with vertices in three distinct fine parts up to 15 τ (card α) ^ 3, by the counting lemma for a uniform equipartition. Passing through the stepped predictions of the fine and coarse partitions, which include the assignments with a repeated part, the energy gap costs 3 √ε (card α) ^ 3 (SimpleGraph.abs_steppedInducedGraphCount3_sub_le). The copies and assignments meeting some part twice cost 3 m (card α) ^ 2 once for each partition.

The number of parts is bounded independently of the graph. As the schedule F is arbitrary, the bound for one round is a maximum over all smaller partition sizes (TauCeti.strongRegularityStepBound), which makes it monotone, and the final bound TauCeti.strongGraphRegularityBound iterates it.

Main declarations #

References #

source
noncomputable def TauCeti.strongRegularityStepBound (ε : ℝ) (F : ℕ → ℝ) (m : ℕ) :
ℕ

The complexity bound for one round of strong regularity, from a partition with at most m parts: the largest of the bounds nestedRefinementBound (min ε (F j)) j for exactly refining regularity, over all j ≤ m. Taking the maximum makes the bound monotone in m for every schedule F.

Instances For
    source
    theorem TauCeti.strongRegularityStepBound_def (ε : ℝ) (F : ℕ → ℝ) (m : ℕ) :
    strongRegularityStepBound ε F m = (partialSups fun (j : ℕ) => nestedRefinementBound (min ε (F j)) j) m

    The bound for one round is the partial supremum of the exact-refinement bounds.

    source
    theorem TauCeti.strongRegularityStepBound_eq_sup_range (ε : ℝ) (F : ℕ → ℝ) (m : ℕ) :
    strongRegularityStepBound ε F m = (Finset.range (m + 1)).sup fun (j : ℕ) => nestedRefinementBound (min ε (F j)) j

    The bound for one round is the largest exact-refinement bound over smaller sizes.

    source
    theorem TauCeti.nestedRefinementBound_le_strongRegularityStepBound {ε : ℝ} {F : ℕ → ℝ} {j m : ℕ} (h : j ≤ m) :
    nestedRefinementBound (min ε (F j)) j ≤ strongRegularityStepBound ε F m

    The bound for one round dominates the bound for exactly refining regularity from any partition with at most m parts.

    source
    theorem TauCeti.le_strongRegularityStepBound {ε : ℝ} {F : ℕ → ℝ} (m : ℕ) :
    m ≤ strongRegularityStepBound ε F m

    One round never needs fewer parts than it starts from.

    source
    theorem TauCeti.strongRegularityStepBound_mono {ε : ℝ} {F : ℕ → ℝ} :
    Monotone (strongRegularityStepBound ε F)

    The bound for one round is monotone in the starting number of parts.

    source
    noncomputable def TauCeti.strongGraphRegularityBound (ε : ℝ) (F : ℕ → ℝ) (l₀ : ℕ) :
    ℕ

    The complexity bound for strong graph regularity, in terms of the starting complexity l₀: ⌊1 / ε⌋₊ + 1 rounds of strongRegularityStepBound ε F, started from the bound nestedRefinementBound ε (max l₀ ⌈2 * l₀ / ε⌉₊) for a uniform equipartition with at least l₀ parts almost refining a partition with at most l₀ parts. It does not depend on the graph.

    Instances For
      source
      theorem TauCeti.strongGraphRegularityBound_def (ε : ℝ) (F : ℕ → ℝ) (l₀ : ℕ) :
      strongGraphRegularityBound ε F l₀ = (strongRegularityStepBound ε F)^[⌊1 / ε⌋₊ + 1] (nestedRefinementBound ε (max l₀ ⌈2 * ↑l₀ / ε⌉₊))

      The complexity bound for strong regularity iterates the bound for one round.

      source
      theorem TauCeti.le_strongGraphRegularityBound {ε : ℝ} {F : ℕ → ℝ} (l₀ : ℕ) :
      l₀ ≤ strongGraphRegularityBound ε F l₀

      The complexity bound for strong graph regularity is at least the starting complexity.

      source
      structure SimpleGraph.StrongRegular {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (P Q : Finpartition Finset.univ) (ε : ℝ) (F : ℕ → ℝ) (l₀ : ℕ) :
      Prop

      A strong regularity witness for G: equipartitions Q ≤ P (Q refines P) with P ε-uniform, Q uniform at the scale F #P.parts, a weighted-energy gap of at most ε between them, and at most strongGraphRegularityBound ε F l₀ fine parts, a bound independent of the graph.

      Instances For
        source
        theorem SimpleGraph.exists_strong_regular {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (P₀ : Finpartition Finset.univ) (hP₀ : P₀.IsEquipartition) {l : ℕ} (hl : l ≤ Fintype.card α) {ε : ℝ} (hε : 0 < ε) {F : ℕ → ℝ} (hF : ∀ (n : ℕ), 0 < F n) :
        ∃ (P : Finpartition Finset.univ) (Q : Finpartition Finset.univ), G.StrongRegular P Q ε F (max l P₀.parts.card) ∧ P.AlmostRefines P₀ ε ∧ l ≤ P.parts.card

        Strong graph regularity. Let ε > 0 and let F : ℕ → ℝ be a positive schedule. Every equipartition P₀ of a finite graph G is almost refined, up to ε, by the coarse partition P of a strong regularity witness (P, Q), where P has at least l parts for any requested l ≤ card α, and Q has at most strongGraphRegularityBound ε F (max l #P₀.parts) parts.

        source
        theorem SimpleGraph.StrongRegular.inducedGraphCount3_estimate {α : Type u_1} [Fintype α] [DecidableEq α] {G : SimpleGraph α} [DecidableRel G.Adj] (J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] {P Q : Finpartition Finset.univ} {ε : ℝ} {F : ℕ → ℝ} {l₀ : ℕ} (h : G.StrongRegular P Q ε F l₀) (hF : 0 < F P.parts.card) {m : ℕ} (hm : ∀ A ∈ P.parts, A.card ≤ m) :
        |↑(J.inducedGraphCount3 G) - J.coarseInducedGraphEstimate G P| ≤ (15 * F P.parts.card + 3 * √ε) * ↑(Fintype.card α) ^ 3 + 6 * ↑m * ↑(Fintype.card α) ^ 2

        Induced counting lemma for strong regularity. Let (P, Q) be a strong regularity witness for G with τ = F #P.parts > 0, and suppose every part of P has at most m vertices. Then for every graph J on Fin 3, the number of labelled induced copies of J in G differs from the coarse prediction J.coarseInducedGraphEstimate G P by at most (15 τ + 3 √ε) (card α) ^ 3 + 6 m (card α) ^ 2. Only the refinement, the equitability and uniformity of Q, and the energy gap are used.