Compare commits

...

2 Commits

Author SHA1 Message Date
Stefan Kebekus ecdc182f2b Update laplace2.lean 2024-06-24 08:03:39 +02:00
Stefan Kebekus adc0378e5d Update laplace2.lean 2024-06-24 07:58:04 +02:00
1 changed files with 20 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,22 @@ 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
(iteratedFDeriv 2 f z)
(fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ • (v₁ j)))
--
-- (fun _ ↦ Finset.univ)
simp at X
sorry