Documentation

Mathlib.Combinatorics.SimpleGraph.Density

Edge density #

This file defines the number and density of edges of a relation/graph.

Main declarations #

Between two finsets of vertices,

Density of a relation #

def Rel.interedges {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :
Finset (α × β)

Finset of edges of a relation between two finsets of vertices.

Equations
Instances For
    def Rel.edgeDensity {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :

    Edge density of a relation between two finsets of vertices.

    Equations
    Instances For
      theorem Rel.mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} {x : α × β} :
      x Rel.interedges r s t x.1 s x.2 t r x.1 x.2
      theorem Rel.mk_mem_interedges_iff {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} {a : α} {b : β} :
      (a, b) Rel.interedges r s t a s b t r a b
      @[simp]
      theorem Rel.interedges_empty_left {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] (t : Finset β) :
      theorem Rel.interedges_mono {α : Type u_4} {β : Type u_5} {r : αβProp} [(a : α) → DecidablePred (r a)] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (hs : s₂ s₁) (ht : t₂ t₁) :
      Rel.interedges r s₂ t₂ Rel.interedges r s₁ t₁
      theorem Rel.card_interedges_add_card_interedges_compl {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :
      (Rel.interedges r s t).card + (Rel.interedges (fun (x : α) (y : β) => ¬r x y) s t).card = s.card * t.card
      theorem Rel.interedges_disjoint_left {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : Finset α} {s' : Finset α} (hs : Disjoint s s') (t : Finset β) :
      theorem Rel.interedges_disjoint_right {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) {t : Finset β} {t' : Finset β} (ht : Disjoint t t') :
      theorem Rel.interedges_eq_biUnion {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] :
      Rel.interedges r s t = s.biUnion fun (x : α) => Finset.map { toFun := fun (x_1 : β) => (x, x_1), inj' := } (Finset.filter (r x) t)
      theorem Rel.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] [DecidableEq α] [DecidableEq β] (s : Finset ι) (t : Finset β) (f : ιFinset α) :
      Rel.interedges r (s.biUnion f) t = s.biUnion fun (a : ι) => Rel.interedges r (f a) t
      theorem Rel.interedges_biUnion_right {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] [DecidableEq α] [DecidableEq β] (s : Finset α) (t : Finset ι) (f : ιFinset β) :
      Rel.interedges r s (t.biUnion f) = t.biUnion fun (b : ι) => Rel.interedges r s (f b)
      theorem Rel.interedges_biUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] [DecidableEq α] [DecidableEq β] (s : Finset ι) (t : Finset κ) (f : ιFinset α) (g : κFinset β) :
      Rel.interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) => Rel.interedges r (f ab.1) (g ab.2)
      theorem Rel.card_interedges_le_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :
      (Rel.interedges r s t).card s.card * t.card
      theorem Rel.edgeDensity_nonneg {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :
      theorem Rel.edgeDensity_le_one {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :
      theorem Rel.edgeDensity_add_edgeDensity_compl {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} (hs : s.Nonempty) (ht : t.Nonempty) :
      Rel.edgeDensity r s t + Rel.edgeDensity (fun (x : α) (y : β) => ¬r x y) s t = 1
      @[simp]
      theorem Rel.edgeDensity_empty_left {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (t : Finset β) :
      @[simp]
      theorem Rel.edgeDensity_empty_right {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) :
      theorem Rel.card_interedges_finpartition_left {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : Finset α} [DecidableEq α] (P : Finpartition s) (t : Finset β) :
      (Rel.interedges r s t).card = aP.parts, (Rel.interedges r a t).card
      theorem Rel.card_interedges_finpartition_right {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {t : Finset β} [DecidableEq β] (s : Finset α) (P : Finpartition t) :
      (Rel.interedges r s t).card = bP.parts, (Rel.interedges r s b).card
      theorem Rel.card_interedges_finpartition {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] (P : Finpartition s) (Q : Finpartition t) :
      (Rel.interedges r s t).card = abP.parts ×ˢ Q.parts, (Rel.interedges r ab.1 ab.2).card
      theorem Rel.mul_edgeDensity_le_edgeDensity {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
      s₂.card / s₁.card * (t₂.card / t₁.card) * Rel.edgeDensity r s₂ t₂ Rel.edgeDensity r s₁ t₁
      theorem Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
      Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁ 1 - s₂.card / s₁.card * (t₂.card / t₁.card)
      theorem Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} (hs : s₂ s₁) (ht : t₂ t₁) (hs₂ : s₂.Nonempty) (ht₂ : t₂.Nonempty) :
      |Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁| 1 - s₂.card / s₁.card * (t₂.card / t₁.card)
      theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [LinearOrderedField 𝕜] (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} {δ : 𝕜} (hs : s₂ s₁) (ht : t₂ t₁) (hδ₀ : 0 δ) (hδ₁ : δ < 1) (hs₂ : (1 - δ) * s₁.card s₂.card) (ht₂ : (1 - δ) * t₁.card t₂.card) :
      |(Rel.edgeDensity r s₂ t₂) - (Rel.edgeDensity r s₁ t₁)| 2 * δ - δ ^ 2
      theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [LinearOrderedField 𝕜] (r : αβProp) [(a : α) → DecidablePred (r a)] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset β} {t₂ : Finset β} {δ : 𝕜} (hs : s₂ s₁) (ht : t₂ t₁) (hδ : 0 δ) (hscard : (1 - δ) * s₁.card s₂.card) (htcard : (1 - δ) * t₁.card t₂.card) :
      |(Rel.edgeDensity r s₂ t₂) - (Rel.edgeDensity r s₁ t₁)| 2 * δ

      If s₂ ⊆ s₁, t₂ ⊆ t₁ and they take up all but a δ-proportion, then the difference in edge densities is at most 2 * δ.

      @[simp]
      theorem Rel.swap_mem_interedges_iff {α : Type u_4} {r : ααProp} [DecidableRel r] {s : Finset α} {t : Finset α} (hr : Symmetric r) {x : α × α} :
      x.swap Rel.interedges r s t x Rel.interedges r t s
      theorem Rel.mk_mem_interedges_comm {α : Type u_4} {r : ααProp} [DecidableRel r] {s : Finset α} {t : Finset α} {a : α} {b : α} (hr : Symmetric r) :
      (a, b) Rel.interedges r s t (b, a) Rel.interedges r t s
      theorem Rel.card_interedges_comm {α : Type u_4} {r : ααProp} [DecidableRel r] (hr : Symmetric r) (s : Finset α) (t : Finset α) :
      (Rel.interedges r s t).card = (Rel.interedges r t s).card
      theorem Rel.edgeDensity_comm {α : Type u_4} {r : ααProp} [DecidableRel r] (hr : Symmetric r) (s : Finset α) (t : Finset α) :

      Density of a graph #

      def SimpleGraph.interedges {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
      Finset (α × α)

      Finset of edges of a relation between two finsets of vertices.

      Equations
      Instances For
        def SimpleGraph.edgeDensity {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] :
        Finset αFinset α

        Density of edges of a graph between two finsets of vertices.

        Equations
        Instances For
          theorem SimpleGraph.interedges_def {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          G.interedges s t = Finset.filter (fun (e : α × α) => G.Adj e.1 e.2) (s ×ˢ t)
          theorem SimpleGraph.edgeDensity_def {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          G.edgeDensity s t = (G.interedges s t).card / (s.card * t.card)
          theorem SimpleGraph.card_interedges_div_card {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          (G.interedges s t).card / (s.card * t.card) = G.edgeDensity s t
          theorem SimpleGraph.mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {x : α × α} :
          x G.interedges s t x.1 s x.2 t G.Adj x.1 x.2
          theorem SimpleGraph.mk_mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {a : α} {b : α} :
          (a, b) G.interedges s t a s b t G.Adj a b
          @[simp]
          theorem SimpleGraph.interedges_empty_left {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (t : Finset α) :
          G.interedges t =
          theorem SimpleGraph.interedges_mono {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
          s₂ s₁t₂ t₁G.interedges s₂ t₂ G.interedges s₁ t₁
          theorem SimpleGraph.interedges_disjoint_left {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s₁ : Finset α} {s₂ : Finset α} (hs : Disjoint s₁ s₂) (t : Finset α) :
          Disjoint (G.interedges s₁ t) (G.interedges s₂ t)
          theorem SimpleGraph.interedges_disjoint_right {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {t₁ : Finset α} {t₂ : Finset α} (s : Finset α) (ht : Disjoint t₁ t₂) :
          Disjoint (G.interedges s t₁) (G.interedges s t₂)
          theorem SimpleGraph.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset ι) (t : Finset α) (f : ιFinset α) :
          G.interedges (s.biUnion f) t = s.biUnion fun (a : ι) => G.interedges (f a) t
          theorem SimpleGraph.interedges_biUnion_right {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset α) (t : Finset ι) (f : ιFinset α) :
          G.interedges s (t.biUnion f) = t.biUnion fun (b : ι) => G.interedges s (f b)
          theorem SimpleGraph.interedges_biUnion {ι : Type u_2} {κ : Type u_3} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset ι) (t : Finset κ) (f : ιFinset α) (g : κFinset α) :
          G.interedges (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun (ab : ι × κ) => G.interedges (f ab.1) (g ab.2)
          theorem SimpleGraph.card_interedges_add_card_interedges_compl {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} [DecidableEq α] (h : Disjoint s t) :
          (G.interedges s t).card + (G.interedges s t).card = s.card * t.card
          theorem SimpleGraph.edgeDensity_add_edgeDensity_compl {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} [DecidableEq α] (hs : s.Nonempty) (ht : t.Nonempty) (h : Disjoint s t) :
          G.edgeDensity s t + G.edgeDensity s t = 1
          theorem SimpleGraph.card_interedges_le_mul {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          (G.interedges s t).card s.card * t.card
          theorem SimpleGraph.edgeDensity_nonneg {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          0 G.edgeDensity s t
          theorem SimpleGraph.edgeDensity_le_one {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          G.edgeDensity s t 1
          @[simp]
          theorem SimpleGraph.edgeDensity_empty_left {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (t : Finset α) :
          G.edgeDensity t = 0
          @[simp]
          theorem SimpleGraph.edgeDensity_empty_right {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) :
          G.edgeDensity s = 0
          @[simp]
          theorem SimpleGraph.swap_mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {x : α × α} :
          x.swap G.interedges s t x G.interedges t s
          theorem SimpleGraph.mk_mem_interedges_comm {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {a : α} {b : α} :
          (a, b) G.interedges s t (b, a) G.interedges t s
          theorem SimpleGraph.edgeDensity_comm {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          G.edgeDensity s t = G.edgeDensity t s