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

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

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₂)

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

@[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₂

source

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‖

source

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‖₊

source

@[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

source

@[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

source

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

source

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

source

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₂)

source

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

source

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

source

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

source

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

source

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.

Instances For

Documentation

Mathlib.Analysis.NormedSpace.AddTorsor

Torsors of normed space actions. #