Module docstring
{"# Torsors of additive normed group actions.
This file defines torsors of additive normed group actions, with a metric space structure. The motivating case is Euclidean affine spaces. "}
NormedAddTorsor
structure
(V : outParam Type*) (P : Type*) [SeminormedAddCommGroup V]
[PseudoMetricSpace P] extends AddTorsor V P
Full source
/-- A `NormedAddTorsor V P` is a torsor of an additive seminormed group
action by a `SeminormedAddCommGroup V` on points `P`. We bundle the pseudometric space
structure and require the distance to be the same as results from the
norm (which in fact implies the distance yields a pseudometric space, but
bundling just the distance and using an instance for the pseudometric space
results in type class problems). -/
class NormedAddTorsor (V : outParam Type*) (P : Type*) [SeminormedAddCommGroup V]
[PseudoMetricSpace P] extends AddTorsor V P where
dist_eq_norm' : ∀ x y : P, dist x y = ‖(x -ᵥ y : V)‖Informal description
A `NormedAddTorsor V P` is a torsor (affine space) over a seminormed additive commutative group `V`, where the points `P` form a pseudometric space. The distance between points in `P` is given by the norm of the difference of their corresponding vectors in `V`. This structure bundles the pseudometric space properties and ensures consistency between the distance function and the norm-induced distance.
NormedAddTorsor.toAddTorsor'
instance
{V P : Type*} [NormedAddCommGroup V] [MetricSpace P] [NormedAddTorsor V P] : AddTorsor V P
Full source
/-- Shortcut instance to help typeclass inference out. -/
instance (priority := 100) NormedAddTorsor.toAddTorsor' {V P : Type*} [NormedAddCommGroup V]
[MetricSpace P] [NormedAddTorsor V P] : AddTorsor V P :=
NormedAddTorsor.toAddTorsorInformal description
For any normed additive commutative group $V$ and metric space $P$ with a normed additive torsor structure, $P$ is also an additive torsor over $V$.
NormedAddTorsor.to_isIsIsometricVAdd
instance
: IsIsometricVAdd V P
Full source
instance (priority := 100) NormedAddTorsor.to_isIsIsometricVAdd : IsIsometricVAdd V P :=
⟨fun c => Isometry.of_dist_eq fun x y => by
simp [NormedAddTorsor.dist_eq_norm']⟩Informal description
For any normed additive torsor $P$ over a seminormed additive commutative group $V$, the action of $V$ on $P$ is isometric. That is, for any vector $v \in V$ and point $p \in P$, the distance between $p$ and $v + p$ is equal to the norm of $v$.
SeminormedAddCommGroup.toNormedAddTorsor
instance
: NormedAddTorsor V V
Full source
/-- A `SeminormedAddCommGroup` is a `NormedAddTorsor` over itself. -/
instance (priority := 100) SeminormedAddCommGroup.toNormedAddTorsor : NormedAddTorsor V V where
dist_eq_norm' := dist_eq_normInformal description
Every seminormed additive commutative group $V$ is a normed additive torsor over itself. That is, $V$ can be viewed as an affine space over itself, where the distance between two points $x$ and $y$ in $V$ is given by the norm of their difference $\|x - y\|$.
AffineSubspace.toNormedAddTorsor
instance
{R : Type*} [Ring R] [Module R V] (s : AffineSubspace R P) [Nonempty s] : NormedAddTorsor s.direction s
Full source
/-- A nonempty affine subspace of a `NormedAddTorsor` is itself a `NormedAddTorsor`. -/
instance AffineSubspace.toNormedAddTorsor {R : Type*} [Ring R] [Module R V]
(s : AffineSubspace R P) [Nonempty s] : NormedAddTorsor s.direction s :=
{ AffineSubspace.toAddTorsor s with
dist_eq_norm' := fun x y => NormedAddTorsor.dist_eq_norm' x.val y.val }Informal description
For any ring $R$, module $V$ over $R$, and nonempty affine subspace $s$ of a normed additive torsor $P$ over $V$, the subspace $s$ inherits a normed additive torsor structure with direction space $s.\text{direction}$.
dist_eq_norm_vsub
theorem
(x y : P) : dist x y = ‖x -ᵥ y‖
Full source
/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub` sometimes doesn't work. -/
theorem dist_eq_norm_vsub (x y : P) : dist x y = ‖x -ᵥ y‖ :=
NormedAddTorsor.dist_eq_norm' x yInformal description
For any two points $x$ and $y$ in a normed additive torsor $P$ over a seminormed additive commutative group $V$, the distance between $x$ and $y$ equals the norm of their difference vector, i.e., $\text{dist}(x, y) = \|x - y\|$.
nndist_eq_nnnorm_vsub
theorem
(x y : P) : nndist x y = ‖x -ᵥ y‖₊
Full source
theorem nndist_eq_nnnorm_vsub (x y : P) : nndist x y = ‖x -ᵥ y‖₊ :=
NNReal.eq <| dist_eq_norm_vsub V x yInformal description
For any two points $x$ and $y$ in a normed additive torsor $P$ over a seminormed additive commutative group $V$, the non-negative distance between $x$ and $y$ equals the non-negative norm of their difference vector, i.e., $\text{nndist}(x, y) = \|x - y\|_{\geq 0}$.
dist_eq_norm_vsub'
theorem
(x y : P) : dist x y = ‖y -ᵥ x‖
Full source
/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub'` sometimes doesn't work. -/
theorem dist_eq_norm_vsub' (x y : P) : dist x y = ‖y -ᵥ x‖ :=
(dist_comm _ _).trans (dist_eq_norm_vsub _ _ _)Informal description
For any two points $x$ and $y$ in a normed additive torsor $P$ over a seminormed additive commutative group $V$, the distance between $x$ and $y$ equals the norm of the difference vector from $y$ to $x$, i.e., $\text{dist}(x, y) = \|y - x\|$.
nndist_eq_nnnorm_vsub'
theorem
(x y : P) : nndist x y = ‖y -ᵥ x‖₊
Full source
theorem nndist_eq_nnnorm_vsub' (x y : P) : nndist x y = ‖y -ᵥ x‖₊ :=
NNReal.eq <| dist_eq_norm_vsub' V x yInformal description
For any two points $x$ and $y$ in a normed additive torsor $P$ over a seminormed additive commutative group $V$, the non-negative distance between $x$ and $y$ equals the non-negative norm of the difference vector from $y$ to $x$, i.e., $\text{nndist}(x, y) = \|y - x\|_{\geq 0}$.
dist_vadd_cancel_left
theorem
(v : V) (x y : P) : dist (v +ᵥ x) (v +ᵥ y) = dist x y
Informal description
For any vector $v$ in a seminormed additive commutative group $V$ and any two points $x, y$ in a normed additive torsor $P$ over $V$, the distance between the translated points $v + x$ and $v + y$ is equal to the distance between $x$ and $y$, i.e., $\text{dist}(v + x, v + y) = \text{dist}(x, y)$.
nndist_vadd_cancel_left
theorem
(v : V) (x y : P) : nndist (v +ᵥ x) (v +ᵥ y) = nndist x y
Full source
theorem nndist_vadd_cancel_left (v : V) (x y : P) : nndist (v +ᵥ x) (v +ᵥ y) = nndist x y :=
NNReal.eq <| dist_vadd_cancel_left _ _ _Informal description
For any vector $v$ in a seminormed additive commutative group $V$ and any two points $x, y$ in a normed additive torsor $P$ over $V$, the non-negative distance between the translated points $v + x$ and $v + y$ is equal to the non-negative distance between $x$ and $y$, i.e., $\text{nndist}(v + x, v + y) = \text{nndist}(x, y)$.
dist_vadd_cancel_right
theorem
(v₁ v₂ : V) (x : P) : dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
Full source
@[simp]
theorem dist_vadd_cancel_right (v₁ v₂ : V) (x : P) : dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂ := by
rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]Informal description
For any vectors $v_1, v_2$ in a seminormed additive commutative group $V$ and any point $x$ in a normed additive torsor $P$ over $V$, the distance between the translated points $v_1 + x$ and $v_2 + x$ is equal to the distance between $v_1$ and $v_2$, i.e., $\text{dist}(v_1 + x, v_2 + x) = \text{dist}(v_1, v_2)$.
nndist_vadd_cancel_right
theorem
(v₁ v₂ : V) (x : P) : nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂
Full source
@[simp]
theorem nndist_vadd_cancel_right (v₁ v₂ : V) (x : P) : nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂ :=
NNReal.eq <| dist_vadd_cancel_right _ _ _Informal description
For any vectors $v_1, v_2$ in a seminormed additive commutative group $V$ and any point $x$ in a normed additive torsor $P$ over $V$, the non-negative distance between the translated points $v_1 + x$ and $v_2 + x$ is equal to the non-negative distance between $v_1$ and $v_2$, i.e., $\text{nndist}(v_1 + x, v_2 + x) = \text{nndist}(v_1, v_2)$.
dist_vadd_left
theorem
(v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖
Full source
@[simp]
theorem dist_vadd_left (v : V) (x : P) : dist (v +ᵥ x) x = ‖v‖ := by
simp [dist_eq_norm_vsub V _ x]Informal description
For any vector $v$ in a seminormed additive commutative group $V$ and any point $x$ in a normed additive torsor $P$ over $V$, the distance between the translated point $v + x$ and the original point $x$ is equal to the norm of $v$, i.e., $\text{dist}(v + x, x) = \|v\|$.
nndist_vadd_left
theorem
(v : V) (x : P) : nndist (v +ᵥ x) x = ‖v‖₊
Full source
@[simp]
theorem nndist_vadd_left (v : V) (x : P) : nndist (v +ᵥ x) x = ‖v‖₊ :=
NNReal.eq <| dist_vadd_left _ _Informal description
For any vector $v$ in a seminormed additive commutative group $V$ and any point $x$ in a normed additive torsor $P$ over $V$, the non-negative distance between the translated point $v + x$ and the original point $x$ is equal to the non-negative norm of $v$, i.e., $\text{nndist}(v + x, x) = \|v\|_+$.
dist_vadd_right
theorem
(v : V) (x : P) : dist x (v +ᵥ x) = ‖v‖
Full source
@[simp]
theorem dist_vadd_right (v : V) (x : P) : dist x (v +ᵥ x) = ‖v‖ := by rw [dist_comm, dist_vadd_left]Informal description
For any vector $v$ in a seminormed additive commutative group $V$ and any point $x$ in a normed additive torsor $P$ over $V$, the distance between the original point $x$ and the translated point $v + x$ is equal to the norm of $v$, i.e., $\text{dist}(x, v + x) = \|v\|$.
nndist_vadd_right
theorem
(v : V) (x : P) : nndist x (v +ᵥ x) = ‖v‖₊
Full source
@[simp]
theorem nndist_vadd_right (v : V) (x : P) : nndist x (v +ᵥ x) = ‖v‖₊ :=
NNReal.eq <| dist_vadd_right _ _Informal description
For any vector $v$ in a seminormed additive commutative group $V$ and any point $x$ in a normed additive torsor $P$ over $V$, the non-negative distance between $x$ and the translated point $v + x$ is equal to the non-negative norm of $v$, i.e., $\text{nndist}(x, v + x) = \|v\|_+$.
IsometryEquiv.vaddConst
definition
(x : P) : V ≃ᵢ P
Full source
/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
addition/subtraction of `x : P`. -/
@[simps!]
def IsometryEquiv.vaddConst (x : P) : V ≃ᵢ P where
toEquiv := Equiv.vaddConst x
isometry_toFun := Isometry.of_dist_eq fun _ _ => dist_vadd_cancel_right _ _ _Informal description
For any point $x$ in a normed additive torsor $P$ over a seminormed additive commutative group $V$, the map that adds $x$ to vectors in $V$ (i.e., $v \mapsto v + x$) is an isometric equivalence between $V$ and $P$. This means it preserves distances: the distance between any two vectors $v_1$ and $v_2$ in $V$ is equal to the distance between their translated points $v_1 + x$ and $v_2 + x$ in $P$.
dist_vsub_cancel_left
theorem
(x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z
Full source
@[simp]
theorem dist_vsub_cancel_left (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z := by
rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]Informal description
For any three points $x, y, z$ in a normed additive torsor $P$, the distance between the difference vectors $x - y$ and $x - z$ is equal to the distance between $y$ and $z$, i.e., $\text{dist}(x - y, x - z) = \text{dist}(y, z)$.
nndist_vsub_cancel_left
theorem
(x y z : P) : nndist (x -ᵥ y) (x -ᵥ z) = nndist y z
Full source
@[simp]
theorem nndist_vsub_cancel_left (x y z : P) : nndist (x -ᵥ y) (x -ᵥ z) = nndist y z :=
NNReal.eq <| dist_vsub_cancel_left _ _ _Informal description
For any three points $x, y, z$ in a normed additive torsor $P$, the non-negative distance between the difference vectors $x - y$ and $x - z$ is equal to the non-negative distance between $y$ and $z$, i.e., $\text{nndist}(x - y, x - z) = \text{nndist}(y, z)$.
IsometryEquiv.constVSub
definition
(x : P) : P ≃ᵢ V
Full source
/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
subtraction from `x : P`. -/
@[simps!]
def IsometryEquiv.constVSub (x : P) : P ≃ᵢ V where
toEquiv := Equiv.constVSub x
isometry_toFun := Isometry.of_dist_eq fun _ _ => dist_vsub_cancel_left _ _ _Informal description
For a fixed point $x$ in a normed additive torsor $P$ over a seminormed additive commutative group $V$, the map that subtracts $x$ from any point $y \in P$ (i.e., $y \mapsto y - x$) is an isometric equivalence between $P$ and $V$. This means it preserves distances: $\text{dist}(y - x, z - x) = \text{dist}(y, z)$ for all $y, z \in P$.
dist_vsub_cancel_right
theorem
(x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y
Full source
@[simp]
theorem dist_vsub_cancel_right (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y :=
(IsometryEquiv.vaddConst z).symm.dist_eq x yInformal description
For any three points $x, y, z$ in a normed additive torsor $P$, the distance between the difference vectors $x - z$ and $y - z$ is equal to the distance between $x$ and $y$, i.e., $\text{dist}(x - z, y - z) = \text{dist}(x, y)$.
nndist_vsub_cancel_right
theorem
(x y z : P) : nndist (x -ᵥ z) (y -ᵥ z) = nndist x y
Full source
@[simp]
theorem nndist_vsub_cancel_right (x y z : P) : nndist (x -ᵥ z) (y -ᵥ z) = nndist x y :=
NNReal.eq <| dist_vsub_cancel_right _ _ _Informal description
For any three points $x, y, z$ in a normed additive torsor $P$, the non-negative distance between the difference vectors $x - z$ and $y - z$ is equal to the non-negative distance between $x$ and $y$, i.e., $\text{nndist}(x - z, y - z) = \text{nndist}(x, y)$.
dist_vadd_vadd_le
theorem
(v v' : V) (p p' : P) : dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p'
Full source
theorem dist_vadd_vadd_le (v v' : V) (p p' : P) :
dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p' := by
simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')Informal description
For any vectors $v, v'$ in a seminormed additive commutative group $V$ and any points $p, p'$ in a normed additive torsor $P$ over $V$, the distance between the translated points $v + p$ and $v' + p'$ satisfies the inequality:
\[ \text{dist}(v + p, v' + p') \leq \text{dist}(v, v') + \text{dist}(p, p'). \]
nndist_vadd_vadd_le
theorem
(v v' : V) (p p' : P) : nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p'
Full source
theorem nndist_vadd_vadd_le (v v' : V) (p p' : P) :
nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p' :=
dist_vadd_vadd_le _ _ _ _Informal description
For any vectors $v, v'$ in a seminormed additive commutative group $V$ and any points $p, p'$ in a normed additive torsor $P$ over $V$, the non-negative distance between the translated points $v + p$ and $v' + p'$ satisfies the inequality:
\[ \text{nndist}(v + p, v' + p') \leq \text{nndist}(v, v') + \text{nndist}(p, p'). \]
dist_vsub_vsub_le
theorem
(p₁ p₂ p₃ p₄ : P) : dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄
Full source
theorem dist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄ := by
rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V]
exact norm_sub_le _ _Informal description
For any four points $p_1, p_2, p_3, p_4$ in a normed additive torsor $P$, the distance between the vector differences $p_1 - p_2$ and $p_3 - p_4$ is bounded by the sum of the distances between $p_1$ and $p_3$, and between $p_2$ and $p_4$. That is,
\[ \text{dist}(p_1 - p_2, p_3 - p_4) \leq \text{dist}(p_1, p_3) + \text{dist}(p_2, p_4). \]
nndist_vsub_vsub_le
theorem
(p₁ p₂ p₃ p₄ : P) : nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
Full source
theorem nndist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄ := by
simp only [← NNReal.coe_le_coe, NNReal.coe_add, ← dist_nndist, dist_vsub_vsub_le]Informal description
For any four points $p_1, p_2, p_3, p_4$ in a normed additive torsor $P$, the non-negative distance between the vector differences $p_1 \ominus p_2$ and $p_3 \ominus p_4$ is bounded by the sum of the non-negative distances between $p_1$ and $p_3$, and between $p_2$ and $p_4$. That is,
\[ \text{nndist}(p_1 \ominus p_2, p_3 \ominus p_4) \leq \text{nndist}(p_1, p_3) + \text{nndist}(p_2, p_4). \]
edist_vadd_vadd_le
theorem
(v v' : V) (p p' : P) : edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p'
Full source
theorem edist_vadd_vadd_le (v v' : V) (p p' : P) :
edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p' := by
simp only [edist_nndist]
norm_cast -- Porting note: was apply_mod_cast
apply dist_vadd_vadd_leInformal description
For any vectors $v, v'$ in a seminormed additive commutative group $V$ and any points $p, p'$ in a normed additive torsor $P$ over $V$, the extended distance between the translated points $v + p$ and $v' + p'$ satisfies the inequality:
\[ \text{edist}(v + p, v' + p') \leq \text{edist}(v, v') + \text{edist}(p, p'). \]
edist_vsub_vsub_le
theorem
(p₁ p₂ p₃ p₄ : P) : edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
Full source
theorem edist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄ := by
simp only [edist_nndist]
norm_cast -- Porting note: was apply_mod_cast
apply dist_vsub_vsub_leInformal description
For any four points $p_1, p_2, p_3, p_4$ in a normed additive torsor $P$, the extended distance between the vector differences $p_1 - p_2$ and $p_3 - p_4$ is bounded by the sum of the extended distances between $p_1$ and $p_3$, and between $p_2$ and $p_4$. That is,
\[ \text{edist}(p_1 - p_2, p_3 - p_4) \leq \text{edist}(p_1, p_3) + \text{edist}(p_2, p_4). \]
pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor
definition
(V P : Type*) [SeminormedAddCommGroup V] [AddTorsor V P] : PseudoMetricSpace P
Full source
/-- The pseudodistance defines a pseudometric space structure on the torsor. This
is not an instance because it depends on `V` to define a `MetricSpace P`. -/
def pseudoMetricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type*) [SeminormedAddCommGroup V]
[AddTorsor V P] : PseudoMetricSpace P where
dist x y := ‖(x -ᵥ y : V)‖
dist_self x := by simp
dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
dist_triangle x y z := by
rw [← vsub_add_vsub_cancel]
apply norm_add_le
Informal description
Given a seminormed additive commutative group $V$ and an additive torsor $P$ over $V$, the pseudometric space structure on $P$ is defined by the distance function $\text{dist}(x, y) = \|x -ᵥ y\|$ for any $x, y \in P$, where $-ᵥ$ denotes the torsor subtraction operation. This distance function satisfies:
1. $\text{dist}(x, x) = 0$ for all $x \in P$,
2. $\text{dist}(x, y) = \text{dist}(y, x)$ for all $x, y \in P$,
3. $\text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z)$ for all $x, y, z \in P$.
metricSpaceOfNormedAddCommGroupOfAddTorsor
definition
(V P : Type*) [NormedAddCommGroup V] [AddTorsor V P] : MetricSpace P
Full source
/-- The distance defines a metric space structure on the torsor. This
is not an instance because it depends on `V` to define a `MetricSpace P`. -/
def metricSpaceOfNormedAddCommGroupOfAddTorsor (V P : Type*) [NormedAddCommGroup V]
[AddTorsor V P] : MetricSpace P where
dist x y := ‖(x -ᵥ y : V)‖
dist_self x := by simp
eq_of_dist_eq_zero h := by simpa using h
dist_comm x y := by simp only [← neg_vsub_eq_vsub_rev y x, norm_neg]
dist_triangle x y z := by
rw [← vsub_add_vsub_cancel]
apply norm_add_le
Informal description
Given a normed additive commutative group $V$ and an additive torsor $P$ over $V$, the function `metricSpaceOfNormedAddCommGroupOfAddTorsor` defines a metric space structure on $P$ where the distance between two points $x$ and $y$ is given by the norm of their difference vector $\|x -ᵥ y\|$. This distance function satisfies the following properties:
1. **Reflexivity**: $\mathrm{dist}(x, x) = 0$ for all $x \in P$,
2. **Identity of indiscernibles**: $\mathrm{dist}(x, y) = 0$ implies $x = y$,
3. **Symmetry**: $\mathrm{dist}(x, y) = \mathrm{dist}(y, x)$ for all $x, y \in P$,
4. **Triangle inequality**: $\mathrm{dist}(x, z) \leq \mathrm{dist}(x, y) + \mathrm{dist}(y, z)$ for all $x, y, z \in P$.
LipschitzWith.vadd
theorem
[PseudoEMetricSpace α] {f : α → V} {g : α → P} {Kf Kg : ℝ≥0} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) (f +ᵥ g)
Full source
theorem LipschitzWith.vadd [PseudoEMetricSpace α] {f : α → V} {g : α → P} {Kf Kg : ℝ≥0}
(hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) (f +ᵥ g) :=
fun x y =>
calc
edist (f x +ᵥ g x) (f y +ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) :=
edist_vadd_vadd_le _ _ _ _
_ ≤ Kf * edist x y + Kg * edist x y := add_le_add (hf x y) (hg x y)
_ = (Kf + Kg) * edist x y := (add_mul _ _ _).symmInformal description
Let $\alpha$ be a pseudoemetric space, $V$ a seminormed additive commutative group, and $P$ a normed additive torsor over $V$. Given Lipschitz functions $f : \alpha \to V$ and $g : \alpha \to P$ with Lipschitz constants $K_f$ and $K_g$ respectively, the function $f + g : \alpha \to P$ defined by $(f + g)(x) = f(x) + g(x)$ is Lipschitz with constant $K_f + K_g$.
LipschitzWith.vsub
theorem
[PseudoEMetricSpace α] {f g : α → P} {Kf Kg : ℝ≥0} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
LipschitzWith (Kf + Kg) (f -ᵥ g)
Full source
theorem LipschitzWith.vsub [PseudoEMetricSpace α] {f g : α → P} {Kf Kg : ℝ≥0}
(hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) (f -ᵥ g) :=
fun x y =>
calc
edist (f x -ᵥ g x) (f y -ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) :=
edist_vsub_vsub_le _ _ _ _
_ ≤ Kf * edist x y + Kg * edist x y := add_le_add (hf x y) (hg x y)
_ = (Kf + Kg) * edist x y := (add_mul _ _ _).symmInformal description
Let $\alpha$ be a pseudoemetric space and $f, g : \alpha \to P$ be Lipschitz functions with constants $K_f$ and $K_g$ respectively, where $P$ is a normed additive torsor over a seminormed additive commutative group $V$. Then the vector subtraction function $f - g : \alpha \to V$ is Lipschitz with constant $K_f + K_g$.
uniformContinuous_vadd
theorem
: UniformContinuous fun x : V × P => x.1 +ᵥ x.2
Full source
theorem uniformContinuous_vadd : UniformContinuous fun x : V × P => x.1 +ᵥ x.2 :=
(LipschitzWith.prod_fst.vadd LipschitzWith.prod_snd).uniformContinuousInformal description
Let $V$ be a seminormed additive commutative group and $P$ a normed additive torsor over $V$. The vector addition operation $+ᵥ : V \times P \to P$ is uniformly continuous, where $V \times P$ is equipped with the product uniform structure.
uniformContinuous_vsub
theorem
: UniformContinuous fun x : P × P => x.1 -ᵥ x.2
Full source
theorem uniformContinuous_vsub : UniformContinuous fun x : P × P => x.1 -ᵥ x.2 :=
(LipschitzWith.prod_fst.vsub LipschitzWith.prod_snd).uniformContinuousInformal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$. The vector subtraction operation $-ᵥ : P \times P \to V$ is uniformly continuous, where the product space $P \times P$ is equipped with the product uniform structure.
NormedAddTorsor.to_continuousVAdd
instance
: ContinuousVAdd V P
Full source
instance (priority := 100) NormedAddTorsor.to_continuousVAdd : ContinuousVAdd V P where
continuous_vadd := uniformContinuous_vadd.continuousInformal description
For any normed additive torsor $P$ over a seminormed additive commutative group $V$, the additive action $+ᵥ \colon V \times P \to P$ is continuous.
continuous_vsub
theorem
: Continuous fun x : P × P => x.1 -ᵥ x.2
Full source
theorem continuous_vsub : Continuous fun x : P × P => x.1 -ᵥ x.2 :=
uniformContinuous_vsub.continuousInformal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$. The vector subtraction operation $-ᵥ : P \times P \to V$, defined by $(x, y) \mapsto x -ᵥ y$, is continuous when $P \times P$ is equipped with the product topology.
Filter.Tendsto.vsub
theorem
{l : Filter α} {f g : α → P} {x y : P} (hf : Tendsto f l (𝓝 x)) (hg : Tendsto g l (𝓝 y)) :
Tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y))
Full source
theorem Filter.Tendsto.vsub {l : Filter α} {f g : α → P} {x y : P} (hf : Tendsto f l (𝓝 x))
(hg : Tendsto g l (𝓝 y)) : Tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y)) :=
(continuous_vsub.tendsto (x, y)).comp (hf.prodMk_nhds hg)Informal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $\alpha$ be a type. For any filter $l$ on $\alpha$ and any functions $f, g: \alpha \to P$, if $f$ tends to $x \in P$ along $l$ and $g$ tends to $y \in P$ along $l$, then the function $(f -ᵥ g) : \alpha \to V$ tends to $(x -ᵥ y) \in V$ along $l$.
Continuous.vsub
theorem
{f g : α → P} (hf : Continuous f) (hg : Continuous g) : Continuous (fun x ↦ f x -ᵥ g x)
Full source
@[fun_prop]
theorem Continuous.vsub {f g : α → P} (hf : Continuous f) (hg : Continuous g) :
Continuous (fun x ↦ f x -ᵥ g x) :=
continuous_vsub.comp₂ hf hgInformal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $f, g : \alpha \to P$ be continuous functions. Then the function $x \mapsto f(x) -ᵥ g(x)$ is continuous.
ContinuousAt.vsub
theorem
{f g : α → P} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun x ↦ f x -ᵥ g x) x
Full source
@[fun_prop]
nonrec theorem ContinuousAt.vsub {f g : α → P} {x : α} (hf : ContinuousAt f x)
(hg : ContinuousAt g x) :
ContinuousAt (fun x ↦ f x -ᵥ g x) x :=
hf.vsub hgInformal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $f, g : \alpha \to P$ be functions. If $f$ is continuous at $x \in \alpha$ and $g$ is continuous at $x$, then the function $x \mapsto f(x) -ᵥ g(x)$ is continuous at $x$.
ContinuousWithinAt.vsub
theorem
{f g : α → P} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
ContinuousWithinAt (fun x ↦ f x -ᵥ g x) s x
Full source
@[fun_prop]
nonrec theorem ContinuousWithinAt.vsub {f g : α → P} {x : α} {s : Set α}
(hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
ContinuousWithinAt (fun x ↦ f x -ᵥ g x) s x :=
hf.vsub hgInformal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $f, g : \alpha \to P$ be functions. For a point $x \in \alpha$ and a subset $s \subseteq \alpha$, if $f$ is continuous within $s$ at $x$ and $g$ is continuous within $s$ at $x$, then the function $x \mapsto f(x) -ᵥ g(x)$ is continuous within $s$ at $x$.
ContinuousOn.vsub
theorem
{f g : α → P} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun x ↦ f x -ᵥ g x) s
Full source
@[fun_prop]
theorem ContinuousOn.vsub {f g : α → P} {s : Set α} (hf : ContinuousOn f s)
(hg : ContinuousOn g s) : ContinuousOn (fun x ↦ f x -ᵥ g x) s := fun x hx ↦
(hf x hx).vsub (hg x hx)Informal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $f, g : \alpha \to P$ be functions. For a subset $s \subseteq \alpha$, if $f$ is continuous on $s$ and $g$ is continuous on $s$, then the function $x \mapsto f(x) -ᵥ g(x)$ is continuous on $s$.
Filter.Tendsto.lineMap
theorem
{l : Filter α} {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R} (h₁ : Tendsto f₁ l (𝓝 p₁)) (h₂ : Tendsto f₂ l (𝓝 p₂))
(hg : Tendsto g l (𝓝 c)) : Tendsto (fun x => AffineMap.lineMap (f₁ x) (f₂ x) (g x)) l (𝓝 <| AffineMap.lineMap p₁ p₂ c)
Full source
theorem Filter.Tendsto.lineMap {l : Filter α} {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R}
(h₁ : Tendsto f₁ l (𝓝 p₁)) (h₂ : Tendsto f₂ l (𝓝 p₂)) (hg : Tendsto g l (𝓝 c)) :
Tendsto (fun x => AffineMap.lineMap (f₁ x) (f₂ x) (g x)) l (𝓝 <| AffineMap.lineMap p₁ p₂ c) :=
(hg.smul (h₂.vsub h₁)).vadd h₁Informal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $R$ be a ring. Given a filter $l$ on a type $\alpha$, functions $f_1, f_2 \colon \alpha \to P$, and $g \colon \alpha \to R$, if $f_1$ tends to $p_1 \in P$ along $l$, $f_2$ tends to $p_2 \in P$ along $l$, and $g$ tends to $c \in R$ along $l$, then the function $x \mapsto \text{AffineMap.lineMap}(f_1(x), f_2(x), g(x))$ tends to $\text{AffineMap.lineMap}(p_1, p_2, c)$ along $l$.
Here, $\text{AffineMap.lineMap}(a, b, c)$ denotes the affine map parameterized by $c$ between points $a$ and $b$ in the torsor $P$.
Filter.Tendsto.midpoint
theorem
[Invertible (2 : R)] {l : Filter α} {f₁ f₂ : α → P} {p₁ p₂ : P} (h₁ : Tendsto f₁ l (𝓝 p₁)) (h₂ : Tendsto f₂ l (𝓝 p₂)) :
Tendsto (fun x => midpoint R (f₁ x) (f₂ x)) l (𝓝 <| midpoint R p₁ p₂)
Full source
theorem Filter.Tendsto.midpoint [Invertible (2 : R)] {l : Filter α} {f₁ f₂ : α → P} {p₁ p₂ : P}
(h₁ : Tendsto f₁ l (𝓝 p₁)) (h₂ : Tendsto f₂ l (𝓝 p₂)) :
Tendsto (fun x => midpoint R (f₁ x) (f₂ x)) l (𝓝 <| midpoint R p₁ p₂) :=
h₁.lineMap h₂ tendsto_const_nhdsInformal description
Let $P$ be a normed additive torsor over a seminormed additive commutative group $V$, and let $R$ be a ring with an invertible element $2$. Given a filter $l$ on a type $\alpha$ and functions $f_1, f_2 \colon \alpha \to P$, if $f_1$ tends to $p_1 \in P$ along $l$ and $f_2$ tends to $p_2 \in P$ along $l$, then the function $x \mapsto \text{midpoint}_R(f_1(x), f_2(x))$ tends to $\text{midpoint}_R(p_1, p_2)$ along $l$.
Here, $\text{midpoint}_R(a, b)$ denotes the midpoint of $a$ and $b$ in the torsor $P$ with respect to the ring $R$.
IsClosed.vadd_right_of_isCompact
theorem
{s : Set V} {t : Set P} (hs : IsClosed s) (ht : IsCompact t) : IsClosed (s +ᵥ t)
Full source
theorem IsClosed.vadd_right_of_isCompact {s : Set V} {t : Set P} (hs : IsClosed s)
(ht : IsCompact t) : IsClosed (s +ᵥ t) := by
-- This result is still true for any `AddTorsor` where `-ᵥ` is continuous,
-- but we don't yet have a nice way to state it.
refine IsSeqClosed.isClosed (fun u p husv hup ↦ ?_)
choose! a ha v hv hav using husv
rcases ht.isSeqCompact hv with ⟨q, hqt, φ, φ_mono, hφq⟩
refine ⟨p -ᵥ q, hs.mem_of_tendsto ((hup.comp φ_mono.tendsto_atTop).vsub hφq)
(Eventually.of_forall fun n ↦ ?_), q, hqt, vsub_vadd _ _⟩
convert ha (φ n) using 1
exact (eq_vadd_iff_vsub_eq _ _ _).mp (hav (φ n)).symmInformal description
Let $V$ be a seminormed additive commutative group and $P$ a pseudometric space forming a normed additive torsor over $V$. For any closed subset $s \subseteq V$ and any compact subset $t \subseteq P$, the set $s +ᵥ t = \{v + p \mid v \in s, p \in t\}$ is closed in $P$.