Torsors of normed space actions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
nndist_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_nndist.nndist p₁ (⇑(affine_map.homothety p₁ c) p₂) = ‖c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist (⇑(affine_map.homothety p₁ c) p₂) p₁ = ‖c‖₊ * has_nndist.nndist 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₂
@[simp]
theorem
nndist_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_nndist.nndist (⇑(affine_map.line_map p₁ p₂) c₁) (⇑(affine_map.line_map p₁ p₂) c₂) = has_nndist.nndist c₁ c₂ * has_nndist.nndist 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
nndist_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_nndist.nndist (⇑(affine_map.line_map p₁ p₂) c) p₁ = ‖c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist p₁ (⇑(affine_map.line_map p₁ p₂) c) = ‖c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist (⇑(affine_map.line_map p₁ p₂) c) p₂ = ‖1 - c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist p₂ (⇑(affine_map.line_map p₁ p₂) c) = ‖1 - c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist (⇑(affine_map.homothety p₁ c) p₂) p₂ = ‖1 - c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist p₂ (⇑(affine_map.homothety p₁ c) p₂) = ‖1 - c‖₊ * has_nndist.nndist 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
nndist_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_nndist.nndist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * has_nndist.nndist 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
nndist_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_nndist.nndist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖₊⁻¹ * has_nndist.nndist 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
nndist_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_nndist.nndist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖₊⁻¹ * has_nndist.nndist 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₂
@[simp]
theorem
nndist_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_nndist.nndist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * has_nndist.nndist 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
nndist_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_nndist.nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (has_nndist.nndist p₁ p₃ + has_nndist.nndist 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
theorem
nndist_midpoint_midpoint_le
{V : Type u_2}
[seminormed_add_comm_group V]
[normed_space ℝ V]
(p₁ p₂ p₃ p₄ : V) :
has_nndist.nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (has_nndist.nndist p₁ p₃ + has_nndist.nndist 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) _