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 ↑(AffineSubspace.direction s) ↔ 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) : dist ((Equiv.pointReflection p) q) p = dist p q

@[simp]

theorem dist_left_pointReflection {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p : P) (q : P) : dist p ((Equiv.pointReflection p) q) = dist p q

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) : dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q

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) : dist q ((Equiv.pointReflection p) q) = ‖2‖ * dist p q

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 : Set.Finite t) (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) : P →ᵃ[ℝ] Q

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.

@[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.symm (DilationEquiv.smulTorsor c hk)) 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) : 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.

Equations

• DilationEquiv.smulTorsor c hk = { toEquiv := { toFun := fun (x : E) => k • x +ᵥ c, invFun := k⁻¹ • fun (x : P) => x -ᵥ c, left_inv := ⋯, right_inv := ⋯ }, edist_eq' := ⋯ }

@[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) : Dilation.ratio (DilationEquiv.smulTorsor c hk) = ‖k‖₊

@[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) : ⇑(DilationEquiv.smulTorsor c hk) ⁻¹' Metric.ball c ‖k‖ = Metric.ball 0 1