Documentation

Mathlib.Analysis.NormedSpace.AddTorsor

Torsors of normed space actions. #

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

theorem AffineSubspace.isClosed_direction_iff {W : Type u_2} {Q : Type u_1} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ W] (s : AffineSubspace ๐•œ Q) :
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist pโ‚ (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) = โ€–cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_center_homothety {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist pโ‚ (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) = โ€–cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_homothety_center {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) pโ‚ = โ€–cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_homothety_center {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) pโ‚ = โ€–cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_lineMap_lineMap {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (cโ‚ : ๐•œ) (cโ‚‚ : ๐•œ) :
dist (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) cโ‚) (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) cโ‚‚) = dist cโ‚ cโ‚‚ * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_lineMap_lineMap {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (cโ‚ : ๐•œ) (cโ‚‚ : ๐•œ) :
nndist (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) cโ‚) (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) cโ‚‚) = nndist cโ‚ cโ‚‚ * nndist pโ‚ pโ‚‚
theorem lipschitzWith_lineMap {V : Type u_3} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_1} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) :
LipschitzWith (nndist pโ‚ pโ‚‚) โ†‘(AffineMap.lineMap pโ‚ pโ‚‚)
@[simp]
theorem dist_lineMap_left {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) pโ‚ = โ€–cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_lineMap_left {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) pโ‚ = โ€–cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_left_lineMap {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist pโ‚ (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) = โ€–cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_left_lineMap {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist pโ‚ (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) = โ€–cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_lineMap_right {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) pโ‚‚ = โ€–1 - cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_lineMap_right {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) pโ‚‚ = โ€–1 - cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_right_lineMap {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist pโ‚‚ (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) = โ€–1 - cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_right_lineMap {V : Type u_3} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist pโ‚‚ (โ†‘(AffineMap.lineMap pโ‚ pโ‚‚) c) = โ€–1 - cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_homothety_self {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) pโ‚‚ = โ€–1 - cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_homothety_self {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) pโ‚‚ = โ€–1 - cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_self_homothety {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
dist pโ‚‚ (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) = โ€–1 - cโ€– * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_self_homothety {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) (c : ๐•œ) :
nndist pโ‚‚ (โ†‘(AffineMap.homothety pโ‚ c) pโ‚‚) = โ€–1 - cโ€–โ‚Š * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_left_midpoint {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
dist pโ‚ (midpoint ๐•œ pโ‚ pโ‚‚) = โ€–2โ€–โปยน * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_left_midpoint {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
nndist pโ‚ (midpoint ๐•œ pโ‚ pโ‚‚) = โ€–2โ€–โ‚Šโปยน * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_midpoint_left {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
dist (midpoint ๐•œ pโ‚ pโ‚‚) pโ‚ = โ€–2โ€–โปยน * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_midpoint_left {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
nndist (midpoint ๐•œ pโ‚ pโ‚‚) pโ‚ = โ€–2โ€–โ‚Šโปยน * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_midpoint_right {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
dist (midpoint ๐•œ pโ‚ pโ‚‚) pโ‚‚ = โ€–2โ€–โปยน * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_midpoint_right {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
nndist (midpoint ๐•œ pโ‚ pโ‚‚) pโ‚‚ = โ€–2โ€–โ‚Šโปยน * nndist pโ‚ pโ‚‚
@[simp]
theorem dist_right_midpoint {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
dist pโ‚‚ (midpoint ๐•œ pโ‚ pโ‚‚) = โ€–2โ€–โปยน * dist pโ‚ pโ‚‚
@[simp]
theorem nndist_right_midpoint {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) :
nndist pโ‚‚ (midpoint ๐•œ pโ‚ pโ‚‚) = โ€–2โ€–โ‚Šโปยน * nndist pโ‚ pโ‚‚
theorem dist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) (pโ‚ƒ : P) (pโ‚„ : P) :
dist (midpoint ๐•œ pโ‚ pโ‚‚) (midpoint ๐•œ pโ‚ƒ pโ‚„) โ‰ค (dist pโ‚ pโ‚ƒ + dist pโ‚‚ pโ‚„) / โ€–2โ€–
theorem nndist_midpoint_midpoint_le' {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] [Invertible 2] (pโ‚ : P) (pโ‚‚ : P) (pโ‚ƒ : P) (pโ‚„ : P) :
nndist (midpoint ๐•œ pโ‚ pโ‚‚) (midpoint ๐•œ pโ‚ƒ pโ‚„) โ‰ค (nndist pโ‚ pโ‚ƒ + nndist pโ‚‚ pโ‚„) / โ€–2โ€–โ‚Š
@[simp]
theorem dist_pointReflection_left {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) (q : P) :
dist (โ†‘(Equiv.pointReflection p) q) p = dist p q
@[simp]
theorem dist_left_pointReflection {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) (q : P) :
dist p (โ†‘(Equiv.pointReflection p) q) = dist p q
@[simp]
theorem dist_pointReflection_right {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (p : P) (q : P) :
@[simp]
theorem dist_right_pointReflection {V : Type u_2} {P : Type u_1} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_3} [NormedField ๐•œ] [NormedSpace ๐•œ V] (p : P) (q : P) :
theorem antilipschitzWith_lineMap {W : Type u_3} {Q : Type u_1} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {๐•œ : Type u_2} [NormedField ๐•œ] [NormedSpace ๐•œ W] {pโ‚ : Q} {pโ‚‚ : Q} (h : pโ‚ โ‰  pโ‚‚) :
AntilipschitzWith (nndist pโ‚ pโ‚‚)โปยน โ†‘(AffineMap.lineMap pโ‚ pโ‚‚)
theorem eventually_homothety_mem_of_mem_interior {W : Type u_3} {Q : Type u_1} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] (๐•œ : Type u_2) [NormedField ๐•œ] [NormedSpace ๐•œ W] (x : Q) {s : Set Q} {y : Q} (hy : y โˆˆ interior s) :
โˆ€แถ  (ฮด : ๐•œ) in nhds 1, โ†‘(AffineMap.homothety x ฮด) y โˆˆ s
theorem eventually_homothety_image_subset_of_finite_subset_interior {W : Type u_3} {Q : Type u_1} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] (๐•œ : Type u_2) [NormedField ๐•œ] [NormedSpace ๐•œ W] (x : Q) {s : Set Q} {t : Set Q} (ht : Set.Finite t) (h : t โŠ† interior s) :
โˆ€แถ  (ฮด : ๐•œ) in nhds 1, โ†‘(AffineMap.homothety x ฮด) '' t โŠ† s
theorem dist_midpoint_midpoint_le {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace โ„ V] (pโ‚ : V) (pโ‚‚ : V) (pโ‚ƒ : V) (pโ‚„ : V) :
dist (midpoint โ„ pโ‚ pโ‚‚) (midpoint โ„ pโ‚ƒ pโ‚„) โ‰ค (dist pโ‚ pโ‚ƒ + dist pโ‚‚ pโ‚„) / 2
theorem nndist_midpoint_midpoint_le {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace โ„ V] (pโ‚ : V) (pโ‚‚ : V) (pโ‚ƒ : V) (pโ‚„ : V) :
nndist (midpoint โ„ pโ‚ pโ‚‚) (midpoint โ„ pโ‚ƒ pโ‚„) โ‰ค (nndist pโ‚ pโ‚ƒ + nndist pโ‚‚ pโ‚„) / 2
def AffineMap.ofMapMidpoint {V : Type u_1} {P : Type u_2} {W : Type u_3} {Q : Type u_4} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] [NormedSpace โ„ V] [NormedSpace โ„ 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.

Instances For