Dilation equivalence #

In this file we define DilationEquiv X Y, a type of bundled equivalences between X and Ysuch thatedist (f x) (f y) = r * edist x yfor somer : ℝ≥0, r ≠ 0`.

We also develop basic API about these equivalences.

TODO #

Add missing lemmas (compare to other *Equiv structures).
[after-port] Add DilationEquivInstance for IsometryEquiv.

source

class DilationEquivClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] extends EquivLike :

Type (max (max u_1 u_2) u_3)

coe : F → X → Y
inv : F → Y → X
left_inv : ∀ (e : F), Function.LeftInverse (EquivLike.inv e) (EquivLike.coe e)
right_inv : ∀ (e : F), Function.RightInverse (EquivLike.inv e) (EquivLike.coe e)
coe_injective' : ∀ (e g : F), EquivLike.coe e = EquivLike.coe g → EquivLike.inv e = EquivLike.inv g → e = g
edist_eq' : ∀ (f : F), ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (↑f x) (↑f y) = ↑r * edist x y

Typeclass saying that F is a type of bundled equivalences such that all e : F are dilations.

Instances

source

instance instDilationClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [DilationEquivClass F X Y] :

DilationClass F X Y

source

structure DilationEquiv (X : Type u_1) (Y : Type u_2) [PseudoEMetricSpace X] [PseudoEMetricSpace Y] extends Equiv :

Type (max u_1 u_2)

toFun : X → Y
invFun : Y → X
left_inv : Function.LeftInverse s.invFun s.toFun
right_inv : Function.RightInverse s.invFun s.toFun
edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun s.toEquiv x) (Equiv.toFun s.toEquiv y) = ↑r * edist x y

Type of equivalences X ≃ Y such that ∀ x y, edist (f x) (f y) = r * edist x y for some r : ℝ≥0, r ≠ 0.

Instances For

source

def «term_≃ᵈ_» :

Lean.TrailingParserDescr

Instances For

source

instance DilationEquiv.instDilationEquivClassDilationEquiv {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] :

DilationEquivClass (X ≃ᵈ Y) X Y

source

instance DilationEquiv.instCoeFunDilationEquivForAll {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] :

CoeFun (X ≃ᵈ Y) fun x => X → Y

source

@[simp]

theorem DilationEquiv.coe_toEquiv {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

↑e.toEquiv = ↑e

source

theorem DilationEquiv.ext {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] {e : X ≃ᵈ Y} {e' : X ≃ᵈ Y} (h : ∀ (x : X), ↑e x = ↑e' x) :

e = e'

source

def DilationEquiv.symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

Y ≃ᵈ X

Inverse DilationEquiv.

Instances For

source

@[simp]

theorem DilationEquiv.symm_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

DilationEquiv.symm (DilationEquiv.symm e) = e

source

@[simp]

theorem DilationEquiv.apply_symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : Y) :

↑e (↑(DilationEquiv.symm e) x) = x

source

@[simp]

theorem DilationEquiv.symm_apply_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) (x : X) :

↑(DilationEquiv.symm e) (↑e x) = x

source

def DilationEquiv.Simps.symm_apply {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

Y → X

See Note [custom simps projection].

Instances For

source

@[simp]

theorem DilationEquiv.refl_apply (X : Type u_4) [PseudoEMetricSpace X] :

↑(DilationEquiv.refl X) = id

source

def DilationEquiv.refl (X : Type u_4) [PseudoEMetricSpace X] :

X ≃ᵈ X

Identity map as a DilationEquiv.

Instances For

source

@[simp]

theorem DilationEquiv.refl_symm {X : Type u_1} [PseudoEMetricSpace X] :

DilationEquiv.symm (DilationEquiv.refl X) = DilationEquiv.refl X

source

@[simp]

theorem DilationEquiv.ratio_refl {X : Type u_1} [PseudoEMetricSpace X] :

Dilation.ratio (DilationEquiv.refl X) = 1

source

@[simp]

theorem DilationEquiv.trans_apply {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) :

↑(DilationEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁

source

def DilationEquiv.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e₁ : X ≃ᵈ Y) (e₂ : Y ≃ᵈ Z) :

X ≃ᵈ Z

Composition of DilationEquivs.

Instances For

source

@[simp]

theorem DilationEquiv.refl_trans {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

DilationEquiv.trans (DilationEquiv.refl X) e = e

source

@[simp]

theorem DilationEquiv.trans_refl {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

DilationEquiv.trans e (DilationEquiv.refl Y) = e

source

@[simp]

theorem DilationEquiv.symm_trans_self {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

DilationEquiv.trans (DilationEquiv.symm e) e = DilationEquiv.refl Y

source

@[simp]

theorem DilationEquiv.self_trans_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

DilationEquiv.trans e (DilationEquiv.symm e) = DilationEquiv.refl X

source

theorem DilationEquiv.surjective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

Function.Surjective ↑e

source

theorem DilationEquiv.bijective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

Function.Bijective ↑e

source

theorem DilationEquiv.injective {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

Function.Injective ↑e

source

@[simp]

theorem DilationEquiv.ratio_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] [PseudoEMetricSpace Z] (e : X ≃ᵈ Y) (e' : Y ≃ᵈ Z) :

Dilation.ratio (DilationEquiv.trans e e') = Dilation.ratio e * Dilation.ratio e'

source

@[simp]

theorem DilationEquiv.ratio_symm {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (e : X ≃ᵈ Y) :

Dilation.ratio (DilationEquiv.symm e) = (Dilation.ratio e)⁻¹

source

instance DilationEquiv.instGroupDilationEquiv {X : Type u_1} [PseudoEMetricSpace X] :

Group (X ≃ᵈ X)

source

theorem DilationEquiv.mul_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (e' : X ≃ᵈ X) :

e * e' = DilationEquiv.trans e' e

source

theorem DilationEquiv.one_def {X : Type u_1} [PseudoEMetricSpace X] :

1 = DilationEquiv.refl X

source

theorem DilationEquiv.inv_def {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :

e⁻¹ = DilationEquiv.symm e

source

@[simp]

theorem DilationEquiv.coe_mul {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (e' : X ≃ᵈ X) :

↑(e * e') = ↑e ∘ ↑e'

source

@[simp]

theorem DilationEquiv.coe_one {X : Type u_1} [PseudoEMetricSpace X] :

↑1 = id

source

theorem DilationEquiv.coe_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :

↑e⁻¹ = ↑(DilationEquiv.symm e)

source

noncomputable def DilationEquiv.ratioHom {X : Type u_1} [PseudoEMetricSpace X] :

(X ≃ᵈ X) →* NNReal

Dilation.ratio as a monoid homomorphism.

Instances For

source

@[simp]

theorem DilationEquiv.ratio_inv {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :

Dilation.ratio e⁻¹ = (Dilation.ratio e)⁻¹

source

@[simp]

theorem DilationEquiv.ratio_pow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℕ) :

Dilation.ratio (e ^ n) = Dilation.ratio e ^ n

source

@[simp]

theorem DilationEquiv.ratio_zpow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℤ) :

Dilation.ratio (e ^ n) = Dilation.ratio e ^ n

source

@[simp]

theorem DilationEquiv.toPerm_apply {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) :

↑DilationEquiv.toPerm e = e.toEquiv

source

def DilationEquiv.toPerm {X : Type u_1} [PseudoEMetricSpace X] :

(X ≃ᵈ X) →* Equiv.Perm X

DilationEquiv.toEquiv as a monoid homomorphism.

Instances For

source

theorem DilationEquiv.coe_pow {X : Type u_1} [PseudoEMetricSpace X] (e : X ≃ᵈ X) (n : ℕ) :

↑(e ^ n) = (↑e)^[n]