Lattice valuations and the Jaccard distance

DefinitionModular valuation#✓fully proved

A function \(f \colon L \to \mathbb{R}\) on a lattice \(L\), with join \(\vee\) and meet \(\wedge\), is a modular valuation when \(f(X) + f(Y) = f(X \vee Y) + f(X \wedge Y)\) for all \(X, Y \in L\).

def IsModularValuation (f : L → ℝ) : Prop :=
  ∀ X Y, f X + f Y = f (X ⊔ Y) + f (X ⊓ Y)

Used by 3

Used byCharacterization of the Gilbert condition · Triangle inequality for the generalized Jaccard distance · Jaccard triangle inequality under the Gilbert condition

DefinitionStrictly positive valuation#✓fully proved

A function \(f \colon L \to \mathbb{R}\) on a lattice \(L\) is strictly positive when \(f(X) > 0\) for every \(X \in L\).

def IsStrictlyPositive (f : L → ℝ) : Prop :=
  ∀ X, 0 < f X

Used by 3

Used byJaccard distance as a single quotient · Triangle inequality for the generalized Jaccard distance · Jaccard triangle inequality under the Gilbert condition

DefinitionGilbert condition#✓fully proved

A function \(f \colon L \to \mathbb{R}\) on a lattice \(L\), with join \(\vee\) and meet \(\wedge\), satisfies the Gilbert condition when \(f(X \vee Z) + f(Z \vee Y) + f(X \wedge Y) \ge f(X \wedge Z) + f(Z \wedge Y) + f(X \vee Y \vee Z)\) for all \(X, Y, Z \in L\).

def GilbertCondition (f : L → ℝ) : Prop :=
  ∀ X Y Z, f (X ⊔ Z) + f (Z ⊔ Y) + f (X ⊓ Y) ≥
    f (X ⊓ Z) + f (Z ⊓ Y) + f (X ⊔ Y ⊔ Z)

Used by 3

Used byCharacterization of the Gilbert condition · Triangle inequality for the generalized Jaccard distance · Jaccard triangle inequality under the Gilbert condition

DefinitionGeneralized Jaccard distance#✓fully proved

For a function \(f \colon L \to \mathbb{R}\) on a lattice \(L\) with join \(\vee\) and meet \(\wedge\), the Jaccard distance of \(X, Y \in L\) is \(d_f(X, Y) = 1 - f(X \wedge Y) / f(X \vee Y)\).

Division by zero is taken to give \(0\), so \(d_f(X, Y) = 1\) when \(f(X \vee Y) = 0\).

noncomputable def jaccardDist (f : L → ℝ) (X Y : L) : ℝ :=
  1 - f (X ⊓ Y) / f (X ⊔ Y)

Used by 3

Used byJaccard distance as a single quotient · Triangle inequality for the generalized Jaccard distance · Jaccard triangle inequality under the Gilbert condition

TheoremCharacterization of the Gilbert condition#✓fully proved

A function \(f \colon L \to \mathbb{R}\) on a lattice \(L\) satisfies the Gilbert condition if and only if \(f\) is a modular valuation and is monotone, that is, \(X \le Y\) implies \(f(X) \le f(Y)\).

theorem gilbertCondition_iff {f : L → ℝ} :
    GilbertCondition f ↔ IsModularValuation f ∧ Monotone f

Uses 2

Statement usesGilbert condition · Modular valuation

TheoremJaccard distance as a single quotient#✓fully proved

Let \(f \colon L \to \mathbb{R}\) be a strictly positive function on a lattice \(L\), with join \(\vee\) and meet \(\wedge\). Then for all \(X, Y \in L\) the Jaccard distance of \(X\) and \(Y\) with respect to \(f\) is \(d_f(X, Y) = (f(X \vee Y) - f(X \wedge Y)) / f(X \vee Y)\).

theorem jaccardDist_eq_div {f : L → ℝ} (hpos : IsStrictlyPositive f) (X Y : L) :
    jaccardDist f X Y = (f (X ⊔ Y) - f (X ⊓ Y)) / f (X ⊔ Y)

Uses 2 · Used by 1

Statement usesStrictly positive valuation · Generalized Jaccard distance

Used byJaccard triangle inequality under the Gilbert condition

TheoremJaccard triangle inequality under the Gilbert condition#✓fully proved

Let \(f \colon L \to \mathbb{R}\) be a strictly positive function on a lattice \(L\) that satisfies the Gilbert condition, and let \(d_f\) be the Jaccard distance of \(f\). Then \(d_f(U, W) + d_f(W, V) \ge d_f(U, V)\) for all \(U, V, W \in L\).

theorem jaccardDist_triangle_of_gilbertCondition {f : L → ℝ}
    (hG : GilbertCondition f) (hpos : IsStrictlyPositive f) (U V W : L) :
    jaccardDist f U W + jaccardDist f W V ≥ jaccardDist f U V

Uses 5 · Used by 1

Statement usesGilbert condition · Strictly positive valuation · Generalized Jaccard distance

Proof usesModular valuation · Jaccard distance as a single quotient

Used byTriangle inequality for the generalized Jaccard distance

TheoremTriangle inequality for the generalized Jaccard distance#✓fully proved

Let \(f \colon L \to \mathbb{R}\) be a strictly positive, monotone modular valuation on a lattice \(L\), and let \(d_f\) be the Jaccard distance of \(f\). Then \(d_f(U, W) + d_f(W, V) \ge d_f(U, V)\) for all \(U, V, W \in L\).

theorem jaccardDist_triangle {f : L → ℝ} (hM : IsModularValuation f)
    (hmono : Monotone f) (hpos : IsStrictlyPositive f) (U V W : L) :
    jaccardDist f U W + jaccardDist f W V ≥ jaccardDist f U V

Uses 5

Statement usesModular valuation · Strictly positive valuation · Generalized Jaccard distance

Proof usesGilbert condition · Jaccard triangle inequality under the Gilbert condition

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.