mathlib documentation

analysis.normed.group.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 (seminormed_add_comm_group V)] [pseudo_metric_space P] :
Type (max u_1 u_2)

A normed_add_torsor V P is a torsor of an additive seminormed group action by a seminormed_add_comm_group 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).

Instances of this typeclass
Instances of other typeclasses for normed_add_torsor
  • normed_add_torsor.has_sizeof_inst
theorem dist_eq_norm_vsub (V : Type u_2) {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x y : P) :

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 dist_eq_norm_vsub' (V : Type u_2) {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x y : P) :

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} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v : V) (x y : P) :
@[simp]
theorem dist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v₁ v₂ : V) (x : P) :
has_dist.dist (v₁ +ᵥ x) (v₂ +ᵥ x) = has_dist.dist v₁ v₂
@[simp]
theorem dist_vadd_left {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v : V) (x : P) :
@[simp]
theorem dist_vadd_right {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v : V) (x : P) :
def isometric.vadd_const {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor 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.

Equations
@[simp]
theorem isometric.vadd_const_apply {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : P) (v : V) :
@[simp]
theorem isometric.vadd_const_symm_apply {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x p' : P) :
@[simp]
theorem isometric.const_vadd_symm_apply {V : Type u_2} (P : Type u_3) [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : V) (ᾰ : P) :
def isometric.const_vadd {V : Type u_2} (P : Type u_3) [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : V) :
P ≃ᵢ P

Self-isometry of a (semi)normed add torsor given by addition of a constant vector x.

Equations
@[simp]
theorem isometric.const_vadd_apply {V : Type u_2} (P : Type u_3) [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : V) (ᾰ : P) :
@[simp]
theorem dist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x y z : P) :
@[simp]
theorem isometric.const_vsub_symm_apply {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : P) (v : V) :
@[simp]
theorem isometric.const_vsub_apply {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x ᾰ : P) :
def isometric.const_vsub {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor 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.

Equations
@[simp]
theorem dist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x y z : P) :
@[simp]
theorem vadd_ball {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : V) (y : P) (r : ) :
@[simp]
theorem vadd_closed_ball {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : V) (y : P) (r : ) :
@[simp]
theorem vadd_sphere {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (x : V) (y : P) (r : ) :
theorem dist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v v' : V) (p p' : P) :
theorem dist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (p₁ p₂ p₃ p₄ : P) :
has_dist.dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) has_dist.dist p₁ p₃ + has_dist.dist p₂ p₄
theorem nndist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v v' : V) (p p' : P) :
theorem nndist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (p₁ p₂ p₃ p₄ : P) :
has_nndist.nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) has_nndist.nndist p₁ p₃ + has_nndist.nndist p₂ p₄
theorem edist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (v v' : V) (p p' : P) :
theorem edist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] (p₁ p₂ p₃ p₄ : P) :
has_edist.edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) has_edist.edist p₁ p₃ + has_edist.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 metric_space P.

Equations

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
theorem lipschitz_with.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [pseudo_emetric_space α] {f : α → V} {g : α → P} {Kf Kg : nnreal} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (f +ᵥ g)
theorem lipschitz_with.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [pseudo_emetric_space α] {f g : α → P} {Kf Kg : nnreal} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
lipschitz_with (Kf + Kg) (f -ᵥ g)
theorem uniform_continuous_vadd {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_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} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] :
uniform_continuous (λ (x : P × P), x.fst -ᵥ x.snd)
@[protected, instance]
theorem continuous_vsub {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] :
continuous (λ (x : P × P), x.fst -ᵥ x.snd)
theorem filter.tendsto.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] {l : filter α} {f g : α → P} {x 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} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [topological_space α] {f g : α → P} (hf : continuous f) (hg : continuous g) :
theorem continuous_at.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [topological_space α] {f g : α → P} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) :
theorem continuous_within_at.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] [topological_space α] {f g : α → P} {x : α} {s : set α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
theorem filter.tendsto.line_map {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] {R : Type u_6} [ring R] [topological_space R] [module R V] [has_continuous_smul R V] {l : filter α} {f₁ f₂ : α → P} {g : α → R} {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 (λ (x : α), (affine_map.line_map (f₁ x) (f₂ x)) (g x)) l (nhds ((affine_map.line_map p₁ p₂) c))
theorem filter.tendsto.midpoint {α : Type u_1} {V : Type u_2} {P : Type u_3} [seminormed_add_comm_group V] [pseudo_metric_space P] [normed_add_torsor V P] {R : Type u_6} [ring R] [topological_space R] [module R V] [has_continuous_smul R V] [invertible 2] {l : filter α} {f₁ f₂ : α → P} {p₁ p₂ : P} (h₁ : filter.tendsto f₁ l (nhds p₁)) (h₂ : filter.tendsto f₂ l (nhds p₂)) :
filter.tendsto (λ (x : α), midpoint R (f₁ x) (f₂ x)) l (nhds (midpoint R p₁ p₂))