A theorem on metrics based on min and max

In this file we give a formal proof of Theorem 17 from [KNYHLM20]. It asserts that d(X,Y)= m min(|X\Y|, |Y\X|) + M max(|X\Y|, |Y\X|) is a metric if and only if m ≤ M.

Main results

• seventeen: the proof of Theorem 17.
• instance jaccard_numerator.metric_space: the realization as a metric_space type.

Notation

• |_| : Notation for cardinality.

References

See [KNYHLM20] for the original proof.

def «term|_|» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem disj₁ {α : Type u_1} [DecidableEq α] (X Y Z : Finset α) : Disjoint (X \ Y ∪ Y \ Z) (Z \ X)

theorem disj₂ {α : Type u_1} [DecidableEq α] (X Y Z : Finset α) : Disjoint (X \ Y) (Y \ Z)

theorem union_rot_sdiff {α : Type u_1} [DecidableEq α] (X Y Z : Finset α) : X \ Y ∪ Y \ Z ∪ Z \ X = X \ Z ∪ Z \ Y ∪ Y \ X

theorem card_rot {α : Type u_1} [DecidableEq α] (X Y Z : Finset α) : |X \ Y| + |Y \ Z| + |Z \ X| = |X \ Z| + |Z \ Y| + |Y \ X|

theorem card_rot_cast {α : Type u_1} [DecidableEq α] (X Y Z : Finset α) : ↑|X \ Y| + ↑|Y \ Z| + ↑|Z \ X| = ↑|X \ Z| + ↑|Z \ Y| + ↑|Y \ X|

noncomputable def δ {α : Type u_1} [DecidableEq α] : ℝ → ℝ → Finset α → Finset α → ℝ

Equations

• δ m M A B = M * (↑|A \ B| ⊔ ↑|B \ A|) + m * ↑(|A \ B| ⊓ |B \ A|)

theorem delta_cast {α : Type u_1} [DecidableEq α] {m M : ℝ} {A B : Finset α} : δ m M A B = M * (↑|A \ B| ⊔ ↑|B \ A|) + m * (↑|A \ B| ⊓ ↑|B \ A|)

theorem delta_comm {α : Type u_1} [DecidableEq α] {m M : ℝ} (A B : Finset α) : δ m M A B = δ m M B A

theorem delta_self {m M : ℝ} {α : Type u_1} [DecidableEq α] (X : Finset α) : δ m M X X = 0

theorem subseteq_of_card_zero {α : Type u_1} [DecidableEq α] (x y : Finset α) : |x \ y| = 0 → x ⊆ y

theorem card_zero_of_not_pos {α : Type u_1} [DecidableEq α] (X : Finset α) : ¬0 < |X| → |X| = 0

theorem eq_zero_of_nonneg_of_nonneg_of_add_zero {a b : ℝ} : 0 ≤ a → 0 ≤ b → 0 = a + b → 0 = a

theorem subset_of_delta_eq_zero {m M : ℝ} {α : Type u_1} [DecidableEq α] (hm : 0 < m) (hM : m ≤ M) (X Y : Finset α) (h : δ m M X Y = 0) : X ⊆ Y

theorem eq_of_delta_eq_zero {m M : ℝ} {α : Type u_1} [DecidableEq α] (hm : 0 < m) (hM : m ≤ M) (X Y : Finset α) (h : δ m M X Y = 0) : X = Y

theorem sdiff_covering {α : Type u_1} [DecidableEq α] {A B C : Finset α} : A \ C ⊆ A \ B ∪ B \ C

theorem sdiff_triangle' {α : Type u_1} [DecidableEq α] (A B C : Finset α) : |A \ C| ≤ |A \ B| + |B \ C|

theorem venn {α : Type u_1} [DecidableEq α] (X Y : Finset α) : X = X \ Y ∪ X ∩ Y

theorem venn_card {α : Type u_1} [DecidableEq α] (X Y : Finset α) : |X| = |X \ Y| + |X ∩ Y|

theorem sdiff_card {α : Type u_1} [DecidableEq α] (X Y : Finset α) : |Y| ≤ |X| → |Y \ X| ≤ |X \ Y|

theorem maxmin_1 {m M : ℝ} {α : Type u_1} [DecidableEq α] {X Y : Finset α} : |X| ≤ |Y| → δ m M X Y = M * ↑|Y \ X| + m * ↑|X \ Y|

theorem maxmin_2 {m M : ℝ} {α : Type u_1} [DecidableEq α] {X Y : Finset α} : |Y| ≤ |X| → δ m M X Y = M * ↑|X \ Y| + m * ↑|Y \ X|

theorem casting {a b : ℕ} : a ≤ b → ↑a ≤ ↑b

theorem mul_sdiff_tri {α : Type u_1} [DecidableEq α] (m : ℝ) (hm : 0 ≤ m) (X Y Z : Finset α) : m * ↑|X \ Z| ≤ m * (↑|X \ Y| + ↑|Y \ Z|)

def triangle_inequality {α : Type u_1} [DecidableEq α] (m M : ℝ) (X Y Z : Finset α) : Prop

Equations

• triangle_inequality m M X Y Z = (δ m M X Y ≤ δ m M X Z + δ m M Z Y)

theorem seventeen_right_yzx {α : Type u_1} [DecidableEq α] {m M : ℝ} {X Y Z : Finset α} : 0 ≤ m → m ≤ M → |Y| ≤ |Z| ∧ |Z| ≤ |X| → triangle_inequality m M X Y Z

theorem co_sdiff {α : Type u_1} [DecidableEq α] (X Y U : Finset α) : X ⊆ U → Y ⊆ U → (U \ X) \ (U \ Y) = Y \ X

theorem co_sdiff_card {α : Type u_1} [DecidableEq α] (X Y U : Finset α) : X ⊆ U → Y ⊆ U → |(U \ X) \ (U \ Y)| = |Y \ X|

theorem co_sdiff_card_max {α : Type u_1} [DecidableEq α] (X Y U : Finset α) : X ⊆ U → Y ⊆ U → |(U \ Y) \ (U \ X)| ⊔ |(U \ X) \ (U \ Y)| = |X \ Y| ⊔ |Y \ X|

theorem co_sdiff_card_min {α : Type u_1} [DecidableEq α] (X Y U : Finset α) : X ⊆ U → Y ⊆ U → |(U \ Y) \ (U \ X)| ⊓ |(U \ X) \ (U \ Y)| = |X \ Y| ⊓ |Y \ X|

theorem delta_complement {m M : ℝ} {α : Type u_1} [DecidableEq α] (X Y U : Finset α) : X ⊆ U → Y ⊆ U → δ m M X Y = δ m M (U \ Y) (U \ X)

theorem seventeen_right_yxz {α : Type u_1} [DecidableEq α] {m M : ℝ} {X Y Z : Finset α} : 0 ≤ m → m ≤ M → |Y| ≤ |X| ∧ |X| ≤ |Z| → triangle_inequality m M X Y Z

theorem sdiff_card_le {α : Type u_1} [DecidableEq α] (X Y U : Finset α) (hx : X ⊆ U) (hy : Y ⊆ U) (h : |X| ≤ |Y|) : |U \ Y| ≤ |U \ X|

theorem seventeen_right_zyx {α : Type u_1} [DecidableEq α] {m M : ℝ} {X Y Z : Finset α} : 0 ≤ m → m ≤ M → |Z| ≤ |Y| ∧ |Y| ≤ |X| → triangle_inequality m M X Y Z

theorem seventeen_right_zxy {m M : ℝ} {α : Type u_1} [DecidableEq α] {X Y Z : Finset α} : 0 ≤ m → m ≤ M → |Z| ≤ |X| ∧ |X| ≤ |Y| → triangle_inequality m M X Y Z

theorem three_places {x y z : ℕ} : y ≤ x → z ≤ y ∧ y ≤ x ∨ y ≤ z ∧ z ≤ x ∨ y ≤ x ∧ x ≤ z

theorem seventeen_right_y_le_x {α : Type u_1} [DecidableEq α] {m M : ℝ} {X Y Z : Finset α} : |Y| ≤ |X| → 0 ≤ m → m ≤ M → triangle_inequality m M X Y Z

theorem seventeen_right_x_le_y {α : Type u_1} [DecidableEq α] {m M : ℝ} {X Y Z : Finset α} : |X| ≤ |Y| → 0 ≤ m → m ≤ M → triangle_inequality m M X Y Z

theorem seventeen_right {α : Type u_1} [DecidableEq α] {m M : ℝ} {X Y Z : Finset α} : 0 ≤ m → m ≤ M → triangle_inequality m M X Y Z

def s_0 : Finset ℕ

Equations

• s_0 = {0}

def s_1 : Finset ℕ

Equations

• s_1 = {1}

def s01 : Finset ℕ

Equations

• s01 = {0, 1}

theorem seventeen {m M : ℝ} : 0 ≤ m → (m ≤ M ↔ ∀ (X Y Z : Finset ℕ), triangle_inequality m M X Y Z)

def delta_triangle {m M : ℝ} (X Y Z : Finset ℕ) (hm : 0 < m) (hM : m ≤ M) : triangle_inequality m M X Z Y

Equations

• ⋯ = ⋯

noncomputable instance instMetricSpaceFinsetNatOfLtOfNatOfLeReal_jaccard {m M : ℝ} (hm : 0 < m) (hM : m ≤ M) : MetricSpace (Finset ℕ)

Instantiate Finset ℕ as a metric space.

Equations

• instMetricSpaceFinsetNatOfLtOfNatOfLeReal_jaccard hm hM = MetricSpace.mk ⋯