Documentation

Mathlib.Analysis.Normed.Group.AddTorsor

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.

class NormedAddTorsor (V : outParam (Type u_1)) (P : Type u_2) [outParam (SeminormedAddCommGroup V)] [PseudoMetricSpace P] extends AddTorsor :
Type (max u_1 u_2)

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

  • vadd : VPP
  • zero_vadd : ∀ (p : P), 0 +ᵥ p = p
  • add_vadd : ∀ (g₁ g₂ : V) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
  • vsub : PPV
  • nonempty : Nonempty P
  • vsub_vadd' : ∀ (p₁ p₂ : P), p₁ -ᵥ p₂ +ᵥ p₂ = p₁
  • vadd_vsub' : ∀ (g : V) (p : P), g +ᵥ p -ᵥ p = g
  • dist_eq_norm' : ∀ (x y : P), dist x y = x -ᵥ y
Instances

    Shortcut instance to help typeclass inference out.

    Equations
    • NormedAddTorsor.toAddTorsor' = NormedAddTorsor.toAddTorsor

    A SeminormedAddCommGroup is a NormedAddTorsor over itself.

    Equations
    theorem dist_eq_norm_vsub (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) :
    dist x y = x -ᵥ y

    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 nndist_eq_nnnorm_vsub (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) :
    theorem dist_eq_norm_vsub' (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) :
    dist x y = y -ᵥ x

    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 nndist_eq_nnnorm_vsub' (V : Type u_2) {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) :
    theorem dist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) (y : P) :
    dist (v +ᵥ x) (v +ᵥ y) = dist x y
    theorem nndist_vadd_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) (y : P) :
    nndist (v +ᵥ x) (v +ᵥ y) = nndist x y
    @[simp]
    theorem dist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v₁ : V) (v₂ : V) (x : P) :
    dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂
    @[simp]
    theorem nndist_vadd_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v₁ : V) (v₂ : V) (x : P) :
    nndist (v₁ +ᵥ x) (v₂ +ᵥ x) = nndist v₁ v₂
    @[simp]
    theorem dist_vadd_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) :
    dist (v +ᵥ x) x = v
    @[simp]
    theorem nndist_vadd_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) :
    @[simp]
    theorem dist_vadd_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) :
    dist x (v +ᵥ x) = v
    @[simp]
    theorem nndist_vadd_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (x : P) :
    @[simp]
    @[simp]
    @[simp]
    theorem IsometryEquiv.vaddConst_invFun {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (p' : P) :
    (IsometryEquiv.vaddConst x).invFun p' = p' -ᵥ x

    Isometry between the tangent space V of a (semi)normed add torsor P and P given by addition/subtraction of x : P.

    Equations
    Instances For
      @[simp]
      theorem dist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) (z : P) :
      dist (x -ᵥ y) (x -ᵥ z) = dist y z
      @[simp]
      theorem nndist_vsub_cancel_left {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) (z : P) :
      nndist (x -ᵥ y) (x -ᵥ z) = nndist y z
      @[simp]
      theorem IsometryEquiv.constVSub_toFun {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :
      ∀ (x_1 : P), (IsometryEquiv.constVSub x) x_1 = x -ᵥ x_1
      @[simp]
      theorem IsometryEquiv.constVSub_invFun {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :
      ∀ (x_1 : V), (IsometryEquiv.constVSub x).invFun x_1 = -x_1 +ᵥ x
      @[simp]
      theorem IsometryEquiv.constVSub_apply {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) :
      ∀ (x_1 : P), (IsometryEquiv.constVSub x) x_1 = x -ᵥ x_1

      Isometry between the tangent space V of a (semi)normed add torsor P and P given by subtraction from x : P.

      Equations
      Instances For
        @[simp]
        theorem dist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) (z : P) :
        dist (x -ᵥ z) (y -ᵥ z) = dist x y
        @[simp]
        theorem nndist_vsub_cancel_right {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (x : P) (y : P) (z : P) :
        nndist (x -ᵥ z) (y -ᵥ z) = nndist x y
        theorem dist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (v' : V) (p : P) (p' : P) :
        dist (v +ᵥ p) (v' +ᵥ p') dist v v' + dist p p'
        theorem nndist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (v' : V) (p : P) (p' : P) :
        nndist (v +ᵥ p) (v' +ᵥ p') nndist v v' + nndist p p'
        theorem dist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :
        dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) dist p₁ p₃ + dist p₂ p₄
        theorem nndist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :
        nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) nndist p₁ p₃ + nndist p₂ p₄
        theorem edist_vadd_vadd_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (v : V) (v' : V) (p : P) (p' : P) :
        edist (v +ᵥ p) (v' +ᵥ p') edist v v' + edist p p'
        theorem edist_vsub_vsub_le {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :
        edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) edist p₁ p₃ + edist p₂ p₄

        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.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          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.

          Equations
          Instances For
            theorem LipschitzWith.vadd {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [PseudoEMetricSpace α] {f : αV} {g : αP} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
            LipschitzWith (Kf + Kg) (f +ᵥ g)
            theorem LipschitzWith.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [PseudoEMetricSpace α] {f : αP} {g : αP} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
            LipschitzWith (Kf + Kg) (f -ᵥ g)
            theorem uniformContinuous_vadd {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] :
            UniformContinuous fun (x : V × P) => x.1 +ᵥ x.2
            theorem uniformContinuous_vsub {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] :
            UniformContinuous fun (x : P × P) => x.1 -ᵥ x.2
            theorem continuous_vsub {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] :
            Continuous fun (x : P × P) => x.1 -ᵥ x.2
            theorem Filter.Tendsto.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {l : Filter α} {f : αP} {g : αP} {x : P} {y : P} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :
            Filter.Tendsto (f -ᵥ g) l (nhds (x -ᵥ y))
            theorem Continuous.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [TopologicalSpace α] {f : αP} {g : αP} (hf : Continuous f) (hg : Continuous g) :
            theorem ContinuousAt.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [TopologicalSpace α] {f : αP} {g : αP} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
            theorem ContinuousWithinAt.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [TopologicalSpace α] {f : αP} {g : αP} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
            theorem ContinuousOn.vsub {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] [TopologicalSpace α] {f : αP} {g : αP} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
            theorem Filter.Tendsto.lineMap {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {R : Type u_6} [Ring R] [TopologicalSpace R] [Module R V] [ContinuousSMul R V] {l : Filter α} {f₁ : αP} {f₂ : αP} {g : αR} {p₁ : P} {p₂ : P} {c : R} (h₁ : Filter.Tendsto f₁ l (nhds p₁)) (h₂ : Filter.Tendsto f₂ l (nhds p₂)) (hg : Filter.Tendsto g l (nhds c)) :
            Filter.Tendsto (fun (x : α) => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) l (nhds ((AffineMap.lineMap p₁ p₂) c))
            theorem Filter.Tendsto.midpoint {α : Type u_1} {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {R : Type u_6} [Ring R] [TopologicalSpace R] [Module R V] [ContinuousSMul R V] [Invertible 2] {l : Filter α} {f₁ : αP} {f₂ : αP} {p₁ : P} {p₂ : P} (h₁ : Filter.Tendsto f₁ l (nhds p₁)) (h₂ : Filter.Tendsto f₂ l (nhds p₂)) :
            Filter.Tendsto (fun (x : α) => midpoint R (f₁ x) (f₂ x)) l (nhds (midpoint R p₁ p₂))
            theorem IsClosed.vadd_right_of_isCompact {V : Type u_2} {P : Type u_3} [SeminormedAddCommGroup V] [PseudoMetricSpace P] [NormedAddTorsor V P] {s : Set V} {t : Set P} (hs : IsClosed s) (ht : IsCompact t) :