73 lines
2.1 KiB
Plaintext
73 lines
2.1 KiB
Plaintext
import Mathlib.Analysis.InnerProductSpace.Basic
|
||
import Mathlib.Analysis.InnerProductSpace.PiL2
|
||
import Mathlib.Algebra.BigOperators.Basic
|
||
import Mathlib.Analysis.Calculus.ContDiff.Bounds
|
||
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
|
||
|
||
open BigOperators
|
||
open Finset
|
||
|
||
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
|
||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
|
||
|
||
#check EuclideanSpace.norm_eq
|
||
#check EuclideanSpace.dist_eq
|
||
|
||
|
||
noncomputable def Laplace₁ (n : ℕ) (f : EuclideanSpace ℝ (Fin n) → F) : EuclideanSpace ℝ (Fin n) → F := by
|
||
let e : Fin n → EuclideanSpace ℝ (Fin n) := fun i ↦ EuclideanSpace.single i (1 : ℝ)
|
||
exact fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![e i, e i]
|
||
|
||
|
||
noncomputable def Laplace₂
|
||
[Fintype ι]
|
||
(v : Basis ι ℝ E)
|
||
(hv : Orthonormal ℝ v)
|
||
(f : E → F) :
|
||
E → F :=
|
||
fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
|
||
|
||
#check ContinuousMultilinearMap.map_sum_finset
|
||
|
||
theorem LaplaceIndep
|
||
[Fintype ι]
|
||
(v₁ : Basis ι ℝ E)
|
||
(hv₁ : Orthonormal ℝ v₁)
|
||
(v₂ : Basis ι ℝ E)
|
||
(hv₂ : Orthonormal ℝ v₂)
|
||
(f : E → F) :
|
||
∑ i, iteratedFDeriv ℝ 2 f z ![v₁ i, v₁ i] = ∑ i, iteratedFDeriv ℝ 2 f z ![v₂ i, v₂ i] := by
|
||
|
||
have (v : E) : v = ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j) :=
|
||
sorry
|
||
|
||
conv =>
|
||
right
|
||
arg 2
|
||
intro i
|
||
rw [this (v₂ i)]
|
||
rw [this (v₂ i)]
|
||
conv =>
|
||
right
|
||
arg 2
|
||
intro i
|
||
--rw [ContinuousMultilinearMap.map_sum_finset]
|
||
|
||
have v : E := by sorry
|
||
let t := ![∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j), ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j)]
|
||
simp at t
|
||
have L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F := by exact iteratedFDeriv ℝ 2 f z
|
||
--have α : Fin 2 → Type* := by exact fun _ ↦ ι
|
||
have g : (i : Fin 2) → ι → E := by exact fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j))
|
||
have A : (i : Fin 2) → Finset ι := by exact fun _ ↦ Finset.univ
|
||
|
||
let X := ContinuousMultilinearMap.map_sum
|
||
(iteratedFDeriv ℝ 2 f z)
|
||
(fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
|
||
|
||
--
|
||
-- (fun _ ↦ Finset.univ)
|
||
simp at X
|
||
|
||
sorry
|