Torsors of normed space actions. #
This file contains lemmas about normed additive torsors over normed spaces.
theorem
affine_subspace.is_closed_direction_iff
{W : Type u_4}
{Q : Type u_5}
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ W]
(s : affine_subspace ๐ Q) :
@[simp]
theorem
dist_center_homothety
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist pโ (โ(affine_map.homothety pโ c) pโ) = โcโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_homothety_center
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist (โ(affine_map.homothety pโ c) pโ) pโ = โcโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_line_map_line_map
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(cโ cโ : ๐) :
has_dist.dist (โ(affine_map.line_map pโ pโ) cโ) (โ(affine_map.line_map pโ pโ) cโ) = has_dist.dist cโ cโ * has_dist.dist pโ pโ
theorem
lipschitz_with_line_map
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P) :
lipschitz_with (has_nndist.nndist pโ pโ) โ(affine_map.line_map pโ pโ)
@[simp]
theorem
dist_line_map_left
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist (โ(affine_map.line_map pโ pโ) c) pโ = โcโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_left_line_map
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist pโ (โ(affine_map.line_map pโ pโ) c) = โcโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_line_map_right
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist (โ(affine_map.line_map pโ pโ) c) pโ = โ1 - cโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_right_line_map
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist pโ (โ(affine_map.line_map pโ pโ) c) = โ1 - cโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_homothety_self
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist (โ(affine_map.homothety pโ c) pโ) pโ = โ1 - cโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_self_homothety
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
(pโ pโ : P)
(c : ๐) :
has_dist.dist pโ (โ(affine_map.homothety pโ c) pโ) = โ1 - cโ * has_dist.dist pโ pโ
@[simp]
theorem
dist_left_midpoint
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
[invertible 2]
(pโ pโ : P) :
has_dist.dist pโ (midpoint ๐ pโ pโ) = โ2โโปยน * has_dist.dist pโ pโ
@[simp]
theorem
dist_midpoint_left
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
[invertible 2]
(pโ pโ : P) :
has_dist.dist (midpoint ๐ pโ pโ) pโ = โ2โโปยน * has_dist.dist pโ pโ
@[simp]
theorem
dist_midpoint_right
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
[invertible 2]
(pโ pโ : P) :
has_dist.dist (midpoint ๐ pโ pโ) pโ = โ2โโปยน * has_dist.dist pโ pโ
@[simp]
theorem
dist_right_midpoint
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
[invertible 2]
(pโ pโ : P) :
has_dist.dist pโ (midpoint ๐ pโ pโ) = โ2โโปยน * has_dist.dist pโ pโ
theorem
dist_midpoint_midpoint_le'
{V : Type u_2}
{P : Type u_3}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ V]
[invertible 2]
(pโ pโ pโ pโ : P) :
has_dist.dist (midpoint ๐ pโ pโ) (midpoint ๐ pโ pโ) โค (has_dist.dist pโ pโ + has_dist.dist pโ pโ) / โ2โ
theorem
antilipschitz_with_line_map
{W : Type u_4}
{Q : Type u_5}
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
{๐ : Type u_6}
[normed_field ๐]
[normed_space ๐ W]
{pโ pโ : Q}
(h : pโ โ pโ) :
antilipschitz_with (has_nndist.nndist pโ pโ)โปยน โ(affine_map.line_map pโ pโ)
theorem
eventually_homothety_mem_of_mem_interior
{W : Type u_4}
{Q : Type u_5}
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
(๐ : Type u_6)
[normed_field ๐]
[normed_space ๐ W]
(x : Q)
{s : set Q}
{y : Q}
(hy : y โ interior s) :
theorem
eventually_homothety_image_subset_of_finite_subset_interior
{W : Type u_4}
{Q : Type u_5}
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
(๐ : Type u_6)
[normed_field ๐]
[normed_space ๐ W]
(x : Q)
{s t : set Q}
(ht : t.finite)
(h : t โ interior s) :
theorem
dist_midpoint_midpoint_le
{V : Type u_2}
[seminormed_add_comm_group V]
[normed_space โ V]
(pโ pโ pโ pโ : V) :
has_dist.dist (midpoint โ pโ pโ) (midpoint โ pโ pโ) โค (has_dist.dist pโ pโ + has_dist.dist pโ pโ) / 2
noncomputable
def
affine_map.of_map_midpoint
{V : Type u_2}
{P : Type u_3}
{W : Type u_4}
{Q : Type u_5}
[seminormed_add_comm_group V]
[pseudo_metric_space P]
[normed_add_torsor V P]
[normed_add_comm_group W]
[metric_space Q]
[normed_add_torsor W Q]
[normed_space โ V]
[normed_space โ W]
(f : P โ Q)
(h : โ (x y : P), f (midpoint โ x y) = midpoint โ (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
- affine_map.of_map_midpoint f h hfc = affine_map.mk' f โ((add_monoid_hom.of_map_midpoint โ โ (โ((affine_equiv.vadd_const โ (f (classical.arbitrary P))).symm) โ f โ โ(affine_equiv.vadd_const โ (classical.arbitrary P))) _ _).to_real_linear_map _) (classical.arbitrary P) _