mathlib documentation

analysis.normed_space.add_torsor

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โ‚‚) :
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) :
โˆ€แถ  (ฮด : ๐•œ) in nhds 1, โ‡‘(affine_map.homothety x ฮด) y โˆˆ 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) :
โˆ€แถ  (ฮด : ๐•œ) in nhds 1, โ‡‘(affine_map.homothety x ฮด) '' t โŠ† 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