feat: Properties of vadd

.codespellignore

@@ -9,3 +9,4 @@ Breal
 ket
 rIn
 FRO
+Commun

PhysLean/SpaceAndTime/Space/Basic.lean

@@ -12,6 +12,7 @@ public import Mathlib.Topology.ContinuousMap.CompactlySupported
 public import Mathlib.Geometry.Manifold.IsManifold.Basic
 public import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
 public import Mathlib.Analysis.InnerProductSpace.Calculus
+public import Mathlib.Geometry.Manifold.Diffeomorph
 /-!
 
 # Space
@@ -288,4 +289,34 @@ noncomputable def manifoldStructure (d : ℕ) :
     simp only [Equiv.coe_vaddConst]
     fun_prop
 
+@[simp]
+lemma manifoldStructure_comp_manifoldStructure_symm {d : ℕ} :
+    (↑(manifoldStructure d) ∘ ↑(manifoldStructure d).symm) = id := by
+  ext1 x
+  simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+
+lemma manifoldStructure_comp_manifoldStructure_symm_apply {d : ℕ}
+    (x : EuclideanSpace ℝ (Fin d)) :
+    (manifoldStructure d) ((manifoldStructure d).symm x) = x := by
+  simpa using (manifoldStructure d).right_inv' (x := x) (by simp [manifoldStructure])
+
+@[simp]
+lemma range_manifoldStructure {d : ℕ} :
+    (Set.range ↑(manifoldStructure d)) = Set.univ := by
+  ext x
+  simpa using ⟨(manifoldStructure d).symm x, manifoldStructure_comp_manifoldStructure_symm_apply x⟩
+
+open Manifold in
+lemma contMDiff_vaddConst (d : ℕ) : ContMDiff
+    (manifoldStructure d) (𝓘(ℝ, EuclideanSpace ℝ (Fin d)))  ⊤ (manifoldStructure d).toFun := by
+  rw [contMDiff_iff]
+  refine ⟨(manifoldStructure d).continuous_toFun, fun x y ↦ ?_⟩
+  simp only [extChartAt, OpenPartialHomeomorph.extend, OpenPartialHomeomorph.refl_partialEquiv,
+    PartialEquiv.refl_source, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq,
+    modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialEquiv.refl_coe,
+    ModelWithCorners.toPartialEquiv_coe, PartialEquiv.refl_trans,
+    ModelWithCorners.toPartialEquiv_coe_symm, manifoldStructure_comp_manifoldStructure_symm,
+    CompTriple.comp_eq, ModelWithCorners.target_eq, Set.preimage_univ, Set.inter_univ]
+  exact contDiffOn_id
+
 end Space

PhysLean/SpaceAndTime/Space/Derivatives/Basic.lean

@@ -104,6 +104,45 @@ lemma deriv_eq_mfderiv {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
   rw [deriv_eq_fderiv_basis, ← mfderiv_eq_fderiv]
   rfl
 
+open Manifold in
+lemma mdifferentiable_manifoldStructure_iff_differentiable {M d} [NormedAddCommGroup M]
+    [NormedSpace ℝ M] {f : Space d → M} {x : Space d} :
+    MDifferentiableAt (Space.manifoldStructure d) 𝓘(ℝ, M) f x ↔ DifferentiableAt ℝ f x := by
+  constructor
+  · intro h
+    rw [← mdifferentiableAt_iff_differentiableAt]
+    apply h.comp (I' := Space.manifoldStructure d)
+    exact (modelDiffeo.symm.mdifferentiable  (WithTop.top_ne_zero)).mdifferentiableAt
+  · intro h
+    apply (mdifferentiableAt_iff_differentiableAt.mpr h).comp (I' := 𝓘(ℝ, Space d))
+    exact (modelDiffeo.mdifferentiable  (WithTop.top_ne_zero)).mdifferentiableAt
+
+
+TODO "3XMN6" "Make the version of the derivative described through
+  `deriv_eq_mfderiv_manifoldStructure` the definition of `deriv` and prove the
+  equivalence with the current definition, under suitable conditions."
+
+open Manifold in
+/-- The spatial-derivative in terms of the derivative of functions between
+  manifolds with the manifold structure `Space.manifoldStructure d`. -/
+lemma deriv_eq_mfderiv_manifoldStructure {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
+    (μ : Fin d) (f : Space d → M) (x : Space d) :
+    deriv μ f x = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M) f x (EuclideanSpace.single μ 1) := by
+  by_cases hf : DifferentiableAt ℝ f x
+  · rw [deriv_eq_mfderiv]
+    change _ = mfderiv (Space.manifoldStructure d) 𝓘(ℝ, M)
+      (f ∘ modelDiffeo) x (EuclideanSpace.single μ 1)
+    rw [mfderiv_comp (I' := 𝓘(ℝ, Space d)) _ hf.mdifferentiableAt
+      (modelDiffeo.mdifferentiable WithTop.top_ne_zero).mdifferentiableAt]
+    simp only [Function.comp_apply, modelDiffeo_apply, mfderiv_eq_fderiv,
+      ContinuousLinearMap.coe_comp']
+    rw [basis_eq_mfderiv_modelDiffeo_single]
+    rfl
+  · rw [deriv_eq, fderiv_zero_of_not_differentiableAt hf,
+      mfderiv_zero_of_not_mdifferentiableAt <|
+      mdifferentiable_manifoldStructure_iff_differentiable.mp.mt hf]
+    simp
+
 /-!
 
 ### A.2. Derivative of the constant function

PhysLean/SpaceAndTime/Space/Module.lean

@@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
 module
 
 public import PhysLean.SpaceAndTime.Space.Basic
+public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Analysis.Distribution.TemperateGrowth
 /-!
 
 # The structure of a module on Space
@@ -474,6 +476,12 @@ def equivPi (d : ℕ) :
     invFun := fun f => ⟨f⟩
   }
 
+/-!
+
+## Basic differentiablity conditions
+
+-/
+
 @[fun_prop]
 lemma mk_continuous {d : ℕ} :
     Continuous (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.continuous
@@ -483,20 +491,54 @@ lemma mk_differentiable {d : ℕ} :
     Differentiable ℝ (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.differentiable
 
 @[fun_prop]
-lemma mk_contDiff {d n : ℕ} :
+lemma mk_contDiff {d  : ℕ} {n : WithTop ℕ∞}:
     ContDiff ℝ n (fun (f : Fin d → ℝ) => (⟨f⟩ : Space d)) := (equivPi d).symm.contDiff
 
 @[simp]
 lemma fderiv_mk {d : ℕ} (f : Fin d → ℝ) :
     fderiv ℝ Space.mk f = (equivPi d).symm := by
   change fderiv ℝ (equivPi d).symm f = _
-  rw [@ContinuousLinearEquiv.fderiv]
+  rw [ContinuousLinearEquiv.fderiv]
 
 @[simp]
 lemma fderiv_val {d : ℕ} (p : Space d) :
     fderiv ℝ Space.val p = (equivPi d) := by
   change fderiv ℝ (equivPi d) p = _
-  rw [@ContinuousLinearEquiv.fderiv]
+  rw [ContinuousLinearEquiv.fderiv]
+
+@[fun_prop]
+lemma contDiffOn_vadd (s : Space d) :
+    ContDiffOn ℝ ω (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) Set.univ := by
+  rw [contDiffOn_univ]
+  refine fun_comp ?_ ?_
+  · exact mk_contDiff (n := ω)
+  · fun_prop
+
+@[fun_prop]
+lemma vadd_differentiable {d} (s : Space d) :
+    Differentiable ℝ (fun (v : EuclideanSpace ℝ (Fin d)) => v +ᵥ s) :=
+  mk_differentiable.comp <| by fun_prop
+
+@[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) (by fun_prop)
+
+@[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 (by fun_prop)
+
+lemma fderiv_space_components {M d} [NormedAddCommGroup M] [NormedSpace ℝ M]
+    (μ : Fin d) (f : M → Space d) (hf : Differentiable ℝ f) (m dm : M):
+    fderiv ℝ f m dm μ  = fderiv ℝ (fun m' => f m' μ) m dm := by
+  trans fderiv ℝ (Space.coordCLM μ ∘ fun m' => f m') m dm
+  · rw [fderiv_comp _ (by fun_prop) (by fun_prop), ContinuousLinearMap.fderiv,
+      ContinuousLinearMap.coe_comp', Function.comp_apply]
+    simp [coordCLM, coord_apply]
+  · congr
+    ext i
+    simp [coordCLM, coord_apply]
 
 /-!
 
@@ -604,4 +646,104 @@ lemma oneEquiv_measurePreserving : MeasurePreserving oneEquiv volume volume :=
 lemma oneEquiv_symm_measurePreserving : MeasurePreserving oneEquiv.symm volume volume := by
   exact LinearIsometryEquiv.measurePreserving oneEquiv.symm
 
+/-!
+
+## Relation to tangent space
+
+-/
+
+open Manifold in
+/-- A diffeomorphism between the two different manifold structures on `Space d`,
+  that equivalent to `manifoldStructure d` and that equivalent to `𝓘(ℝ, Space d)` -/
+noncomputable def modelDiffeo {d} :
+    Diffeomorph (manifoldStructure d) 𝓘(ℝ, Space d) (Space d) (Space d) ⊤ where
+  toFun p :=  p
+  invFun p :=  p
+  left_inv _ := rfl
+  right_inv _ := rfl
+  contMDiff_toFun := by
+    refine contMDiff_iff.mpr ⟨continuous_id', fun x y => ?_⟩
+    simp [manifoldStructure]
+    fun_prop
+  contMDiff_invFun := by
+    refine contMDiff_iff.mpr ⟨continuous_id', fun x y => ?_⟩
+    simp [manifoldStructure]
+    fun_prop
+
+@[simp]
+lemma modelDiffeo_apply (p : Space d) :
+    modelDiffeo p = p := rfl
+
+open Manifold in
+/-- The derivative of `modelDiffeo` provides an equivalence between
+  `Space d` and `EuclideanSpace ℝ (Fin d)`. This equivalences takes the basis
+  of `EuclideanSpace ℝ (Fin d)` to the basis of `Space d`, and vice versa. -/
+lemma basis_eq_mfderiv_modelDiffeo_single (d : ℕ) (μ : Fin d) (x : Space d) :
+    basis μ = mfderiv (manifoldStructure d) 𝓘(ℝ, Space d) (modelDiffeo (d := d)) x
+      (EuclideanSpace.single μ 1) := by
+  simp [mfderiv]
+  rw [if_pos (modelDiffeo.mdifferentiable (WithTop.top_ne_zero)).mdifferentiableAt]
+  change _ = fderiv ℝ (manifoldStructure d).symm (manifoldStructure d x) (EuclideanSpace.single μ 1)
+  simp [manifoldStructure]
+  ext i
+  rw [fderiv_space_components _ _ (by fun_prop)]
+  simp only [vadd_apply, fderiv_add_const]
+  change _ = fderiv ℝ (EuclideanSpace.proj i) (x -ᵥ Classical.choice _) (EuclideanSpace.single μ 1)
+  simp [basis_apply]
+  congr 1
+  exact Eq.propIntro (fun a => Eq.symm a) fun a => (Eq.symm a)
+
+
+/-!
+
+## Properties of vadd with module structure
+
+-/
+
+lemma norm_vadd_le_add {d} (v : EuclideanSpace ℝ (Fin d)) (s : Space d) :
+    ‖v +ᵥ s‖ ≤ ‖v‖ + ‖s‖ := by
+  trans ‖s - (-v +ᵥ (0 : Space d))‖
+  · apply le_of_eq
+    congr
+    ext i
+    simp only [vadd_apply, sub_apply, PiLp.neg_apply, zero_apply, add_zero, sub_neg_eq_add]
+    ring
+  · apply (norm_sub_le _ _).trans <| le_of_eq _
+    simp only [norm_vadd_zero, norm_neg]
+    ring
+
+@[fun_prop]
+lemma differentiable_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
+    Differentiable ℝ (fun (s : Space d) => v +ᵥ s) :=
+  mk_differentiable.comp <| by fun_prop
+
+@[simp]
+lemma fderiv_vadd {d} (v : EuclideanSpace ℝ (Fin d)) :
+    fderiv ℝ (fun s => v +ᵥ s) = fun (_ : Space d) => ContinuousLinearMap.id ℝ _ := by
+  ext s ds i
+  change fderiv ℝ (fun s => v +ᵥ s) s ds i = _
+  rw [fderiv_space_components]
+  simp
+  trans fderiv ℝ (coordCLM i) s ds
+  · congr
+    ext j
+    simp [coordCLM, coord_apply]
+  · rw [ContinuousLinearMap.fderiv]
+    simp [coordCLM, coord_apply]
+  · fun_prop
+
+@[fun_prop]
+lemma vadd_hasTemperateGrowth {d} (v : EuclideanSpace ℝ (Fin d)) :
+    Function.HasTemperateGrowth (fun s : Space d => v +ᵥ s) := by
+  apply Function.HasTemperateGrowth.of_fderiv (k := 1) (C := 1 + ‖v‖)
+  · rw [fderiv_vadd]
+    simp
+  · fun_prop
+  · intro x
+    simp
+    apply (norm_vadd_le_add _ _).trans
+    have : 0 ≤ ‖v‖ := by positivity
+    have : 0 ≤ ‖x‖ := by positivity
+    nlinarith
+
 end Space