Add file

Nevanlinna/diffOp.lean

@@ -0,0 +1,104 @@
+import Mathlib.Analysis.Calculus.ContDiff.Basic
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+/-
+
+Let E, F, G be vector spaces over nontrivally normed field 𝕜, a homogeneus
+linear differential operator of order n is a map that attaches to every point e
+of E a linear evaluation 
+
+{Continuous 𝕜-multilinear maps E → F in n variables} → G
+
+In other words, homogeneus linear differential operator of order n is an
+instance of the type:
+
+D : E → (ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ E) F) →ₗ[𝕜] G
+
+Given any map f : E → F, one obtains a map D f : E → G by sending a point e to
+the evaluation (D e), applied to the n.th derivative of f at e
+
+fun e ↦ D e (iteratedFDeriv 𝕜 n f e)
+
+-/
+
+@[ext]
+class HomLinDiffOp 
+  (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+  (n : ℕ)
+  (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  (G : Type*) [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+where
+  tensorfield : E → ( E [×n]→L[𝕜] F) →L[𝕜] G
+--  tensorfield : E → (ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ E) F) →ₗ[𝕜] G
+
+
+namespace HomLinDiffOp
+
+noncomputable def toFun
+  {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+  {n : ℕ}
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+  (o : HomLinDiffOp 𝕜 n E F G)
+  : (E → F) → (E → G) :=
+  fun f z ↦ o.tensorfield z (iteratedFDeriv 𝕜 n f z)
+
+
+noncomputable def Laplace
+  {𝕜 : Type*} [RCLike 𝕜]
+  {n : ℕ}
+  : HomLinDiffOp 𝕜 2 (EuclideanSpace 𝕜 (Fin n)) 𝕜 𝕜
+  where
+  tensorfield := by
+    intro _
+
+    let v := stdOrthonormalBasis 𝕜 (EuclideanSpace 𝕜 (Fin n))
+    rw [finrank_euclideanSpace_fin] at v
+
+    exact {
+      toFun := fun f' ↦ ∑ i, f' ![v i, v i]
+      map_add' := by 
+        intro f₁ f₂
+        exact Finset.sum_add_distrib 
+      map_smul' := by
+        intro m f
+        exact Eq.symm (Finset.mul_sum Finset.univ (fun i ↦ f ![v i, v i]) m)
+      cont := by 
+        simp
+        apply continuous_finset_sum
+        intro i _
+        exact ContinuousMultilinearMap.continuous_eval_const ![v i, v i]
+    }
+
+
+noncomputable def Gradient
+  {𝕜 : Type*} [RCLike 𝕜]
+  {n : ℕ}
+  : HomLinDiffOp 𝕜 1 (EuclideanSpace 𝕜 (Fin n)) 𝕜 (EuclideanSpace 𝕜 (Fin n))
+  where
+  tensorfield := by
+    intro _
+
+    let v := stdOrthonormalBasis 𝕜 (EuclideanSpace 𝕜 (Fin n))
+    rw [finrank_euclideanSpace_fin] at v
+
+    exact {
+      toFun := fun f' ↦ ∑ i, (f' ![v i]) • (v i)
+      map_add' := by 
+        intro f₁ f₂
+        simp; simp_rw [add_smul, Finset.sum_add_distrib]
+      map_smul' := by
+        intro m f
+        simp; simp_rw [Finset.smul_sum, ←smul_assoc,smul_eq_mul]
+      cont := by 
+        simp
+        apply continuous_finset_sum
+        intro i _
+        apply Continuous.smul
+        exact ContinuousMultilinearMap.continuous_eval_const ![v i]
+        exact continuous_const
+    }
+
+end HomLinDiffOp