Merge branch 'main' into SL-wedge-product

DeRhamCohomology/ContinuousAlternatingMap/Curry.lean

@@ -86,6 +86,21 @@ theorem uncurryFin_uncurryFinCLM_comp_of_symmetric {f : E →L[𝕜] E →L[𝕜
     Fin.succAbove_succAbove_predAbove, Fin.neg_one_pow_succAbove_add_predAbove, pow_succ',
     neg_one_mul, neg_smul, Fin.removeNth_apply, add_neg_cancel]
 
+/- Interior product -/
+def curryFin (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F :=
+  LinearMap.mkContinuous
+    { toFun := fun x =>
+        { toContinuousMultilinearMap := f.1.curryLeft x
+          map_eq_zero_of_eq' := fun v i j hv hne ↦ by
+            apply f.map_eq_zero_of_eq (Fin.cons x v) (i := i.succ) (j := j.succ) <;> simpa }
+      map_add' := fun x y => by ext; simp
+      map_smul' := fun c x => by ext; simp }
+    ‖f‖ fun x => by
+      rw [LinearMap.coe_mk, AddHom.coe_mk, ← norm_toContinuousMultilinearMap]
+      dsimp
+      refine ContinuousLinearMap.le_of_opNorm_le f.curryLeft ?_ x
+      apply le_of_eq
+      exact ContinuousMultilinearMap.curryLeft_norm f.toContinuousMultilinearMap
 
 variable [DecidableEq ι] [DecidableEq ι']
 

DeRhamCohomology/DifferentialForm.lean

@@ -59,6 +59,18 @@ def constOfIsEmpty (x : F) : Ω^0⟮E, F⟯ :=
 def ederiv (ω : Ω^n⟮E, F⟯) : Ω^n + 1⟮E, F⟯ :=
   fun x ↦ .uncurryFin (fderiv ℝ ω x)
 
+theorem ederiv_add (ω₁ ω₂ : Ω^n⟮E, F⟯) {x : E} (hω₁ : DifferentiableAt ℝ ω₁ x)
+    (hω₂ : DifferentiableAt ℝ ω₂ x) : ederiv (ω₁ + ω₂) x = ederiv ω₁ x + ederiv ω₂ x := by
+  simp [ederiv, fderiv_add' hω₁ hω₂, uncurryFin_add]
+
+theorem ederiv_smul (ω : Ω^n⟮E, F⟯) (c : ℝ) {x : E} (hω : DifferentiableAt ℝ ω x):
+    ederiv (c • ω) x = c • ederiv ω x := by
+  simp [ederiv, fderiv_const_smul' hω, uncurryFin_smul]
+
+theorem ederiv_constOfIsEmpty (x : E) (y : F) :
+    ederiv (constOfIsEmpty y) x = .uncurryFin (fderiv ℝ (constOfIsEmpty y) x) :=
+  rfl
+
 theorem Filter.EventuallyEq.ederiv_eq {ω₁ ω₂ : Ω^n⟮E, F⟯} {x : E}
     (h : ω₁ =ᶠ[𝓝 x] ω₂) : ederiv ω₁ x = ederiv ω₂ x := by
   ext v