Torsors of normed space actions. #

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

@[simp]

theorem dist_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ p : P) (c : 𝕜) :

dist ((AffineMap.homothety p c) p₁) ((AffineMap.homothety p c) p₂) = ‖c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ p : P) (c : 𝕜) :

nndist ((AffineMap.homothety p c) p₁) ((AffineMap.homothety p c) p₂) = ‖c‖₊ * nndist p₁ p₂

source

theorem lipschitzWith_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p : P) (c : 𝕜) :

LipschitzWith ‖c‖₊ ⇑(AffineMap.homothety p c)

source

@[simp]

theorem dist_center_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist p₁ ((AffineMap.homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_center_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist p₁ ((AffineMap.homothety p₁ c) p₂) = ‖c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_homothety_center {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist ((AffineMap.homothety p₁ c) p₂) p₁ = ‖c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_homothety_center {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist ((AffineMap.homothety p₁ c) p₂) p₁ = ‖c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_lineMap_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c₁ c₂ : 𝕜) :

dist ((AffineMap.lineMap p₁ p₂) c₁) ((AffineMap.lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂

source

@[simp]

theorem nndist_lineMap_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c₁ c₂ : 𝕜) :

nndist ((AffineMap.lineMap p₁ p₂) c₁) ((AffineMap.lineMap p₁ p₂) c₂) = nndist c₁ c₂ * nndist p₁ p₂

source

theorem lipschitzWith_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) :

LipschitzWith (nndist p₁ p₂) ⇑(AffineMap.lineMap p₁ p₂)

source

@[simp]

theorem dist_lineMap_left {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist ((AffineMap.lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_lineMap_left {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist ((AffineMap.lineMap p₁ p₂) c) p₁ = ‖c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_left_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist p₁ ((AffineMap.lineMap p₁ p₂) c) = ‖c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_left_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist p₁ ((AffineMap.lineMap p₁ p₂) c) = ‖c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_lineMap_right {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist ((AffineMap.lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_lineMap_right {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist ((AffineMap.lineMap p₁ p₂) c) p₂ = ‖1 - c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_right_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist p₂ ((AffineMap.lineMap p₁ p₂) c) = ‖1 - c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_right_lineMap {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist p₂ ((AffineMap.lineMap p₁ p₂) c) = ‖1 - c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_homothety_self {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist ((AffineMap.homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_homothety_self {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist ((AffineMap.homothety p₁ c) p₂) p₂ = ‖1 - c‖₊ * nndist p₁ p₂

source

@[simp]

theorem dist_self_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

dist p₂ ((AffineMap.homothety p₁ c) p₂) = ‖1 - c‖ * dist p₁ p₂

source

@[simp]

theorem nndist_self_homothety {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p₁ p₂ : P) (c : 𝕜) :

nndist p₂ ((AffineMap.homothety p₁ c) p₂) = ‖1 - c‖₊ * nndist p₁ p₂

source

theorem Metric.image_homothety_ball {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p c : P) (r : ℝ) {x : 𝕜} (hx : x ≠ 0) :

⇑(AffineMap.homothety c x) '' ball p r = ball ((AffineMap.homothety c x) p) (‖x‖ * r)

source

theorem Metric.image_homothety_closedBall {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p c : P) (r : ℝ) {x : 𝕜} (hx : x ≠ 0) :

⇑(AffineMap.homothety c x) '' closedBall p r = closedBall ((AffineMap.homothety c x) p) (‖x‖ * r)

source

theorem Metric.image_homothety_closedBall_of_nonneg {W : Type u_3} {Q : Type u_4} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 W] (p c : Q) {r : ℝ} (hr : 0 ≤ r) (x : 𝕜) :

⇑(AffineMap.homothety c x) '' closedBall p r = closedBall ((AffineMap.homothety c x) p) (‖x‖ * r)

source

theorem Metric.image_homothety_sphere {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] (p c : P) (r : ℝ) {x : 𝕜} (hx : x ≠ 0) :

⇑(AffineMap.homothety c x) '' sphere p r = sphere ((AffineMap.homothety c x) p) (‖x‖ * r)

source

theorem Metric.image_homothety_sphere_of_nonneg {W : Type u_3} {Q : Type u_4} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 W] [NormedSpace ℝ W] [Nontrivial W] (p c : Q) {r : ℝ} (hr : 0 ≤ r) (x : 𝕜) :

⇑(AffineMap.homothety c x) '' sphere p r = sphere ((AffineMap.homothety c x) p) (‖x‖ * r)

source

@[simp]

theorem dist_left_midpoint {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

dist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

source

@[simp]

theorem nndist_left_midpoint {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

nndist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * nndist p₁ p₂

source

@[simp]

theorem dist_midpoint_left {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂

source

@[simp]

theorem nndist_midpoint_left {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

nndist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖₊⁻¹ * nndist p₁ p₂

source

@[simp]

theorem dist_midpoint_right {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂

source

@[simp]

theorem nndist_midpoint_right {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

nndist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖₊⁻¹ * nndist p₁ p₂

source

@[simp]

theorem dist_right_midpoint {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

dist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

source

@[simp]

theorem nndist_right_midpoint {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

nndist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * nndist p₁ p₂

source

theorem dist_left_midpoint_eq_dist_right_midpoint {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ : P) :

dist p₁ (midpoint 𝕜 p₁ p₂) = dist p₂ (midpoint 𝕜 p₁ p₂)

The midpoint of the segment AB is the same distance from A as it is from B.

source

theorem dist_midpoint_midpoint_le' {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ p₃ p₄ : P) :

dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖

source

theorem nndist_midpoint_midpoint_le' {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 V] [Invertible 2] (p₁ p₂ p₃ p₄ : P) :

nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / ‖2‖₊

source

@[simp]

theorem dist_pointReflection_left {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p q : P) :

dist ((Equiv.pointReflection p) q) p = dist p q

source

@[simp]

theorem dist_left_pointReflection {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p q : P) :

dist p ((Equiv.pointReflection p) q) = dist p q

source

theorem dist_pointReflection_right {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 V] (p q : P) :

dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q

source

theorem dist_right_pointReflection {V : Type u_1} {P : Type u_2} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (𝕜 : Type u_5) [NormedField 𝕜] [NormedSpace 𝕜 V] (p q : P) :

dist q ((Equiv.pointReflection p) q) = ‖2‖ * dist p q

source

theorem antilipschitzWith_lineMap {W : Type u_3} {Q : Type u_4} [NormedAddCommGroup W] [MetricSpace Q] [NormedAddTorsor W Q] {𝕜 : Type u_5} [NormedField 𝕜] [NormedSpace 𝕜 W] {p₁ p₂ : Q} (h : p₁ ≠ p₂) :

AntilipschitzWith (nndist p₁ p₂)⁻¹ ⇑(AffineMap.lineMap p₁ p₂)

source

theorem dist_midpoint_midpoint_le {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] (p₁ p₂ p₃ p₄ : V) :

dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2

source

theorem nndist_midpoint_midpoint_le {V : Type u_1} [SeminormedAddCommGroup V] [NormedSpace ℝ V] (p₁ p₂ p₃ p₄ : V) :

nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / 2

source

noncomputable 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) :

P →ᵃ[ℝ ] Q

A continuous map between two normed affine spaces is an affine map provided that it sends midpoints to midpoints.

Instances For

source

def DilationEquiv.smulTorsor {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {k : 𝕜} (hk : k ≠ 0) :

E ≃ᵈ P

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.

Instances For

source

@[simp]

theorem DilationEquiv.smulTorsor_apply {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {k : 𝕜} (hk : k ≠ 0) (x✝ : E) :

(smulTorsor c hk) x✝ = k • x✝ +ᵥ c

source

@[simp]

theorem DilationEquiv.smulTorsor_symm_apply {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] (c : P) {k : 𝕜} (hk : k ≠ 0) (x✝ : P) :

(smulTorsor c hk).symm x✝ = (k⁻¹ • fun (x : P) => x -ᵥ c) x✝

source

theorem DilationEquiv.smulTorsor_ratio {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] {c : P} {k : 𝕜} (hk : k ≠ 0) {x y : E} (h : dist x y ≠ 0) :

Dilation.ratio (smulTorsor c hk) = ‖k‖₊

source

@[simp]

theorem DilationEquiv.smulTorsor_preimage_ball {𝕜 : Type u_1} {E : Type u_2} [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [NormSMulClass 𝕜 E] {P : Type u_3} [PseudoMetricSpace P] [NormedAddTorsor E P] {c : P} {k : 𝕜} (hk : k ≠ 0) :

⇑(smulTorsor c hk) ⁻¹' Metric.ball c ‖k‖ = Metric.ball 0 1

Documentation

Mathlib.Analysis.Normed.Affine.AddTorsor

Torsors of normed space actions. #