Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.SpaceAndTime.Space.Basic
public import Physlib.SpaceAndTime.Space.Origin
public import Mathlib.Geometry.Manifold.Diffeomorph
public import Mathlib.Analysis.Distribution.TemperateGrowth
public import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
public import Mathlib.Analysis.Calculus.ContDiff.WithLp
public import Mathlib.Tactic.Cases
public import Mathlib.Analysis.Calculus.FDeriv.WithLpThe structure of a module on Space
The scope of this module is to define on Space d the structure of a Module
(aka vector space), a Norm and an InnerProductSpace, and give properties of these structures.
These instances require certain non-canonical choices to be made, for example the choice of a zero and for a basis, a choice of orientation.
Instances in Lean
In Lean, an instance supplies a typeclass automatically. When a definition or
theorem needs a structure such as AddCommGroup (Space d), Module ℝ (Space d),
NormedAddCommGroup (Space d), InnerProductSpace ℝ (Space d), or
MeasurableSpace (Space d), typeclass inference searches for the corresponding
instance and inserts it without the user passing it explicitly.
These instances make Space d usable with standard mathematical notation and
with the Mathlib API. For example, they allow expressions such as p + q,
c • p, ‖p‖, inner ℝ p q, and measurable-set arguments involving the Borel
structure. They also make general theorems about modules, normed groups, inner
product spaces, and measurable spaces apply directly to Space d.
For Space d, these instances are intentional choices rather than inherited
facts: the type was defined as a structure instead of an abbreviation for
Euclidean space. In particular, the additive and module structures choose an
origin, while the norm, inner product, and Borel structure choose the standard
Euclidean coordinate geometry.
@[expose] public sectionA.1. Instance of an additive commutative monoid
instance {d} : Add (Space d) where
add p q := ⟨fun i => p.val i + q.val i⟩@[simp]
lemma add_val {d: ℕ} (x y : Space d) :
(x + y).val = x.val + y.val := rfl@[simp]
lemma add_apply {d : ℕ} (x y : Space d) (i : Fin d) :
(x + y) i = x i + y i := d:ℕx:Space dy:Space di:Fin d⊢ (x + y).val i = x.val i + y.val i
All goals completed! 🐙instance {d} : AddCommMonoid (Space d) where
add_assoc a b c:= d:ℕa:Space db:Space dc:Space d⊢ a + b + c = a + (b + c)
d:ℕa:Space db:Space dc:Space d⊢ (a + b + c).val = (a + (b + c)).val
d:ℕa:Space db:Space dc:Space d⊢ a.val + b.val + c.val = a.val + (b.val + c.val)
All goals completed! 🐙
zero_add a := d:ℕa:Space d⊢ 0 + a = a
d:ℕa:Space d⊢ (0 + a).val = a.val
d:ℕa:Space d⊢ (fun x => 0) = 0
All goals completed! 🐙
add_zero a := d:ℕa:Space d⊢ a + 0 = a
d:ℕa:Space d⊢ (a + 0).val = a.val
d:ℕa:Space d⊢ (fun x => 0) = 0
All goals completed! 🐙
add_comm a b := d:ℕa:Space db:Space d⊢ a + b = b + a
d:ℕa:Space db:Space d⊢ (a + b).val = (b + a).val
d:ℕa:Space db:Space d⊢ a.val + b.val = b.val + a.val
All goals completed! 🐙
nsmul n a := ⟨fun i => n • a.val i⟩@[simp]
lemma nsmul_val {d : ℕ} (n : ℕ) (a : Space d) :
(n • a).val = fun i => n • a.val i := rfl@[simp]
lemma nsmul_apply {d : ℕ} (n : ℕ) (a : Space d) (i : Fin d) :
(n • a) i = n • (a i) := d:ℕn:ℕa:Space di:Fin d⊢ (n • a).val i = n • a.val i All goals completed! 🐙lemma eq_vadd_zero {d} (s : Space d) :
∃ v : EuclideanSpace ℝ (Fin d), s = v +ᵥ (0 : Space d) := d:ℕs:Space d⊢ ∃ v, s = v +ᵥ 0
d:ℕv:EuclideanSpace ℝ (Fin d)⊢ ∃ v_1, v +ᵥ 0 = v_1 +ᵥ 0
All goals completed! 🐙@[simp]
lemma add_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
(v1 +ᵥ (0 : Space d)) + (v2 +ᵥ (0 : Space d)) = (v1 + v2) +ᵥ (0 : Space d) := d:ℕv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)⊢ (v1 +ᵥ 0) + (v2 +ᵥ 0) = (v1 + v2) +ᵥ 0
d:ℕv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)i:Fin d⊢ ((v1 +ᵥ 0) + (v2 +ᵥ 0)).val i = ((v1 + v2) +ᵥ 0).val i
All goals completed! 🐙
A.2. Instance of a module over ℝ
instance {d} : SMul ℝ (Space d) where
smul c p := ⟨fun i => c * p.val i⟩@[simp]
lemma smul_val {d : ℕ} (c : ℝ) (p : Space d) :
(c • p).val = fun i => c * p.val i := rfl@[simp]
lemma smul_apply {d : ℕ} (c : ℝ) (p : Space d) (i : Fin d) :
(c • p) i = c * (p i) := d:ℕc:ℝp:Space di:Fin d⊢ (c • p).val i = c * p.val i All goals completed! 🐙@[simp]
lemma smul_vadd_zero {d} (k : ℝ) (v : EuclideanSpace ℝ (Fin d)) :
k • (v +ᵥ (0 : Space d)) = (k • v) +ᵥ (0 : Space d) := d:ℕk:ℝv:EuclideanSpace ℝ (Fin d)⊢ k • (v +ᵥ 0) = k • v +ᵥ 0
d:ℕk:ℝv:EuclideanSpace ℝ (Fin d)i:Fin d⊢ (k • (v +ᵥ 0)).val i = (k • v +ᵥ 0).val i
All goals completed! 🐙instance {d} : Module ℝ (Space d) where
one_smul x := d:ℕx:Space d⊢ 1 • x = x
d:ℕx:Space di:Fin d⊢ (1 • x).val i = x.val i
All goals completed! 🐙
mul_smul a b x := d:ℕa:ℝb:ℝx:Space d⊢ (a * b) • x = a • b • x
d:ℕa:ℝb:ℝx:Space di:Fin d⊢ ((a * b) • x).val i = (a • b • x).val i
All goals completed! 🐙
smul_add a x y := d:ℕa:ℝx:Space dy:Space d⊢ a • (x + y) = a • x + a • y
d:ℕa:ℝx:Space dy:Space di:Fin d⊢ (a • (x + y)).val i = (a • x + a • y).val i
All goals completed! 🐙
smul_zero a := d:ℕa:ℝ⊢ a • 0 = 0
d:ℕa:ℝi:Fin d⊢ (a • 0).val i = val 0 i
All goals completed! 🐙
add_smul a b x := d:ℕa:ℝb:ℝx:Space d⊢ (a + b) • x = a • x + b • x
d:ℕa:ℝb:ℝx:Space di:Fin d⊢ ((a + b) • x).val i = (a • x + b • x).val i
All goals completed! 🐙
zero_smul x := d:ℕx:Space d⊢ 0 • x = 0
d:ℕx:Space di:Fin d⊢ (0 • x).val i = val 0 i
All goals completed! 🐙A.3. Instance of an inner product space
lemma norm_eq {d} (p : Space d) : ‖p‖ = √ (∑ i, (p i) ^ 2) := d:ℕp:Space d⊢ ‖p‖ = √(∑ i, p.val i ^ 2)
All goals completed! 🐙d:ℕp:Space di:Fin d⊢ |p.val i| ≤ √(∑ i, p.val i ^ 2)
exact Real.abs_le_sqrt
(Finset.single_le_sum (f := fun j => (p j) ^ 2) (fun j _ => d:ℕp:Space di:Fin dj:Fin dx✝:j ∈ Finset.univ⊢ 0 ≤ p.val j ^ 2 All goals completed! 🐙) (Finset.mem_univ i))d:ℕp:Space d⊢ √(∑ i, p.val i ^ 2) ^ 2 = ∑ i, p.val i ^ 2
exact Real.sq_sqrt (d:ℕp:Space d⊢ 0 ≤ ∑ i, p.val i ^ 2 All goals completed! 🐙)lemma point_dim_zero_eq (p : Space 0) : p = 0 :=
Subsingleton.elim p 0@[simp]
lemma norm_vadd_zero {d} (v : EuclideanSpace ℝ (Fin d)) :
‖v +ᵥ (0 : Space d)‖ = ‖v‖ := d:ℕv:EuclideanSpace ℝ (Fin d)⊢ ‖v +ᵥ 0‖ = ‖v‖
All goals completed! 🐙instance : Neg (Space d) where
neg p := ⟨fun i => - (p.val i)⟩@[simp]
lemma neg_val {d : ℕ} (p : Space d) :
(-p).val = fun i => - (p.val i) := rfl@[simp]
lemma neg_apply {d : ℕ} (p : Space d) (i : Fin d) :
(-p) i = - (p i) := d:ℕp:Space di:Fin d⊢ (-p).val i = -p.val i All goals completed! 🐙@[simp]
lemma sub_apply {d} (p q : Space d) (i : Fin d) :
(p - q) i = p i - q i := d:ℕp:Space dq:Space di:Fin d⊢ (p - q).val i = p.val i - q.val i
All goals completed! 🐙@[simp]
lemma sub_val {d} (p q : Space d) :
(p - q).val = fun i => p.val i - q.val i := d:ℕp:Space dq:Space d⊢ (p - q).val = fun i => p.val i - q.val i All goals completed! 🐙@[simp]
lemma vadd_zero_sub_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
(v1 +ᵥ (0 : Space d)) - (v2 +ᵥ (0 : Space d)) = (v1 - v2) +ᵥ (0 : Space d) := d:ℕv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)⊢ (v1 +ᵥ 0) - (v2 +ᵥ 0) = (v1 - v2) +ᵥ 0
d:ℕv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)i:Fin d⊢ ((v1 +ᵥ 0) - (v2 +ᵥ 0)).val i = ((v1 - v2) +ᵥ 0).val i
All goals completed! 🐙@[simp]
lemma dist_eq_norm {d} (p q : Space d) :
dist p q = ‖p - q‖ := rflinstance {d} : Inner ℝ (Space d) where
inner p q := ∑ i, p i * q i@[simp]
lemma inner_vadd_zero {d} (v1 v2 : EuclideanSpace ℝ (Fin d)) :
inner ℝ (v1 +ᵥ (0 : Space d)) (v2 +ᵥ (0 : Space d)) = Inner.inner ℝ v1 v2 := d:ℕv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)⊢ inner ℝ (v1 +ᵥ 0) (v2 +ᵥ 0) = inner ℝ v1 v2
All goals completed! 🐙lemma inner_apply {d} (p q : Space d) :
inner ℝ p q = ∑ i, p i * q i := d:ℕp:Space dq:Space d⊢ inner ℝ p q = ∑ i, p.val i * q.val i All goals completed! 🐙instance {d} : InnerProductSpace ℝ (Space d) where
norm_smul_le a x := d:ℕa:ℝx:Space d⊢ ‖a • x‖ ≤ ‖a‖ * ‖x‖
d:ℕa:ℝv:EuclideanSpace ℝ (Fin d)⊢ ‖a • (v +ᵥ 0)‖ ≤ ‖a‖ * ‖v +ᵥ 0‖
All goals completed! 🐙
norm_sq_eq_re_inner x := d:ℕx:Space d⊢ ‖x‖ ^ 2 = RCLike.re (inner ℝ x x)
d:ℕv:EuclideanSpace ℝ (Fin d)⊢ ‖v +ᵥ 0‖ ^ 2 = RCLike.re (inner ℝ (v +ᵥ 0) (v +ᵥ 0))
All goals completed! 🐙
conj_inner_symm x y := d:ℕx:Space dy:Space d⊢ (starRingEnd ℝ) (inner ℝ y x) = inner ℝ x y
All goals completed! 🐙
add_left x y z := d:ℕx:Space dy:Space dz:Space d⊢ inner ℝ (x + y) z = inner ℝ x z + inner ℝ y z
d:ℕy:Space dz:Space dv1:EuclideanSpace ℝ (Fin d)⊢ inner ℝ ((v1 +ᵥ 0) + y) z = inner ℝ (v1 +ᵥ 0) z + inner ℝ y z
d:ℕz:Space dv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)⊢ inner ℝ ((v1 +ᵥ 0) + (v2 +ᵥ 0)) z = inner ℝ (v1 +ᵥ 0) z + inner ℝ (v2 +ᵥ 0) z
d:ℕv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)v3:EuclideanSpace ℝ (Fin d)⊢ inner ℝ ((v1 +ᵥ 0) + (v2 +ᵥ 0)) (v3 +ᵥ 0) = inner ℝ (v1 +ᵥ 0) (v3 +ᵥ 0) + inner ℝ (v2 +ᵥ 0) (v3 +ᵥ 0)
All goals completed! 🐙
smul_left x y a := d:ℕx:Space dy:Space da:ℝ⊢ inner ℝ (a • x) y = (starRingEnd ℝ) a * inner ℝ x y
d:ℕy:Space da:ℝv1:EuclideanSpace ℝ (Fin d)⊢ inner ℝ (a • (v1 +ᵥ 0)) y = (starRingEnd ℝ) a * inner ℝ (v1 +ᵥ 0) y
d:ℕa:ℝv1:EuclideanSpace ℝ (Fin d)v2:EuclideanSpace ℝ (Fin d)⊢ inner ℝ (a • (v1 +ᵥ 0)) (v2 +ᵥ 0) = (starRingEnd ℝ) a * inner ℝ (v1 +ᵥ 0) (v2 +ᵥ 0)
All goals completed! 🐙lemma norm_smul_sphere {d : ℕ} (n : ↑(Metric.sphere (0 : Space d) 1))
{r : ℝ} (hr : 0 ≤ r) :
‖(r • (n : Space d))‖ = r := d:ℕn:↑(Metric.sphere 0 1)r:ℝhr:0 ≤ r⊢ ‖r • ↑n‖ = r
All goals completed! 🐙A.4. Instance of a measurable space
instance {d : ℕ} : BorelSpace (Space d) where
measurable_eq := d:ℕ⊢ instMeasurableSpace = borel (Space d) All goals completed! 🐙
The norm on Space
Inner product
lemma inner_eq_sum {d} (p q : Space d) :
inner ℝ p q = ∑ i, p i * q i := d:ℕp:Space dq:Space d⊢ inner ℝ p q = ∑ i, p.val i * q.val i
All goals completed! 🐙d:ℕι:Typeinst✝:Fintype ιf:ι → Space di:Fin dP:(ι : Type) → [Fintype ι] → Prop := fun ι [Fintype ι] => ∀ (f : ι → Space d) (i : Fin d), (∑ x, f x).val i = ∑ x, (f x).val ih1:P ι⊢ (∑ x, f x).val i = ∑ x, (f x).val i
All goals completed! 🐙Basis
A basis in Lean is typically represented by Module.Basis ι R M: an indexed
family of vectors in an R-module M such that every element of M has a
unique finite linear expansion in those vectors. The index type ι names the
basis vectors, and the map basis.repr gives the coordinate representation of a
vector with respect to that basis.
For inner product spaces, Lean also has OrthonormalBasis ι R M. This is a
basis whose vectors are orthonormal, packaged together with a linear isometric
equivalence between M and its coordinate space. It can be coerced to the
underlying Module.Basis using basis.toBasis when only the linear-algebraic
basis structure is needed.
The standard basis below is indexed by Fin d, so the basis vector basis i
is the unit vector in the ith coordinate direction of Space d.
lemma apply_eq_basis_repr_apply {d} (p : Space d) (i : Fin d) :
p i = basis.repr p i := d:ℕp:Space di:Fin d⊢ p.val i = (basis.repr p).ofLp i
All goals completed! 🐙@[simp]
lemma basis_repr_apply {d} (p : Space d) (i : Fin d) :
basis.repr p i = p i := d:ℕp:Space di:Fin d⊢ (basis.repr p).ofLp i = p.val i
All goals completed! 🐙@[simp]
lemma basis_repr_symm_apply {d} (v : EuclideanSpace ℝ (Fin d)) (i : Fin d) :
basis.repr.symm v i = v i := d:ℕv:EuclideanSpace ℝ (Fin d)i:Fin d⊢ (basis.repr.symm v).val i = v.ofLp i All goals completed! 🐙lemma basis_apply {d} (i j : Fin d) :
basis i j = if i = j then 1 else 0 := d:ℕi:Fin dj:Fin d⊢ (basis i).val j = if i = j then 1 else 0
All goals completed! 🐙@[simp]
lemma basis_self {d} (i : Fin d) : basis i i = 1 := d:ℕi:Fin d⊢ (basis i).val i = 1
All goals completed! 🐙@[simp high]
lemma inner_basis {d} (p : Space d) (i : Fin d) :
inner ℝ p (basis i) = p i := d:ℕp:Space di:Fin d⊢ inner ℝ p (basis i) = p.val i
All goals completed! 🐙@[simp high]
lemma basis_inner {d} (i : Fin d) (p : Space d) :
inner ℝ (basis i) p = p i := d:ℕi:Fin dp:Space d⊢ inner ℝ (basis i) p = p.val i
All goals completed! 🐙lemma basis_repr_inner_eq {d} (p : Space d) (v : EuclideanSpace ℝ (Fin d)) :
⟪basis.repr p, v⟫_ℝ = ⟪p, basis.repr.symm v⟫_ℝ :=
LinearIsometryEquiv.inner_map_eq_flip basis.repr p vinstance {d : ℕ} : FiniteDimensional ℝ (Space d) :=
Module.Basis.finiteDimensional_of_finite (h := basis.toBasis)@[simp]
lemma finrank_eq_dim {d : ℕ} : Module.finrank ℝ (Space d) = d := d:ℕ⊢ Module.finrank ℝ (Space d) = d
All goals completed! 🐙@[simp]
lemma rank_eq_dim {d : ℕ} : Module.rank ℝ (Space d) = d := d:ℕ⊢ Module.rank ℝ (Space d) = ↑d
All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙d:ℕP:Space d → Prophb:∀ (i : Fin d), P (basis i)hzero:P 0hadd:∀ (p1 p2 : Space d), P p1 → P p2 → P (p1 + p2)hsmul:∀ (c : ℝ) (p : Space d), P p → P (c • p)p:Space d⊢ P (∑ i, (basis.repr p).ofLp i • basis i)
All goals completed! 🐙Coordinates
lemma coord_apply (μ : Fin d) (p : Space d) :
coord μ p = p μ := d:ℕμ:Fin dp:Space d⊢ coord μ p = p.val μ
All goals completed! 🐙@[fun_prop]
lemma coord_contDiff {i} : ContDiff ℝ ∞ (fun x : Space d => x.coord i) :=
(coordCLM i).contDifflemma coordCLM_apply (μ : Fin d) (p : Space d) :
coordCLM μ p = coord μ p := d:ℕμ:Fin dp:Space d⊢ (coordCLM μ) p = coord μ p
All goals completed! 🐙@[inherit_doc coord]
scoped notation "𝔁" => coord@[fun_prop]
lemma eval_continuous {d} (i : Fin d) :
Continuous (fun p : Space d => p i) := d:ℕi:Fin d⊢ Continuous fun p => p.val i
d:ℕi:Fin dx✝:Space d⊢ x✝.val i = (coordCLM i) x✝
All goals completed! 🐙@[fun_prop]
lemma eval_differentiable {d} (i : Fin d) :
Differentiable ℝ (fun p : Space d => p i) := d:ℕi:Fin d⊢ Differentiable ℝ fun p => p.val i
d:ℕi:Fin dx✝:Space d⊢ x✝.val i = (coordCLM i) x✝
All goals completed! 🐙@[fun_prop]
lemma eval_contDiff {d n} (i : Fin d) :
ContDiff ℝ n (fun p : Space d => p i) := d:ℕn:ℕ∞ωi:Fin d⊢ ContDiff ℝ n fun p => p.val i
d:ℕn:ℕ∞ωi:Fin dx✝:Space d⊢ x✝.val i = (coordCLM i) x✝
All goals completed! 🐙Basic differentiablity conditions
@[fun_prop]
lemma mk_continuous {d : ℕ} :
Continuous (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.continuous@[fun_prop]
lemma mk_differentiable {d : ℕ} :
Differentiable ℝ (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.differentiable@[fun_prop]
lemma mk_contDiff {d : ℕ} {n : WithTop ℕ∞}:
ContDiff ℝ n (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.contDiffAll goals completed! 🐙All goals completed! 🐙d:ℕp:Space dy:Space di:Fin dh:(fun p => p.val i) = ⇑(coordCLM i)⊢ (coordCLM i) y = y.val i
All goals completed! 🐙@[fun_prop]
lemma contDiffOn_vadd (s : Space d) :
ContDiffOn ℝ ω (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) Set.univ :=
contDiffOn_univ.mpr <| fun_comp (mk_contDiff (n := ω)) (d:ℕs:Space d⊢ ContDiff ℝ ω fun v i => v.ofLp i + s.val i All goals completed! 🐙)@[fun_prop]
lemma vadd_differentiable {d} (s : Space d) :
Differentiable ℝ (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) :=
mk_differentiable.comp <| d:ℕs:Space d⊢ Differentiable ℝ fun v i => v.ofLp i + s.val i All goals completed! 🐙@[fun_prop]
lemma contDiffOn_vsub (s1 : Space d) :
ContDiffOn ℝ ω (fun (s : Space d) => s -ᵥ s1) Set.univ :=
contDiffOn_univ.mpr <| fun_comp (PiLp.contDiff_toLp) (d:ℕs1:Space d⊢ ContDiff ℝ ω fun s i => s.val i - s1.val i All goals completed! 🐙)@[fun_prop]
lemma vsub_differentiable {d} (s1 : Space d) :
Differentiable ℝ (fun (s : Space d) => s -ᵥ s1) :=
(PiLp.contDiff_toLp.differentiable (NeZero.ne' 2).symm).comp (d:ℕs1:Space d⊢ Differentiable ℝ fun s i => s.val i - s1.val i All goals completed! 🐙)M:Type u_1d:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin df:M → Space dhf:Differentiable ℝ fm:Mdm:M⊢ ((fderiv ℝ f m) dm).val μ = (coordCLM μ) ((fderiv ℝ (fun m' => f m') m) dm)
All goals completed! 🐙
M:Type u_1d:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin df:M → Space dhf:Differentiable ℝ fm:Mdm:M⊢ (fderiv ℝ (⇑(coordCLM μ) ∘ fun m' => f m') m) dm = (fderiv ℝ (fun m' => (f m').val μ) m) dm M:Type u_1d:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin df:M → Space dhf:Differentiable ℝ fm:Mdm:M⊢ (⇑(coordCLM μ) ∘ fun m' => f m') = fun m' => (f m').val μ
M:Type u_1d:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mμ:Fin df:M → Space dhf:Differentiable ℝ fm:Mdm:Mi:M⊢ (⇑(coordCLM μ) ∘ fun m' => f m') i = (f i).val μ
All goals completed! 🐙Directions
Notion of direction where unit returns a unit vector in the direction specified.
Unit vector specifying the direction.
structure Direction (d : ℕ := 3) where unit : Space d
norm : ‖unit‖ = 1d:ℕs:Direction d⊢ 1 ^ 2 = 1
All goals completed! 🐙One equiv
lemma oneEquiv_coe :
(oneEquiv : Space 1 → ℝ) = fun x => x 0 := ⊢ ⇑oneEquiv = fun x => x.val 0
All goals completed! 🐙lemma oneEquiv_symm_coe :
(oneEquiv.symm : ℝ → Space 1) = (fun x => ⟨fun _ => x⟩) := ⊢ ⇑oneEquiv.symm = fun x => { val := fun x_1 => x }
All goals completed! 🐙lemma oneEquiv_symm_apply (x : ℝ) (i : Fin 1) :
oneEquiv.symm x i = x := x:ℝi:Fin 1⊢ (oneEquiv.symm x).val i = x
All goals completed! 🐙lemma oneEquiv_continuous :
Continuous (oneEquiv : Space 1 → ℝ) := ⊢ Continuous ⇑oneEquiv
⊢ Continuous fun x => x.val 0
All goals completed! 🐙lemma oneEquiv_symm_continuous :
Continuous (oneEquiv.symm : ℝ → Space 1) := ⊢ Continuous ⇑oneEquiv.symm
⊢ Continuous fun x => { val := fun x_1 => x }
All goals completed! 🐙s:Set (Space 1)hs:MeasurableSet s⊢ MeasurableSet (⇑oneEquivCLE.symm ⁻¹' s)
All goals completed! 🐙s:Set ℝhs:MeasurableSet s⊢ MeasurableSet (⇑oneEquivCLE.symm.symm ⁻¹' s)
All goals completed! 🐙lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
LinearIsometryEquiv.measurePreserving oneEquivlemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume :=
LinearIsometryEquiv.measurePreserving oneEquiv.symmRelation to tangent space
@[simp]
lemma modelDiffeo_apply {d : ℕ} (p : Space d) :
modelDiffeo p = p := rflProperties of vadd with module structure
lemma norm_vadd_le_add {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
‖v +ᵥ s‖ ≤ ‖v‖ + ‖s‖ := d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖v +ᵥ s‖ ≤ ‖v‖ + ‖s‖
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖v +ᵥ s‖ ≤ ‖s - (-v +ᵥ 0)‖d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖s - (-v +ᵥ 0)‖ ≤ ‖v‖ + ‖s‖
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖v +ᵥ s‖ ≤ ‖s - (-v +ᵥ 0)‖ d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖v +ᵥ s‖ = ‖s - (-v +ᵥ 0)‖
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ v +ᵥ s = s - (-v +ᵥ 0)
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space di:Fin d⊢ (v +ᵥ s).val i = (s - (-v +ᵥ 0)).val i
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space di:Fin d⊢ v.ofLp i + s.val i = s.val i + v.ofLp i
All goals completed! 🐙
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖s - (-v +ᵥ 0)‖ ≤ ‖v‖ + ‖s‖ d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖s‖ + ‖-v +ᵥ 0‖ = ‖v‖ + ‖s‖
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space d⊢ ‖s‖ + ‖v‖ = ‖v‖ + ‖s‖
All goals completed! 🐙@[fun_prop]
lemma differentiable_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
Differentiable ℝ (fun (s : Space d) => v +ᵥ s) :=
mk_differentiable.comp <| d:ℕv:EuclideanSpace ℝ (Fin d)⊢ Differentiable ℝ fun s i => v.ofLp i + s.val i All goals completed! 🐙d:ℕv:EuclideanSpace ℝ (Fin d)s:Space dds:Space di:Fin d⊢ (fderiv ℝ (fun m' => (v +ᵥ m').val i) s) ds = ((ContinuousLinearMap.id ℝ (Space d)) ds).val id:ℕv:EuclideanSpace ℝ (Fin d)s:Space dds:Space di:Fin d⊢ Differentiable ℝ fun s => v +ᵥ s
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space dds:Space di:Fin d⊢ (fderiv ℝ (fun m' => (v +ᵥ m').val i) s) ds = ((ContinuousLinearMap.id ℝ (Space d)) ds).val i All goals completed! 🐙
d:ℕv:EuclideanSpace ℝ (Fin d)s:Space dds:Space di:Fin d⊢ Differentiable ℝ fun s => v +ᵥ s All goals completed! 🐙@[fun_prop]
lemma vadd_hasTemperateGrowth {d} (v : EuclideanSpace ℝ (Fin d)) :
Function.HasTemperateGrowth (fun s : Space d => v +ᵥ s) := d:ℕv:EuclideanSpace ℝ (Fin d)⊢ Function.HasTemperateGrowth fun s => v +ᵥ s
d:ℕv:EuclideanSpace ℝ (Fin d)⊢ Function.HasTemperateGrowth (fderiv ℝ fun s => v +ᵥ s)d:ℕv:EuclideanSpace ℝ (Fin d)⊢ Differentiable ℝ fun s => v +ᵥ sd:ℕv:EuclideanSpace ℝ (Fin d)⊢ ∀ (x : Space d), ‖v +ᵥ x‖ ≤ (1 + ‖v‖) * (1 + ‖x‖) ^ 1
d:ℕv:EuclideanSpace ℝ (Fin d)⊢ Function.HasTemperateGrowth (fderiv ℝ fun s => v +ᵥ s) All goals completed! 🐙
d:ℕv:EuclideanSpace ℝ (Fin d)⊢ Differentiable ℝ fun s => v +ᵥ s All goals completed! 🐙
d:ℕv:EuclideanSpace ℝ (Fin d)⊢ ∀ (x : Space d), ‖v +ᵥ x‖ ≤ (1 + ‖v‖) * (1 + ‖x‖) ^ 1 d:ℕv:EuclideanSpace ℝ (Fin d)x:Space d⊢ ‖v +ᵥ x‖ ≤ (1 + ‖v‖) * (1 + ‖x‖) ^ 1
d:ℕv:EuclideanSpace ℝ (Fin d)x:Space d⊢ ‖v +ᵥ x‖ ≤ (1 + ‖v‖) * (1 + ‖x‖)
d:ℕv:EuclideanSpace ℝ (Fin d)x:Space d⊢ ‖v‖ + ‖x‖ ≤ (1 + ‖v‖) * (1 + ‖x‖)
All goals completed! 🐙