Update diffOp.lean
This commit is contained in:
parent
5bd004d653
commit
789c1100bc
@ -5,7 +5,7 @@ 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
|
||||
of E a linear evaluation
|
||||
|
||||
{Continuous 𝕜-multilinear maps E → F in n variables} → G
|
||||
|
||||
@ -22,7 +22,7 @@ fun e ↦ D e (iteratedFDeriv 𝕜 n f e)
|
||||
-/
|
||||
|
||||
@[ext]
|
||||
class HomLinDiffOp
|
||||
class HomLinDiffOp
|
||||
(𝕜 : Type*) [NontriviallyNormedField 𝕜]
|
||||
(n : ℕ)
|
||||
(E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E]
|
||||
@ -59,13 +59,13 @@ noncomputable def Laplace
|
||||
|
||||
exact {
|
||||
toFun := fun f' ↦ ∑ i, f' ![v i, v i]
|
||||
map_add' := by
|
||||
map_add' := by
|
||||
intro f₁ f₂
|
||||
exact Finset.sum_add_distrib
|
||||
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
|
||||
cont := by
|
||||
simp
|
||||
apply continuous_finset_sum
|
||||
intro i _
|
||||
@ -86,13 +86,13 @@ noncomputable def Gradient
|
||||
|
||||
exact {
|
||||
toFun := fun f' ↦ ∑ i, (f' ![v i]) • (v i)
|
||||
map_add' := by
|
||||
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
|
||||
cont := by
|
||||
simp
|
||||
apply continuous_finset_sum
|
||||
intro i _
|
||||
|
Loading…
Reference in New Issue
Block a user