# 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) extends :
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).

• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : V) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• vsub : PPV
• nonempty :
• 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
Instances
theorem NormedAddTorsor.dist_eq_norm' {V : outParam (Type u_1)} {P : Type u_2} [self : ] (x : P) (y : P) :
dist x y = x -ᵥ y
@[instance 100]
instance NormedAddTorsor.toAddTorsor' {V : Type u_1} {P : Type u_2} [] [] :

Shortcut instance to help typeclass inference out.

Equations
@[instance 100]
instance NormedAddTorsor.to_isometricVAdd {V : Type u_2} {P : Type u_3} [] :
Equations
• =
@[instance 100]

A SeminormedAddCommGroup is a NormedAddTorsor over itself.

Equations
instance AffineSubspace.toNormedAddTorsor {V : Type u_2} {P : Type u_3} [] {R : Type u_6} [Ring R] [Module R V] (s : ) [Nonempty s] :

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

Equations
theorem dist_eq_norm_vsub (V : Type u_2) {P : Type u_3} [] (x : P) (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} [] (x : P) (y : P) :
theorem dist_eq_norm_vsub' (V : Type u_2) {P : Type u_3} [] (x : P) (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} [] (x : P) (y : P) :
theorem dist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [] (v : V) (x : P) (y : P) :
dist (v +ᵥ x) (v +ᵥ y) = dist x y
theorem nndist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [] (v : V) (x : P) (y : P) :
nndist (v +ᵥ x) (v +ᵥ y) = nndist x y
@[simp]
theorem dist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [] (v₁ : 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} [] (v₁ : 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} [] (v : V) (x : P) :
dist (v +ᵥ x) x = v
@[simp]
theorem nndist_vadd_left {V : Type u_2} {P : Type u_3} [] (v : V) (x : P) :
@[simp]
theorem dist_vadd_right {V : Type u_2} {P : Type u_3} [] (v : V) (x : P) :
dist x (v +ᵥ x) = v
@[simp]
theorem nndist_vadd_right {V : Type u_2} {P : Type u_3} [] (v : V) (x : P) :
@[simp]
theorem IsometryEquiv.vaddConst_apply {V : Type u_2} {P : Type u_3} [] (x : P) (v : V) :
= v +ᵥ x
@[simp]
theorem IsometryEquiv.vaddConst_toFun {V : Type u_2} {P : Type u_3} [] (x : P) (v : V) :
= v +ᵥ x
@[simp]
theorem IsometryEquiv.vaddConst_invFun {V : Type u_2} {P : Type u_3} [] (x : P) (p' : P) :
.invFun p' = p' -ᵥ x
@[simp]
theorem IsometryEquiv.vaddConst_symm_apply {V : Type u_2} {P : Type u_3} [] (x : P) (p' : P) :
.symm p' = p' -ᵥ x
def IsometryEquiv.vaddConst {V : Type u_2} {P : Type u_3} [] (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.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem dist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [] (x : P) (y : P) (z : P) :
dist (x -ᵥ y) (x -ᵥ z) = dist y z
@[simp]
theorem nndist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [] (x : P) (y : P) (z : P) :
nndist (x -ᵥ y) (x -ᵥ z) = nndist y z
@[simp]
theorem IsometryEquiv.constVSub_toFun {V : Type u_2} {P : Type u_3} [] (x : P) :
∀ (x_1 : P), x_1 = x -ᵥ x_1
@[simp]
theorem IsometryEquiv.constVSub_symm_apply {V : Type u_2} {P : Type u_3} [] (x : P) :
∀ (x_1 : V), .symm x_1 = -x_1 +ᵥ x
@[simp]
theorem IsometryEquiv.constVSub_invFun {V : Type u_2} {P : Type u_3} [] (x : P) :
∀ (x_1 : V), .invFun x_1 = -x_1 +ᵥ x
@[simp]
theorem IsometryEquiv.constVSub_apply {V : Type u_2} {P : Type u_3} [] (x : P) :
∀ (x_1 : P), x_1 = x -ᵥ x_1
def IsometryEquiv.constVSub {V : Type u_2} {P : Type u_3} [] (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.

Equations
• = { toEquiv := , isometry_toFun := }
Instances For
@[simp]
theorem dist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [] (x : P) (y : P) (z : P) :
dist (x -ᵥ z) (y -ᵥ z) = dist x y
@[simp]
theorem nndist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [] (x : P) (y : P) (z : P) :
nndist (x -ᵥ z) (y -ᵥ z) = nndist x y
theorem dist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [] (v : V) (v' : V) (p : 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} [] (v : V) (v' : V) (p : 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} [] (p₁ : P) (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} [] (p₁ : P) (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} [] (v : V) (v' : V) (p : 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} [] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :
edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) edist p₁ p₃ + edist p₂ 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.

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

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.

Equations
Instances For
theorem LipschitzWith.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [] {f : αV} {g : αP} {Kf : NNReal} {Kg : NNReal} (hf : ) (hg : ) :
LipschitzWith (Kf + Kg) (f +ᵥ g)
theorem LipschitzWith.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [] {f : αP} {g : αP} {Kf : NNReal} {Kg : NNReal} (hf : ) (hg : ) :
LipschitzWith (Kf + Kg) (f -ᵥ g)
theorem uniformContinuous_vadd {V : Type u_2} {P : Type u_3} [] :
UniformContinuous fun (x : V × P) => x.1 +ᵥ x.2
theorem uniformContinuous_vsub {V : Type u_2} {P : Type u_3} [] :
UniformContinuous fun (x : P × P) => x.1 -ᵥ x.2
@[instance 100]
instance NormedAddTorsor.to_continuousVAdd {V : Type u_2} {P : Type u_3} [] :
Equations
• =
theorem continuous_vsub {V : Type u_2} {P : Type u_3} [] :
Continuous fun (x : P × P) => x.1 -ᵥ x.2
theorem Filter.Tendsto.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [] {l : } {f : αP} {g : αP} {x : P} {y : P} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :
Filter.Tendsto (f -ᵥ g) l (nhds (x -ᵥ y))
theorem Continuous.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [] [] {f : αP} {g : αP} (hf : ) (hg : ) :
theorem ContinuousAt.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [] [] {f : αP} {g : αP} {x : α} (hf : ) (hg : ) :
theorem ContinuousWithinAt.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [] [] {f : αP} {g : αP} {x : α} {s : Set α} (hf : ) (hg : ) :
theorem ContinuousOn.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [] [] {f : αP} {g : αP} {s : Set α} (hf : ) (hg : ) :
theorem Filter.Tendsto.lineMap {α : Type u_1} {V : Type u_2} {P : Type u_3} [] {R : Type u_6} [Ring R] [] [Module R V] [] {l : } {f₁ : αP} {f₂ : αP} {g : αR} {p₁ : P} {p₂ : P} {c : R} (h₁ : Filter.Tendsto f₁ l (nhds p₁)) (h₂ : Filter.Tendsto f₂ l (nhds p₂)) (hg : Filter.Tendsto g l (nhds c)) :
Filter.Tendsto (fun (x : α) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) l (nhds (() c))
theorem Filter.Tendsto.midpoint {α : Type u_1} {V : Type u_2} {P : Type u_3} [] {R : Type u_6} [Ring R] [] [Module R V] [] [] {l : } {f₁ : αP} {f₂ : αP} {p₁ : P} {p₂ : P} (h₁ : Filter.Tendsto f₁ l (nhds p₁)) (h₂ : Filter.Tendsto f₂ l (nhds p₂)) :
Filter.Tendsto (fun (x : α) => midpoint R (f₁ x) (f₂ x)) l (nhds (midpoint R p₁ p₂))
theorem IsClosed.vadd_right_of_isCompact {V : Type u_2} {P : Type u_3} [] {s : Set V} {t : Set P} (hs : ) (ht : ) :