feat: Frénet moving frame and Frénet equation for plane curves

Mathlib.lean

@@ -4472,6 +4472,7 @@ public import Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
 public import Mathlib.Geometry.Manifold.VectorField.LieBracket
 public import Mathlib.Geometry.Manifold.VectorField.Pullback
 public import Mathlib.Geometry.Manifold.WhitneyEmbedding
+public import Mathlib.Geometry.PlaneCurves
 public import Mathlib.Geometry.Polygon.Basic
 public import Mathlib.Geometry.RingedSpace.Basic
 public import Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Mathlib/Analysis/Calculus/Deriv/Prod.lean

@@ -7,6 +7,8 @@ module
 
 public import Mathlib.Analysis.Calculus.Deriv.Basic
 public import Mathlib.Analysis.Calculus.FDeriv.Prod
+public import Mathlib.Analysis.Calculus.FDeriv.WithLp
+public import Mathlib.Analysis.InnerProductSpace.PiL2
 
 /-!
 # Derivatives of functions taking values in product types
@@ -98,6 +100,23 @@ theorem deriv_pi (h : ∀ i, DifferentiableAt 𝕜 (fun x => φ x i) x) :
   simp only [deriv, fderiv_pi h]
   simp
 
+theorem hasDerivWithinAt_pi_piLp [Fintype ι] {p : ENNReal} [Fact (1 ≤ p)] {f : 𝕜 → PiLp p E'}
+  {f' : PiLp p E'} {s : Set 𝕜} {x : 𝕜} :
+    HasDerivWithinAt f f' s x ↔ ∀ i, HasDerivWithinAt (fun t ↦ f t i) (f' i) s x := by
+  have := Fintype.ofFinite ι
+  have hd : HasDerivWithinAt f f' s x ↔ HasFDerivWithinAt f (ContinuousLinearMap.smulRight
+                 (1 : 𝕜 →L[𝕜] 𝕜) f') s x := hasDerivWithinAt_iff_hasFDerivWithinAt
+  rw [hd, hasFDerivWithinAt_piLp]
+  congr! 3
+
+theorem hasDerivWithinAt_pi_euclidean [Fintype ι] {f : 𝕜 → EuclideanSpace 𝕜 ι}
+  {f' : EuclideanSpace 𝕜 ι} {s : Set 𝕜} {x : 𝕜} :
+    HasDerivWithinAt f f' s x ↔ ∀ i, HasDerivWithinAt (fun t ↦  f t i) (f' i) s x := by
+  have := Fintype.ofFinite ι
+  convert hasDerivWithinAt_pi_piLp using 1
+  · infer_instance
+  · exact ⟨by norm_num⟩
+
 end Pi