Documentation

Mathlib.Topology.MetricSpace.BundledFun

Pseudometrics as bundled functions #

This file defines a pseudometric as a bundled function. This allows one to define a semilattice on them, and to construct families of pseudometrics.

Implementation notes #

The PseudoMetric definition is made as general as possible without any required axioms for the codomain. The axioms come into play only in proofs and further constructions like the SemilatticeSup instance. This allows one to talk about functions mapping into something like { fuel: ℕ, time: ℕ } even though there is no linear order.

In most cases, the codomain will be a linear ordered additive monoid like ℝ, ℝ≥0, ℝ≥0∞, in which all of the axioms below are satisfied.

structure PseudoMetric (X : Type u_1) (R : Type u_2) [Zero R] [Add R] [LE R] :

Type (max u_1 u_2)

A pseudometric as a bundled function.

toFun : X → X → R
The underlying binary function mapping into a linearly ordered additive monoid.
refl' (x : X) : self.toFun x x = 0
A pseudometric must take identical elements to 0.
symm' (x y : X) : self.toFun x y = self.toFun y x
A pseudometric must be symmetric.
triangle' (x y z : X) : self.toFun x z ≤ self.toFun x y + self.toFun y z
A pseudometric must respect the triangle inequality.

Instances For

theorem PseudoMetric.ext {X : Type u_1} {R : Type u_2} {inst✝ : Zero R} {inst✝¹ : Add R} {inst✝² : LE R} {x y : PseudoMetric X R} (toFun : x.toFun = y.toFun) :

x = y

theorem PseudoMetric.ext_iff {X : Type u_1} {R : Type u_2} {inst✝ : Zero R} {inst✝¹ : Add R} {inst✝² : LE R} {x y : PseudoMetric X R} :

x = y ↔ x.toFun = y.toFun

instance PseudoMetric.instFunLikeForall {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] :

FunLike (PseudoMetric X R) X (X → R)

Equations

PseudoMetric.instFunLikeForall = { coe := PseudoMetric.toFun, coe_injective' := ⋯ }

@[simp]

theorem PseudoMetric.coe_mk {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] (d : X → X → R) (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z) :

⇑{ toFun := d, refl' := refl, symm' := symm, triangle' := triangle } = d

theorem PseudoMetric.mk_apply {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] (d : X → X → R) (refl : ∀ (x : X), d x x = 0) (symm : ∀ (x y : X), d x y = d y x) (triangle : ∀ (x y z : X), d x z ≤ d x y + d y z) (x y : X) :

{ toFun := d, refl' := refl, symm' := symm, triangle' := triangle } x y = d x y

@[simp]

theorem PseudoMetric.refl {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] (d : PseudoMetric X R) (x : X) :

d x x = 0

theorem PseudoMetric.symm {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] (d : PseudoMetric X R) (x y : X) :

d x y = d y x

theorem PseudoMetric.triangle {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] (d : PseudoMetric X R) (x y z : X) :

d x z ≤ d x y + d y z

instance PseudoMetric.instLE {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] :

LE (PseudoMetric X R)

Equations

PseudoMetric.instLE = { le := fun (d d' : PseudoMetric X R) => ⇑d ≤ ⇑d' }

@[simp]

theorem PseudoMetric.coe_le_coe {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] {d d' : PseudoMetric X R} :

⇑d ≤ ⇑d' ↔ d ≤ d'

instance PseudoMetric.instPartialOrder {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [PartialOrder R] :

PartialOrder (PseudoMetric X R)

Equations

PseudoMetric.instPartialOrder = PartialOrder.lift (fun (f : PseudoMetric X R) => ⇑f) ⋯

instance PseudoMetric.instBot {X : Type u_1} {R : Type u_2} [AddZeroClass R] [Preorder R] :

Bot (PseudoMetric X R)

Equations

PseudoMetric.instBot = { bot := { toFun := 0, refl' := ⋯, symm' := ⋯, triangle' := ⋯ } }

@[simp]

theorem PseudoMetric.coe_bot {X : Type u_1} {R : Type u_2} [AddZeroClass R] [Preorder R] :

⇑⊥ = 0

@[simp]

theorem PseudoMetric.bot_apply {X : Type u_1} {R : Type u_2} [AddZeroClass R] [Preorder R] (x y : X) :

⊥ x y = 0

instance PseudoMetric.instMaxOfAddLeftMonoOfAddRightMono {X : Type u_1} {R : Type u_2} [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] :

Max (PseudoMetric X R)

Equations

PseudoMetric.instMaxOfAddLeftMonoOfAddRightMono = { max := fun (d d' : PseudoMetric X R) => { toFun := fun (x y : X) => d x y ⊔ d' x y, refl' := ⋯, symm' := ⋯, triangle' := ⋯ } }

@[simp]

theorem PseudoMetric.coe_sup {X : Type u_1} {R : Type u_2} [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] (d d' : PseudoMetric X R) :

⇑(d ⊔ d') = ⇑d ⊔ ⇑d'

@[simp]

theorem PseudoMetric.sup_apply {X : Type u_1} {R : Type u_2} [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] (d d' : PseudoMetric X R) (x y : X) :

(d ⊔ d') x y = d x y ⊔ d' x y

instance PseudoMetric.instSemilatticeSupOfAddLeftMonoOfAddRightMono {X : Type u_1} {R : Type u_2} [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] :

SemilatticeSup (PseudoMetric X R)

Equations

PseudoMetric.instSemilatticeSupOfAddLeftMonoOfAddRightMono = { toPartialOrder := PseudoMetric.instPartialOrder, sup := max, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

theorem PseudoMetric.nonneg {X : Type u_1} {R : Type u_2} [AddCommMonoid R] [LinearOrder R] [AddLeftStrictMono R] (d : PseudoMetric X R) (x y : X) :

0 ≤ d x y

instance PseudoMetric.instOrderBot {X : Type u_1} {R : Type u_2} [AddCommMonoid R] [LinearOrder R] [AddLeftStrictMono R] :

OrderBot (PseudoMetric X R)

Equations

PseudoMetric.instOrderBot = { toBot := PseudoMetric.instBot, bot_le := ⋯ }

@[simp]

theorem PseudoMetric.coe_finsetSup {X : Type u_1} {R : Type u_2} [AddCommMonoid R] [LinearOrder R] [AddLeftStrictMono R] [IsOrderedAddMonoid R] {Y : Type u_3} {f : Y → PseudoMetric X R} {s : Finset Y} (hs : s.Nonempty) :

⇑(s.sup f) = ⇑(s.sup' hs fun (x : Y) => f x)

theorem PseudoMetric.finsetSup_apply {X : Type u_1} {R : Type u_2} [AddCommMonoid R] [LinearOrder R] [AddLeftStrictMono R] [IsOrderedAddMonoid R] {Y : Type u_3} {f : Y → PseudoMetric X R} {s : Finset Y} (hs : s.Nonempty) (x y : X) :

(s.sup f) x y = s.sup' hs fun (i : Y) => (f i) x y

class PseudoMetric.IsUltra {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] [Max R] (d : PseudoMetric X R) :

A pseudometric can be nonarchimedean (or ultrametric), with a stronger triangle inequality such that d x z ≤ max (d x y) (d y z).

le_sup' (x y z : X) : d x z ≤ d x y ⊔ d y z
Strong triangle inequality of an ultrametric.

Instances

theorem PseudoMetric.IsUltra.le_sup {X : Type u_1} {R : Type u_2} [Zero R] [Add R] [LE R] [Max R] {d : PseudoMetric X R} [hd : d.IsUltra] {x y z : X} :

d x z ≤ d x y ⊔ d y z

instance PseudoMetric.IsUltra.bot {X : Type u_1} {R : Type u_2} [AddZeroClass R] [SemilatticeSup R] :

instance PseudoMetric.IsUltra.sup {X : Type u_1} {R : Type u_2} [AddZeroClass R] [SemilatticeSup R] [AddLeftMono R] [AddRightMono R] {d d' : PseudoMetric X R} [d.IsUltra] [d'.IsUltra] :

(d ⊔ d').IsUltra

theorem PseudoMetric.IsUltra.finsetSup {X : Type u_1} {R : Type u_2} {Y : Type u_3} [AddCommMonoid R] [LinearOrder R] [AddLeftStrictMono R] [IsOrderedAddMonoid R] {f : Y → PseudoMetric X R} {s : Finset Y} (h : ∀ d ∈ s, (f d).IsUltra) :

(s.sup f).IsUltra

theorem PseudoMetric.isSymmetricRel_ball {X : Type u_1} {R : Type u_2} [Add R] [Zero R] [Preorder R] (d : PseudoMetric X R) {ε : R} :

IsSymmetricRel {xy : X × X | d xy.1 xy.2 < ε}

theorem PseudoMetric.isSymmetricRel_closedBall {X : Type u_1} {R : Type u_2} [Add R] [Zero R] [LE R] (d : PseudoMetric X R) {ε : R} :

IsSymmetricRel {xy : X × X | d xy.1 xy.2 ≤ ε}

theorem PseudoMetric.IsUltra.isTransitiveRel_ball {X : Type u_1} {R : Type u_2} [Add R] [Zero R] [LinearOrder R] (d : PseudoMetric X R) [d.IsUltra] {ε : R} :

IsTransitiveRel {xy : X × X | d xy.1 xy.2 < ε}

theorem PseudoMetric.IsUltra.isTransitiveRel_closedBall {X : Type u_1} {R : Type u_2} [Add R] [Zero R] [SemilatticeSup R] (d : PseudoMetric X R) [d.IsUltra] {ε : R} :

IsTransitiveRel {xy : X × X | d xy.1 xy.2 ≤ ε}