Update laplace2.lean

This commit is contained in:
Stefan Kebekus 2024-06-24 07:58:04 +02:00
parent d287c24453
commit adc0378e5d
1 changed files with 18 additions and 1 deletions

View File

@ -27,6 +27,8 @@ noncomputable def Laplace₂
E → F :=
fun z ↦ ∑ i, iteratedFDeriv 2 f z ![v i, v i]
#check ContinuousMultilinearMap.map_sum_finset
theorem LaplaceIndep
[Fintype ι]
(v₁ : Basis ι E)
@ -49,5 +51,20 @@ theorem LaplaceIndep
right
arg 2
intro i
rw [ContinuousMultilinearMap.map_sum_finset]
--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_finset
(iteratedFDeriv 2 f z)
(fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ • (v₁ j)))
(fun _ ↦ Finset.univ)
simp at X
sorry