Torsors of additive normed group actions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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)
- to_add_torsor : add_torsor V P
- dist_eq_norm' : ∀ (x y : P), has_dist.dist x y = ‖x -ᵥ y‖
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
@[protected, instance]
def
normed_add_torsor.to_add_torsor'
{V : Type u_1}
{P : Type u_2}
[normed_add_comm_group V]
[metric_space P]
[normed_add_torsor V P] :
add_torsor V P
Shortcut instance to help typeclass inference out.
@[protected, instance]
def
normed_add_torsor.to_has_isometric_vadd
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
@[protected, instance]
A seminormed_add_comm_group is a normed_add_torsor over itself.
@[protected, nolint, instance]
def
affine_subspace.to_normed_add_torsor
{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_1}
[ring R]
[module R V]
(s : affine_subspace R P)
[nonempty ↥s] :
normed_add_torsor ↥(s.direction) ↥s
A nonempty affine subspace of a normed_add_torsor is itself a normed_add_torsor.
Equations
- s.to_normed_add_torsor = {to_add_torsor := {to_add_action := add_torsor.to_add_action s.to_add_torsor, to_has_vsub := add_torsor.to_has_vsub s.to_add_torsor, nonempty := _, vsub_vadd' := _, vadd_vsub' := _}, dist_eq_norm' := _}
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) :
has_dist.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}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x y : P) :
has_nndist.nndist x y = ‖x -ᵥ y‖₊
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) :
has_dist.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}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x y : P) :
has_nndist.nndist x y = ‖y -ᵥ x‖₊
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) :
has_dist.dist (v +ᵥ x) (v +ᵥ y) = has_dist.dist x y
@[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
nndist_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_nndist.nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = has_nndist.nndist 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) :
has_dist.dist (v +ᵥ x) x = ‖v‖
@[simp]
theorem
nndist_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) :
has_nndist.nndist (v +ᵥ x) x = ‖v‖₊
@[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) :
has_dist.dist x (v +ᵥ x) = ‖v‖
@[simp]
theorem
nndist_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) :
has_nndist.nndist x (v +ᵥ x) = ‖v‖₊
def
isometry_equiv.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
- isometry_equiv.vadd_const x = {to_equiv := equiv.vadd_const x, isometry_to_fun := _}
@[simp]
theorem
isometry_equiv.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) :
⇑((isometry_equiv.vadd_const x).symm) p' = p' -ᵥ x
@[simp]
theorem
isometry_equiv.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) :
⇑(isometry_equiv.vadd_const x) v = v +ᵥ x
@[simp]
theorem
isometry_equiv.vadd_const_to_equiv
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x : 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) :
has_dist.dist (x -ᵥ y) (x -ᵥ z) = has_dist.dist y z
@[simp]
theorem
isometry_equiv.const_vsub_to_equiv
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
(x : P) :
@[simp]
theorem
isometry_equiv.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) :
def
isometry_equiv.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
- isometry_equiv.const_vsub x = {to_equiv := equiv.const_vsub x, isometry_to_fun := _}
@[simp]
theorem
isometry_equiv.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) :
⇑(isometry_equiv.const_vsub x) ᾰ = x -ᵥ ᾰ
@[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) :
has_dist.dist (x -ᵥ z) (y -ᵥ z) = has_dist.dist x y
@[simp]
theorem
nndist_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) :
has_nndist.nndist (x -ᵥ z) (y -ᵥ z) = has_nndist.nndist x y
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) :
has_dist.dist (v +ᵥ p) (v' +ᵥ p') ≤ has_dist.dist v v' + 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) :
has_nndist.nndist (v +ᵥ p) (v' +ᵥ p') ≤ has_nndist.nndist v v' + has_nndist.nndist 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_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) :
has_edist.edist (v +ᵥ p) (v' +ᵥ p') ≤ has_edist.edist v v' + has_edist.edist 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₄
def
pseudo_metric_space_of_normed_add_comm_group_of_add_torsor
(V : Type u_1)
(P : Type u_2)
[seminormed_add_comm_group V]
[add_torsor V 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
- pseudo_metric_space_of_normed_add_comm_group_of_add_torsor V P = {to_has_dist := {dist := λ (x y : P), ‖x -ᵥ y‖}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : P), ↑⟨(λ (x y : P), ‖x -ᵥ y‖) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : P), ‖x -ᵥ y‖) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : P), ‖x -ᵥ y‖) _ _ _, cobounded_sets := _}
def
metric_space_of_normed_add_comm_group_of_add_torsor
(V : Type u_1)
(P : Type u_2)
[normed_add_comm_group V]
[add_torsor 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
- metric_space_of_normed_add_comm_group_of_add_torsor V P = {to_pseudo_metric_space := {to_has_dist := {dist := λ (x y : P), ‖x -ᵥ y‖}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : P), ↑⟨(λ (x y : P), ‖x -ᵥ y‖) x y, _⟩, edist_dist := _, to_uniform_space := uniform_space_of_dist (λ (x y : P), ‖x -ᵥ y‖) _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : P), ‖x -ᵥ y‖) _ _ _, cobounded_sets := _}, eq_of_dist_eq_zero := _}
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]
def
normed_add_torsor.to_has_continuous_vadd
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P] :
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) :
continuous (f -ᵥ 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) :
continuous_at (f -ᵥ 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) :
continuous_within_at (f -ᵥ 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₂))