mathlib documentation

analysis.normed_space.add_torsor

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]
structure normed_add_torsor (V : out_param (Type u_1)) (P : Type u_2) [out_param (normed_group V)] [metric_space P] :
Type (max u_1 u_2)

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

Instances
theorem dist_eq_norm_vsub (V : Type u_2) {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor 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.

@[simp]
theorem dist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (v : V) (x y : P) :
dist (v +ᵥ x) (v +ᵥ y) = dist x y

@[simp]
theorem dist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (v₁ v₂ : V) (x : P) :
dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂

@[simp]
theorem dist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (x y z : P) :
dist (x -ᵥ y) (x -ᵥ z) = dist y z

@[simp]
theorem dist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (x y z : P) :
dist (x -ᵥ z) (y -ᵥ z) = dist x y

theorem dist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (v v' : V) (p p' : P) :
dist (v +ᵥ p) (v' +ᵥ p') dist v v' + dist p p'

theorem dist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (p₁ p₂ p₃ p₄ : P) :
dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) dist p₁ p₃ + dist p₂ p₄

theorem nndist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (v v' : V) (p p' : P) :
nndist (v +ᵥ p) (v' +ᵥ p') nndist v v' + nndist p p'

theorem nndist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor 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} [normed_group V] [metric_space P] [normed_add_torsor 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} [normed_group V] [metric_space P] [normed_add_torsor V P] (p₁ p₂ p₃ p₄ : P) :
edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) edist p₁ p₃ + edist p₂ p₄

def metric_space_of_normed_group_of_add_torsor (V : Type u_1) (P : Type u_2) [normed_group V] [affine_space V P] :

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

Equations
def isometric.vadd_const {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
P → V ≃ᵢ P

The map v ↦ v +ᵥ p as an isometric equivalence between V and P.

Equations
@[simp]
theorem isometric.coe_vadd_const {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (p : P) :
(isometric.vadd_const p) = λ (v : V), v +ᵥ p

@[simp]
theorem isometric.coe_vadd_const_symm {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (p : P) :
((isometric.vadd_const p).symm) = λ (p' : P), p' -ᵥ p

@[simp]
theorem isometric.vadd_const_to_equiv {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (p : P) :

def isometric.const_vsub {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
P → P ≃ᵢ V

p' ↦ p -ᵥ p' as an equivalence.

Equations
@[simp]
theorem isometric.coe_const_vsub {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (p : P) :

@[simp]
theorem isometric.coe_const_vsub_symm {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (p : P) :
((isometric.const_vsub p).symm) = λ (v : V), -v +ᵥ p

def isometric.const_vadd {V : Type u_2} (P : Type u_3) [normed_group V] [metric_space P] [normed_add_torsor V P] :
V → P ≃ᵢ P

The map p ↦ v +ᵥ p as an isometric automorphism of P.

Equations
@[simp]
theorem isometric.coe_const_vadd {V : Type u_2} (P : Type u_3) [normed_group V] [metric_space P] [normed_add_torsor V P] (v : V) :

@[simp]
theorem isometric.const_vadd_zero (V : Type u_2) (P : Type u_3) [normed_group V] [metric_space P] [normed_add_torsor V P] :

def isometric.point_reflection {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
P → P ≃ᵢ P

Point reflection in x as an isometric homeomorphism.

Equations
theorem isometric.point_reflection_apply {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (x y : P) :

@[simp]
theorem isometric.point_reflection_self {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (x : P) :

@[simp]
theorem isometric.dist_point_reflection_fixed {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (x y : P) :

theorem isometric.dist_point_reflection_self' {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (x y : P) :

theorem isometric.dist_point_reflection_self {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (𝕜 : Type u_1) [normed_field 𝕜] [normed_space 𝕜 V] (x y : P) :

theorem isometric.point_reflection_fixed_iff {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] (𝕜 : Type u_1) [normed_field 𝕜] [normed_space 𝕜 V] [invertible 2] {x y : P} :

theorem isometric.dist_point_reflection_self_real {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [normed_space V] (x y : P) :

@[simp]
theorem isometric.point_reflection_midpoint_left {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [normed_space V] (x y : P) :

@[simp]
theorem isometric.point_reflection_midpoint_right {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [normed_space V] (x y : P) :

theorem lipschitz_with.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [emetric_space α] {f : α → V} {g : α → P} {Kf Kg : ℝ≥0} :
lipschitz_with Kf flipschitz_with Kg glipschitz_with (Kf + Kg) (f +ᵥ g)

theorem lipschitz_with.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [emetric_space α] {f g : α → P} {Kf Kg : ℝ≥0} :
lipschitz_with Kf flipschitz_with Kg glipschitz_with (Kf + Kg) (f -ᵥ g)

theorem uniform_continuous_vadd {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
uniform_continuous (λ (x : V × P), x.fst +ᵥ x.snd)

theorem uniform_continuous_vsub {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
uniform_continuous (λ (x : P × P), x.fst -ᵥ x.snd)

theorem continuous_vadd {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
continuous (λ (x : V × P), x.fst +ᵥ x.snd)

theorem continuous_vsub {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] :
continuous (λ (x : P × P), x.fst -ᵥ x.snd)

theorem filter.tendsto.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] {l : filter α} {f : α → V} {g : α → P} {v : V} {p : P} :
filter.tendsto f l (𝓝 v)filter.tendsto g l (𝓝 p)filter.tendsto (f +ᵥ g) l (𝓝 (v +ᵥ p))

theorem filter.tendsto.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] {l : filter α} {f g : α → P} {x y : P} :
filter.tendsto f l (𝓝 x)filter.tendsto g l (𝓝 y)filter.tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y))

theorem continuous.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [topological_space α] {f : α → V} {g : α → P} :

theorem continuous.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [topological_space α] {f g : α → P} :

theorem continuous_at.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [topological_space α] {f : α → V} {g : α → P} {x : α} :

theorem continuous_at.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [topological_space α] {f g : α → P} {x : α} :

theorem continuous_within_at.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [topological_space α] {f : α → V} {g : α → P} {x : α} {s : set α} :

theorem continuous_within_at.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] [topological_space α] {f g : α → P} {x : α} {s : set α} :

theorem isometry.vadd_vsub {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] {V' : Type u_4} {P' : Type u_5} [normed_group V'] [metric_space P'] [normed_add_torsor V' P'] {f : P → P'} (hf : isometry f) {p : P} {g : V → V'} :
(∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p)isometry g

The map g from V1 to V2 corresponding to a map f from P1 to P2, at a base point p, is an isometry if f is one.

def affine_map.of_map_midpoint {V : Type u_2} {P : Type u_3} [normed_group V] [metric_space P] [normed_add_torsor V P] {V' : Type u_4} {P' : Type u_5} [normed_group V'] [metric_space P'] [normed_add_torsor V' P'] [normed_space V] [normed_space V'] (f : P → P') :
(∀ (x y : P), f (midpoint x y) = midpoint (f x) (f y))continuous f(P →ᵃ[] P')

A continuous map between two normed affine spaces is an affine map provided that it sends midpoints to midpoints.

Equations