# 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 semi_normed_add_torsor (V : out_param (Type u_1)) (P : Type u_2)  :
Type (max u_1 u_2)
• dist_eq_norm' : ∀ (x y : P), dist x y = x -ᵥ y

A semi_normed_add_torsor V P is a torsor of an additive seminormed group action by a semi_normed_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
@[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)
• dist_eq_norm' : ∀ (x y : P), dist x y = x -ᵥ y

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
@[instance]
def normed_add_torsor.to_semi_normed_add_torsor {V : Type u_1} {P : Type u_2} [normed_group V] [metric_space P] [β : P] :

A normed_add_torsor is a semi_normed_add_torsor.

Equations
@[instance]
def semi_normed_group.normed_add_torsor {V : Type u_2}  :

A semi_normed_group is a semi_normed_add_torsor over itself.

Equations
@[instance]
def normed_group.normed_add_torsor {W : Type u_4} [normed_group W] :

A normed_group is a normed_add_torsor over itself.

Equations
theorem dist_eq_norm_vsub (V : Type u_2) {P : Type u_3} (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} (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} (v₁ v₂ : V) (x : P) :
dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist 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 dist_vadd_right {V : Type u_2} {P : Type u_3} (v : V) (x : P) :
dist x (v +ᵥ x) = v
@[simp]
theorem dist_vsub_cancel_left {V : Type u_2} {P : Type u_3} (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} (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} (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} (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} (v v' : V) (p p' : P) :
nndist (v +ᵥ p) (v' +ᵥ p') v' + p'
theorem nndist_vsub_vsub_le {V : Type u_2} {P : Type u_3} (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) (p p' : P) :
edist (v +ᵥ p) (v' +ᵥ p') v' + p'
theorem edist_vsub_vsub_le {V : Type u_2} {P : Type u_3} (p₁ p₂ p₃ p₄ : P) :
edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) edist p₁ p₃ + edist p₂ p₄
def pseudo_metric_space_of_normed_group_of_add_torsor (V : Type u_1) (P : Type u_2) [ 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
def metric_space_of_normed_group_of_add_torsor (V : Type u_1) (P : Type u_2) [normed_group 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
theorem lipschitz_with.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} {f : α → V} {g : α → P} {Kf Kg : ℝ≥0} (hf : f) (hg : g) :
lipschitz_with (Kf + Kg) (f +ᵥ g)
theorem lipschitz_with.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} {f g : α → P} {Kf Kg : ℝ≥0} (hf : f) (hg : g) :
lipschitz_with (Kf + Kg) (f -ᵥ g)
theorem uniform_continuous_vadd {V : Type u_2} {P : Type u_3}  :
uniform_continuous (λ (x : V × P), x.fst +ᵥ x.snd)
theorem uniform_continuous_vsub {V : Type u_2} {P : Type u_3}  :
uniform_continuous (λ (x : P × P), x.fst -ᵥ x.snd)
theorem continuous_vadd {V : Type u_2} {P : Type u_3}  :
continuous (λ (x : V × P), x.fst +ᵥ x.snd)
theorem continuous_vsub {V : Type u_2} {P : Type u_3}  :
continuous (λ (x : P × P), x.fst -ᵥ x.snd)
theorem filter.tendsto.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} {l : filter α} {f : α → V} {g : α → P} {v : V} {p : P} (hf : (𝓝 v)) (hg : (𝓝 p)) :
filter.tendsto (f +ᵥ g) l (𝓝 (v +ᵥ p))
theorem filter.tendsto.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} {l : filter α} {f g : α → P} {x y : P} (hf : (𝓝 x)) (hg : (𝓝 y)) :
filter.tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y))
theorem continuous.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} {f : α → V} {g : α → P} (hf : continuous f) (hg : continuous g) :
theorem continuous.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} {f g : α → P} (hf : continuous f) (hg : continuous g) :
theorem continuous_at.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} {f : α → V} {g : α → P} {x : α} (hf : x) (hg : x) :
theorem continuous_at.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} {f g : α → P} {x : α} (hf : x) (hg : x) :
theorem continuous_within_at.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} {f : α → V} {g : α → P} {x : α} {s : set α} (hf : x) (hg : x) :
theorem continuous_within_at.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} {f g : α → P} {x : α} {s : set α} (hf : x) (hg : x) :
theorem filter.tendsto.line_map {α : Type u_1} {V : Type u_2} {P : Type u_3} {R : Type u_6} [ring R] [ V] [ V] {l : filter α} {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R} (h₁ : l (𝓝 p₁)) (h₂ : l (𝓝 p₂)) (hg : (𝓝 c)) :
filter.tendsto (λ (x : α), (affine_map.line_map (f₁ x) (f₂ x)) (g x)) l (𝓝 ( p₂) c))
theorem filter.tendsto.midpoint {α : Type u_1} {V : Type u_2} {P : Type u_3} {R : Type u_6} [ring R] [ V] [ V] [invertible 2] {l : filter α} {f₁ f₂ : α → P} {p₁ p₂ : P} (h₁ : l (𝓝 p₁)) (h₂ : l (𝓝 p₂)) :
filter.tendsto (λ (x : α), (f₁ x) (f₂ x)) l (𝓝 (midpoint R p₁ p₂))
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
dist p₁ ( c) p₂) = c * dist p₁ p₂
@[simp]
theorem dist_homothety_center {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
dist ( c) p₂) p₁ = c * dist p₁ p₂
@[simp]
theorem dist_homothety_self {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
dist ( c) p₂) p₂ = 1 - c * dist p₁ p₂
@[simp]
theorem dist_self_homothety {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] (p₁ p₂ : P) (c : 𝕜) :
dist p₂ ( c) p₂) = 1 - c * dist p₁ p₂
@[simp]
theorem dist_left_midpoint {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
dist p₁ (midpoint 𝕜 p₁ p₂) = 2⁻¹ * dist p₁ p₂
@[simp]
theorem dist_midpoint_left {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
dist (midpoint 𝕜 p₁ p₂) p₁ = 2⁻¹ * dist p₁ p₂
@[simp]
theorem dist_midpoint_right {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
dist (midpoint 𝕜 p₁ p₂) p₂ = 2⁻¹ * dist p₁ p₂
@[simp]
theorem dist_right_midpoint {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ : P) :
dist p₂ (midpoint 𝕜 p₁ p₂) = 2⁻¹ * dist p₁ p₂
theorem dist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_3} {𝕜 : Type u_6} [normed_field 𝕜] [ V] [invertible 2] (p₁ p₂ p₃ p₄ : P) :
dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) (dist p₁ p₃ + dist p₂ p₄) / 2
theorem dist_midpoint_midpoint_le {V : Type u_2} (p₁ p₂ p₃ p₄ : V) :
dist p₁ p₂) p₃ p₄) (dist p₁ p₃ + dist p₂ p₄) / 2
def affine_map.of_map_midpoint {V : Type u_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [normed_group W] [metric_space Q] [ Q] [ W] (f : P → Q) (h : ∀ (x y : P), f x y) = (f x) (f y)) (hfc : continuous f) :

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

Equations