Compare commits
No commits in common. "ecdc182f2b76661be8b3aad96bf9f8769b0a712b" and "d287c24453fa6808dc88ac03037f17bbe1448587" have entirely different histories.
ecdc182f2b
...
d287c24453
|
@ -27,8 +27,6 @@ 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)
|
||||
|
@ -51,22 +49,5 @@ theorem LaplaceIndep
|
|||
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
|
||||
|
||||
rw [ContinuousMultilinearMap.map_sum_finset]
|
||||
sorry
|
||||
|
|
Loading…
Reference in New Issue