Torsors of additive normed group actions.

This file defines torsors of additive normed group actions, with a metric space structure. The motivating case is Euclidean affine spaces.

class NormedAddTorsor (V : outParam (Type u_1)) (P : Type u_2) [SeminormedAddCommGroup V] [PseudoMetricSpace P] extends AddTorsor V P : Type (max u_1 u_2)

A NormedAddTorsor V P is a torsor of an additive seminormed group action by a SeminormedAddCommGroup V on points P. We bundle the pseudometric space structure and require the distance to be the same as results from the norm (which in fact implies the distance yields a pseudometric space, but bundling just the distance and using an instance for the pseudometric space results in type class problems).

• vadd : V → P → P
• add_vadd (g₁ g₂ : V) (p : P) : (g₁ + g₂) +ᵥ p = g₁ +ᵥ g₂ +ᵥ p
• zero_vadd (p : P) : 0 +ᵥ p = p
• vsub : P → P → V
• nonempty : Nonempty P
• vsub_vadd' (p₁ p₂ : P) : (p₁ -ᵥ p₂) +ᵥ p₂ = p₁
• vadd_vsub' (g : V) (p : P) : (g +ᵥ p) -ᵥ p = g
• dist_eq_norm' (x y : P) : dist x y = ‖x -ᵥ y‖

@[implicit_reducible, instance 100]

instance NormedAddTorsor.toAddTorsor' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [MetricSpace P] [NormedAddTorsor V P] : AddTorsor V P

Shortcut instance to help typeclass inference out.

@[instance 100]

instance NormedAddTorsor.to_isIsIsometricVAdd {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] : IsIsometricVAdd V P

@[implicit_reducible, instance 100]

instance SeminormedAddCommGroup.toNormedAddTorsor {V : Type u_2} [SeminormedAddCommGroup V] : NormedAddTorsor V V

A SeminormedAddCommGroup is a NormedAddTorsor over itself.

@[implicit_reducible]

instance AffineSubspace.toNormedAddTorsor {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {R : Type u_6} [Ring R] [Module R V] (s : AffineSubspace R P) [Nonempty ↥s] : NormedAddTorsor ↥s.direction ↥s

A nonempty affine subspace of a NormedAddTorsor is itself a NormedAddTorsor.

@[implicit_reducible]

instance instNormedAddTorsorProd {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] : NormedAddTorsor (V × W) (P × Q)

theorem dist_eq_norm_vsub (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) : dist x y = ‖x -ᵥ y‖

The distance equals the norm of subtracting two points. In this lemma, it is necessary to have V as an explicit argument; otherwise rw dist_eq_norm_vsub sometimes doesn't work.

theorem nndist_eq_nnnorm_vsub (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) : nndist x y = ‖x -ᵥ y‖₊

theorem dist_eq_norm_vsub' (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) : dist x y = ‖y -ᵥ x‖

The distance equals the norm of subtracting two points. In this lemma, it is necessary to have V as an explicit argument; otherwise rw dist_eq_norm_vsub' sometimes doesn't work.

theorem nndist_eq_nnnorm_vsub' (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y : P) : nndist x y = ‖y -ᵥ x‖₊

theorem dist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x y : P) : dist (v +ᵥ x) (v +ᵥ y) = dist x y

theorem nndist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x y : P) : nndist (v +ᵥ x) (v +ᵥ y) = nndist x y

@[simp]

theorem dist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v₁ v₂ : V) (x : P) : dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂

@[simp]

theorem nndist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v₁ v₂ : V) (x : P) : nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂

@[simp]

theorem dist_vadd_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖

@[simp]

theorem nndist_vadd_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) : nndist (v +ᵥ x) x = ‖v‖₊

@[simp]

theorem dist_vadd_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) : dist x (v +ᵥ x) = ‖v‖

@[simp]

theorem nndist_vadd_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) : nndist x (v +ᵥ x) = ‖v‖₊

def IsometryEquiv.vaddConst {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) : V ≃ᵢ P

Isometry between the tangent space V of a (semi)normed add torsor P and P given by addition/subtraction of x : P.

@[simp]

theorem IsometryEquiv.vaddConst_apply {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (v : V) : (vaddConst x) v = v +ᵥ x

@[simp]

theorem IsometryEquiv.vaddConst_symm_apply {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x p' : P) : (vaddConst x).symm p' = p' -ᵥ x

@[simp]

theorem dist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z

@[simp]

theorem nndist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y z : P) : nndist (x -ᵥ y) (x -ᵥ z) = nndist y z

def IsometryEquiv.constVSub {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) : P ≃ᵢ V

Isometry between the tangent space V of a (semi)normed add torsor P and P given by subtraction from x : P.

@[simp]

theorem IsometryEquiv.constVSub_apply {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x x✝ : P) : (constVSub x) x✝ = x -ᵥ x✝

@[simp]

theorem IsometryEquiv.constVSub_symm_apply {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (x✝ : V) : (constVSub x).symm x✝ = -x✝ +ᵥ x

@[simp]

theorem dist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y

@[simp]

theorem nndist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x y z : P) : nndist (x -ᵥ z) (y -ᵥ z) = nndist x y

theorem dist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v v' : V) (p p' : P) : dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'

theorem nndist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v v' : V) (p p' : P) : nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'

theorem dist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ p₄ : P) : dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄

theorem nndist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ p₄ : P) : nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄

theorem edist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v v' : V) (p p' : P) : edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'

theorem edist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ p₄ : P) : edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄

@[implicit_reducible]

def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V : Type u_6) (P : Type u_7) [SeminormedAddCommGroup V] [AddTorsor V P] : PseudoMetricSpace P

The pseudodistance defines a pseudometric space structure on the torsor. This is not an instance because it depends on V to define a MetricSpace P.

@[implicit_reducible]

def metricSpaceOfNormedAddCommGroupOfAddTorsor (V : Type u_6) (P : Type u_7) [NormedAddCommGroup V] [AddTorsor V P] : MetricSpace P

The distance defines a metric space structure on the torsor. This is not an instance because it depends on V to define a MetricSpace P.

theorem LipschitzWith.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [PseudoEMetricSpace α] {f : α → V} {g : α → P} {Kf Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) (f +ᵥ g)

theorem LipschitzWith.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [PseudoEMetricSpace α] {f g : α → P} {Kf Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) (f -ᵥ g)

theorem uniformContinuous_vadd {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] : UniformContinuous fun (x : V × P) => x.1 +ᵥ x.2

theorem uniformContinuous_vsub {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] : UniformContinuous fun (x : P × P) => x.1 -ᵥ x.2

instance instIsTopologicalAddTorsor_1 {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] : IsTopologicalAddTorsor P

@[reducible, inline]

abbrev Function.Injective.normedAddTorsor {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {Q : Type u_6} [VAdd V Q] [VSub V Q] [Nonempty Q] [PseudoMetricSpace Q] (f : Q → P) (hf : Injective f) (vadd : ∀ (c : V) (x : Q), f (c +ᵥ x) = c +ᵥ f x) (vsub : ∀ (x y : Q), x -ᵥ y = f x -ᵥ f y) (norm : ∀ (x y : Q), dist x y = dist (f x) (f y)) : NormedAddTorsor V Q

Pullback of a normed add torsor along an injective map.

@[reducible, inline]

abbrev Function.Surjective.normedAddTorsor {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {Q : Type u_6} [VAdd V Q] [VSub V Q] [PseudoMetricSpace Q] (f : P → Q) (hf : Surjective f) (vadd : ∀ (c : V) (x : P), f (c +ᵥ x) = c +ᵥ f x) (vsub : ∀ (x y : P), x -ᵥ y = f x -ᵥ f y) (norm : ∀ (x y : P), dist x y = dist (f x) (f y)) : NormedAddTorsor V Q

Pushforward of a normed add torsor along a surjective map.