Documentation

Mathlib.Analysis.Normed.Affine.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_4} {Q : Type u_5} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {๐•œ : Type u_6} [NormedField ๐•œ] [NormedSpace ๐•œ W] (s : AffineSubspace ๐•œ Q) :
IsClosed โ†‘s.direction โ†” IsClosed โ†‘s
@[simp]
theorem dist_center_homothety {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [NormedField ๐•œ] [NormedSpace ๐•œ V] (pโ‚ : P) (pโ‚‚ : P) :
LipschitzWith (nndist pโ‚ pโ‚‚) โ‡‘(AffineMap.lineMap pโ‚ pโ‚‚)
@[simp]
theorem dist_lineMap_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {๐•œ : Type u_6} [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_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) (q : P) :
@[simp]
theorem dist_left_pointReflection {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) (q : P) :
theorem dist_pointReflection_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (๐•œ : Type u_6) [NormedField ๐•œ] [NormedSpace ๐•œ V] (p : P) (q : P) :
theorem dist_right_pointReflection {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (๐•œ : Type u_6) [NormedField ๐•œ] [NormedSpace ๐•œ V] (p : P) (q : P) :
theorem antilipschitzWith_lineMap {W : Type u_4} {Q : Type u_5} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {๐•œ : Type u_6} [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_4} {Q : Type u_5} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] (๐•œ : Type u_6) [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_4} {Q : Type u_5} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] (๐•œ : Type u_6) [NormedField ๐•œ] [NormedSpace ๐•œ W] (x : Q) {s : Set Q} {t : Set Q} (ht : t.Finite) (h : t โŠ† interior s) :
โˆ€แถ  (ฮด : ๐•œ) in nhds 1, โ‡‘(AffineMap.homothety x ฮด) '' t โŠ† s
theorem dist_midpoint_midpoint_le {V : Type u_2} [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_2} [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_2} {P : Type u_3} {W : Type u_4} {Q : Type u_5} [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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem DilationEquiv.smulTorsor_symm_apply {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {k : ๐•œ} (hk : k โ‰  0) :
    โˆ€ (x : P), (DilationEquiv.smulTorsor c hk).symm x = (kโปยน โ€ข fun (x : P) => x -แตฅ c) x
    @[simp]
    theorem DilationEquiv.smulTorsor_apply {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {k : ๐•œ} (hk : k โ‰  0) :
    โˆ€ (x : E), (DilationEquiv.smulTorsor c hk) x = k โ€ข x +แตฅ c
    def DilationEquiv.smulTorsor {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {k : ๐•œ} (hk : k โ‰  0) :

    Scaling by an element k of the scalar ring as a DilationEquiv with ratio โ€–kโ€–โ‚Š, mapping from a normed space to a normed torsor over that space sending 0 to c.

    Equations
    Instances For
      @[simp]
      theorem DilationEquiv.smulTorsor_ratio {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] {c : P} {k : ๐•œ} (hk : k โ‰  0) {x : E} {y : E} (h : dist x y โ‰  0) :
      @[simp]
      theorem DilationEquiv.smulTorsor_preimage_ball {๐•œ : Type u_1} {E : Type u_2} [NormedDivisionRing ๐•œ] [SeminormedAddCommGroup E] [Module ๐•œ E] [BoundedSMul ๐•œ E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] {c : P} {k : ๐•œ} (hk : k โ‰  0) :