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.

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.

    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.fst s x.snd t r x.fst x.snd
      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 β) :
      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_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 α) :
      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 β) :
      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 (Finset.biUnion s f) (Finset.biUnion t g) = Finset.biUnion (s ×ˢ t) fun ab => Rel.interedges r (f ab.fst) (g ab.snd)
      theorem Rel.card_interedges_le_mul {α : Type u_4} {β : Type u_5} (r : αβProp) [(a : α) → DecidablePred (r a)] (s : Finset α) (t : Finset β) :
      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 : Finset.Nonempty s) (ht : Finset.Nonempty t) :
      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 β) :
      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) :
      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) :
      Finset.card (Rel.interedges r s t) = Finset.sum (P.parts ×ˢ Q.parts) fun ab => Finset.card (Rel.interedges r ab.fst ab.snd)
      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₂ : Finset.Nonempty s₂) (ht₂ : Finset.Nonempty t₂) :
      ↑(Finset.card s₂) / ↑(Finset.card s₁) * (↑(Finset.card t₂) / ↑(Finset.card t₁)) * 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₂ : Finset.Nonempty s₂) (ht₂ : Finset.Nonempty t₂) :
      Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁ 1 - ↑(Finset.card s₂) / ↑(Finset.card s₁) * (↑(Finset.card t₂) / ↑(Finset.card t₁))
      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₂ : Finset.Nonempty s₂) (ht₂ : Finset.Nonempty t₂) :
      |Rel.edgeDensity r s₂ t₂ - Rel.edgeDensity r s₁ t₁| 1 - ↑(Finset.card s₂) / ↑(Finset.card s₁) * (↑(Finset.card t₂) / ↑(Finset.card t₁))
      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 - δ) * ↑(Finset.card s₁) ↑(Finset.card s₂)) (ht₂ : (1 - δ) * ↑(Finset.card t₁) ↑(Finset.card t₂)) :
      |↑(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 - δ) * ↑(Finset.card s₁) ↑(Finset.card s₂)) (htcard : (1 - δ) * ↑(Finset.card t₁) ↑(Finset.card t₂)) :
      |↑(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 : α × α} :
      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 α) :
      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.

      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.

        Instances For
          theorem SimpleGraph.interedges_def {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          SimpleGraph.interedges G s t = Finset.filter (fun e => SimpleGraph.Adj G e.fst e.snd) (s ×ˢ t)
          theorem SimpleGraph.edgeDensity_def {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          @[simp]
          theorem SimpleGraph.mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {x : α × α} :
          x SimpleGraph.interedges G s t x.fst s x.snd t SimpleGraph.Adj G x.fst x.snd
          theorem SimpleGraph.mk_mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {a : α} {b : α} :
          theorem SimpleGraph.interedges_mono {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s₁ : Finset α} {s₂ : Finset α} {t₁ : Finset α} {t₂ : Finset α} :
          s₂ s₁t₂ t₁SimpleGraph.interedges G s₂ t₂ SimpleGraph.interedges G 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 α) :
          theorem SimpleGraph.interedges_disjoint_right {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {t₁ : Finset α} {t₂ : Finset α} (s : Finset α) (ht : Disjoint t₁ t₂) :
          theorem SimpleGraph.interedges_biUnion_left {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset ι) (t : Finset α) (f : ιFinset α) :
          theorem SimpleGraph.interedges_biUnion_right {ι : Type u_2} {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] [DecidableEq α] (s : Finset α) (t : Finset ι) (f : ιFinset α) :
          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 α) :
          theorem SimpleGraph.edgeDensity_nonneg {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          theorem SimpleGraph.edgeDensity_le_one {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] (s : Finset α) (t : Finset α) :
          @[simp]
          @[simp]
          theorem SimpleGraph.swap_mem_interedges_iff {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {x : α × α} :
          theorem SimpleGraph.mk_mem_interedges_comm {α : Type u_4} (G : SimpleGraph α) [DecidableRel G.Adj] {s : Finset α} {t : Finset α} {a : α} {b : α} :