chore(Analysis/InnerProductSpace): the Laplacian is k-linear (leanprover-community#33739)

Author: mcdoll

Mathlib/Analysis/InnerProductSpace/Laplacian.lean

@@ -114,8 +114,9 @@ end secondDerivativeAPI
 -/
 
 variable
+  {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedAlgebra ℝ 𝕜]
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
-  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [IsScalarTower ℝ 𝕜 F]
   {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
   {f f₁ f₂ : E → F} {x : E} {s : Set E}
 
@@ -259,7 +260,7 @@ theorem laplacian_congr_nhds (h : f₁ =ᶠ[𝓝 x] f₂) :
   simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, hx]
 
 /-!
-## ℝ-Linearity of Δ on Continuously Differentiable Functions
+## 𝕜-Linearity of Δ on Continuously Differentiable Functions
 -/
 
 /-- The Laplacian commutes with addition. -/
@@ -292,27 +293,27 @@ theorem _root_.ContDiffAt.laplacian_add_nhds (h₁ : ContDiffAt ℝ 2 f₁ x) (h
   exact h₁x.laplacian_add h₂x
 
 /-- The Laplacian commutes with scalar multiplication. -/
-theorem laplacianWithin_smul (v : ℝ) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s)
+theorem laplacianWithin_smul (v : 𝕜) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s)
     (hx : x ∈ s) :
     (Δ[s] (v • f)) x = v • (Δ[s] f) x := by
   simp [laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis _ hs hx,
     iteratedFDerivWithin_const_smul_apply hf hs hx,
     Finset.smul_sum]
 
 /-- The Laplacian commutes with scalar multiplication. -/
-theorem laplacian_smul (v : ℝ) (hf : ContDiffAt ℝ 2 f x) : Δ (v • f) x = v • (Δ f) x := by
+theorem laplacian_smul (v : 𝕜) (hf : ContDiffAt ℝ 2 f x) : Δ (v • f) x = v • (Δ f) x := by
   simp [laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, iteratedFDeriv_const_smul_apply hf,
     Finset.smul_sum]
 
 /-- The Laplacian commutes with scalar multiplication. -/
 theorem laplacianWithin_smul_nhds
-    (v : ℝ) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) :
+    (v : 𝕜) (hf : ContDiffWithinAt ℝ 2 f s x) (hs : UniqueDiffOn ℝ s) :
     Δ[s] (v • f) =ᶠ[𝓝[s] x] v • (Δ[s] f) := by
   filter_upwards [(hf.eventually (by simp)).filter_mono (nhdsWithin_mono _ (Set.subset_insert ..)),
     eventually_mem_nhdsWithin] with a h₁a using laplacianWithin_smul v h₁a hs
 
 /-- The Laplacian commutes with scalar multiplication. -/
-theorem laplacian_smul_nhds (v : ℝ) (h : ContDiffAt ℝ 2 f x) :
+theorem laplacian_smul_nhds (v : 𝕜) (h : ContDiffAt ℝ 2 f x) :
     Δ (v • f) =ᶠ[𝓝 x] v • (Δ f) := by
   filter_upwards [h.eventually (by simp)] with a ha
   simp [laplacian_smul v ha]