mathlib documentation

analysis.normed_space.add_torsor

Torsors of normed space actions. #

This file contains lemmas about normed additive torsors over normed spaces.

@[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