Compare commits
2 Commits
d287c24453
...
ecdc182f2b
Author | SHA1 | Date |
---|---|---|
Stefan Kebekus | ecdc182f2b | |
Stefan Kebekus | adc0378e5d |
|
@ -27,6 +27,8 @@ noncomputable def Laplace₂
|
||||||
E → F :=
|
E → F :=
|
||||||
fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
|
fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
|
||||||
|
|
||||||
|
#check ContinuousMultilinearMap.map_sum_finset
|
||||||
|
|
||||||
theorem LaplaceIndep
|
theorem LaplaceIndep
|
||||||
[Fintype ι]
|
[Fintype ι]
|
||||||
(v₁ : Basis ι ℝ E)
|
(v₁ : Basis ι ℝ E)
|
||||||
|
@ -49,5 +51,22 @@ theorem LaplaceIndep
|
||||||
right
|
right
|
||||||
arg 2
|
arg 2
|
||||||
intro i
|
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
|
sorry
|
||||||
|
|
Loading…
Reference in New Issue