105 lines
3.0 KiB
Plaintext
105 lines
3.0 KiB
Plaintext
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
|