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) : IsClosed ↑(AffineSubspace.direction s) ↔ IsClosed ↑s

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

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

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