Mathlib.Combinatorics.SimpleGraph.Density._auxLemma.1
theorem Mathlib.Combinatorics.SimpleGraph.Density._auxLemma.1 :
∀ {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [inst : (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)
The theorem, named `_auxLemma.1` in the `Mathlib.Combinatorics.SimpleGraph.Density` namespace, states that for any types `α` and `β`, any relation `r` between elements of `α` and `β`, and any finsets `s` of α and `t` of β, a pair `x` of type `α × β` is in the finset `Rel.interedges r s t` if and only if the first element of `x` is in `s`, the second element of `x` is in `t`, and the relation `r` holds between the two elements of `x`. This is under the condition that `r` is a decidable predicate.
More concisely: For any decidable relation `r` between types `α` and `β`, and finsets `s` of `α` and `t` of `β`, an element `(x, y)` of `α × β` is in the intersection of the relation's edges and the cartesian product of `s` and `t` if and only if the first component `x` is in `s`, the second component `y` is in `t`, and `r` holds between `x` and `y`.
|
Rel.mem_interedges_iff
theorem Rel.mem_interedges_iff :
∀ {α : Type u_4} {β : Type u_5} {r : α → β → Prop} [inst : (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
The theorem `Rel.mem_interedges_iff` states that for any types `α` and `β`, any relation `r` from `α` to `β` that is a decidable predicate, any finite sets `s` of type `α` and `t` of type `β`, and any pair `x` of type `α × β`, the pair `x` is an element of the finite set of edges between `s` and `t` (denoted as `Rel.interedges r s t`) if and only if the first element of `x` belongs to `s`, the second element of `x` belongs to `t`, and the relation `r` holds between the first and second elements of `x`.
More concisely: For any decidable relation $r$ between types $\alpha$ and $\beta$, sets $s$ and $t$ of finite elements from $\alpha$ and $\beta$ respectively, the pair $(x\_1, x\_2)$ is an edge between $s$ and $t$ in $r$ if and only if $x\_1 \in s$, $x\_2 \in t$, and $(x\_1, x\_2) \in r$.
|
Rel.swap_mem_interedges_iff
theorem Rel.swap_mem_interedges_iff :
∀ {α : Type u_4} {r : α → α → Prop} [inst : DecidableRel r] {s t : Finset α},
Symmetric r → ∀ {x : α × α}, x.swap ∈ Rel.interedges r s t ↔ x ∈ Rel.interedges r t s
This theorem states that, for any type `α` and a decidable relation `r` on `α`, given two finite sets `s` and `t` of type `α`, if `r` is symmetric, then for any pair of elements `x` of type `α`, the pair `x` is in the set of interedges of `r` between `t` and `s` if and only if the swapped pair of `x` is in the set of interedges of `r` between `s` and `t`. Here, "interedges" refers to a set of all pairs `(a, b)` from `s` and `t` respectively such that `a` is related to `b` under the relation `r`. The "swapped" of a pair `(a, b)` is the pair `(b, a)`. The symmetry of the relation `r` is crucial for this theorem, implying that if `a` is related to `b`, then `b` is also related to `a`.
More concisely: For any finite sets `s` and `t` of a type `α` with a decidable, symmetric relation `r`, the set of interedges between `s` and `t` is equal to the set of swapped interedges between `s` and `t`.
|
Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul
theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul :
∀ {𝕜 : Type u_1} {α : Type u_4} {β : Type u_5} [inst : LinearOrderedField 𝕜] (r : α → β → Prop)
[inst_1 : (a : α) → DecidablePred (r a)] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β} {δ : 𝕜},
s₂ ⊆ s₁ →
t₂ ⊆ t₁ →
0 ≤ δ →
(1 - δ) * ↑s₁.card ≤ ↑s₂.card →
(1 - δ) * ↑t₁.card ≤ ↑t₂.card → |↑(Rel.edgeDensity r s₂ t₂) - ↑(Rel.edgeDensity r s₁ t₁)| ≤ 2 * δ
This theorem, `Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul`, states that given a linear ordered field `𝕜`, types `α` and `β`, a relation `r` from `α` to `β`, and four finite subsets `s₁`, `s₂` of `α` and `t₁`, `t₂` of `β`, and a non-negative element `δ` in `𝕜`. If `s₂` is a subset of `s₁`, `t₂` is a subset of `t₁`, and the sizes of `s₂` and `t₂` are each at least `(1 - δ)` times that of `s₁` and `t₁` respectively, then the absolute difference in edge densities between the relations `r` restricted to `s₂` and `t₂` and to `s₁` and `t₁` is at most `2 * δ`.
Here, edge density of a relation between two sets of vertices is defined as the number of interedges divided by the product of the cardinals of the two sets. The theorem is essentially a statement about how edge densities can change when we consider subsets of the vertex sets and is significant in the study of graph theory.
More concisely: Given a linear ordered field 𝕜, types α and β, a relation r from α to β, and finite subsets s₁, s₂ of α and t₁, t₂ of β, if s₂ ⊆ s₁, t₂ ⊆ t₁, and |s₂|, |t₂| ≥ (1 - δ) * |s₁|, |t₁| for some δ ≥ 0, then the absolute difference in edge densities between r restricted to s₂ and t₂, and r restricted to s₁ and t₁ is at most 2 * δ.
|