Update laplace2.lean
This commit is contained in:
Stefan Kebekus
parent
42cf2e41b9
commit
c1766f6a38
|
|
@ -25,57 +25,211 @@ lemma vectorPresentation
|
||||||
simp
|
simp
|
||||||
|
|
||||||
|
|
||||||
theorem LaplaceIndep
|
theorem BilinearCalc
|
||||||
[Fintype ι]
|
[Fintype ι]
|
||||||
|
(v : Basis ι ℝ E)
|
||||||
|
(c : ι → ℝ)
|
||||||
|
(L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) :
|
||||||
|
L (fun _ => ∑ j : ι, c j • v j) = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L ((fun i => v (x i))) := by
|
||||||
|
|
||||||
|
rw [L.map_sum]
|
||||||
|
conv =>
|
||||||
|
left
|
||||||
|
arg 2
|
||||||
|
intro r
|
||||||
|
rw [L.map_smul_univ]
|
||||||
|
simp
|
||||||
|
|
||||||
|
|
||||||
|
lemma c2
|
||||||
|
[Fintype ι]
|
||||||
|
(b : Basis ι ℝ E)
|
||||||
|
(hb : Orthonormal ℝ b)
|
||||||
|
(x y : E) :
|
||||||
|
⟪x, y⟫_ℝ = ∑ i : ι, ⟪x, b i⟫_ℝ * ⟪y, b i⟫_ℝ := by
|
||||||
|
rw [vectorPresentation b hb x]
|
||||||
|
rw [vectorPresentation b hb y]
|
||||||
|
rw [Orthonormal.inner_sum hb]
|
||||||
|
simp
|
||||||
|
conv =>
|
||||||
|
right
|
||||||
|
arg 2
|
||||||
|
intro i'
|
||||||
|
rw [Orthonormal.inner_left_fintype hb]
|
||||||
|
rw [Orthonormal.inner_left_fintype hb]
|
||||||
|
|
||||||
|
|
||||||
|
lemma fin_sum
|
||||||
|
[Fintype ι]
|
||||||
|
(f : ι → ι → F) :
|
||||||
|
∑ r : Fin 2 → ι, f (r 0) (r 1) = ∑ r₀ : ι, (∑ r₁ : ι, f r₀ r₁) := by
|
||||||
|
|
||||||
|
rw [← Fintype.sum_prod_type']
|
||||||
|
apply Fintype.sum_equiv (finTwoArrowEquiv ι)
|
||||||
|
intro x
|
||||||
|
dsimp
|
||||||
|
|
||||||
|
|
||||||
|
theorem LaplaceIndep
|
||||||
|
[Fintype ι] [DecidableEq ι]
|
||||||
(v₁ : Basis ι ℝ E)
|
(v₁ : Basis ι ℝ E)
|
||||||
(hv₁ : Orthonormal ℝ v₁)
|
(hv₁ : Orthonormal ℝ v₁)
|
||||||
(v₂ : Basis ι ℝ E)
|
(v₂ : Basis ι ℝ E)
|
||||||
(hv₂ : Orthonormal ℝ v₂)
|
(hv₂ : Orthonormal ℝ v₂)
|
||||||
(f : E → F) :
|
(L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) :
|
||||||
∑ i, iteratedFDeriv ℝ 2 f z ![v₁ i, v₁ i] = ∑ i, iteratedFDeriv ℝ 2 f z ![v₂ i, v₂ i] := by
|
∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by
|
||||||
|
|
||||||
have (v : E) : v = ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j) :=
|
have vector_vs_function
|
||||||
sorry
|
{y : Fin 2 → ι}
|
||||||
|
{v : ι → E}
|
||||||
|
: (fun i => v (y i)) = ![v (y 0), v (y 1)] := by
|
||||||
|
funext i
|
||||||
|
by_cases h : i = 0
|
||||||
|
· rw [h]
|
||||||
|
simp
|
||||||
|
· rw [Fin.eq_one_of_neq_zero i h]
|
||||||
|
simp
|
||||||
|
|
||||||
conv =>
|
conv =>
|
||||||
right
|
right
|
||||||
arg 2
|
arg 2
|
||||||
intro i
|
intro i
|
||||||
rw [this (v₂ i)]
|
rw [vectorPresentation v₁ hv₁ (v₂ i)]
|
||||||
rw [this (v₂ i)]
|
rw [BilinearCalc]
|
||||||
|
rw [Finset.sum_comm]
|
||||||
conv =>
|
conv =>
|
||||||
right
|
right
|
||||||
arg 2
|
arg 2
|
||||||
intro i
|
intro y
|
||||||
--rw [ContinuousMultilinearMap.map_sum_finset]
|
rw [← Finset.sum_smul]
|
||||||
|
rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))]
|
||||||
|
rw [vector_vs_function]
|
||||||
|
simp
|
||||||
|
|
||||||
have v : E := by sorry
|
rw [fin_sum (fun i₀ ↦ (fun i₁ ↦ ⟪v₁ i₀, v₁ i₁⟫_ℝ • L ![v₁ i₀, v₁ i₁]))]
|
||||||
--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
|
have xx {r₀ : ι} : ∀ r₁ : ι, r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ℝ • L ![v₁ r₀, v₁ r₁] = 0 := by
|
||||||
(iteratedFDeriv ℝ 2 f z)
|
intro r₁ hr₁
|
||||||
(fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
|
rw [orthonormal_iff_ite.1 hv₁]
|
||||||
|
simp
|
||||||
|
tauto
|
||||||
|
|
||||||
--
|
conv =>
|
||||||
-- (fun _ ↦ Finset.univ)
|
right
|
||||||
simp at X
|
arg 2
|
||||||
|
intro r₀
|
||||||
sorry
|
rw [Fintype.sum_eq_single r₀ xx]
|
||||||
|
rw [orthonormal_iff_ite.1 hv₁]
|
||||||
noncomputable def Laplace₁ (n : ℕ) (f : EuclideanSpace ℝ (Fin n) → F) : EuclideanSpace ℝ (Fin n) → F := by
|
apply sum_congr
|
||||||
let e : Fin n → EuclideanSpace ℝ (Fin n) := fun i ↦ EuclideanSpace.single i (1 : ℝ)
|
rfl
|
||||||
exact fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![e i, e i]
|
intro x _
|
||||||
|
rw [vector_vs_function]
|
||||||
|
simp
|
||||||
|
|
||||||
|
|
||||||
noncomputable def Laplace₂
|
noncomputable def Laplace_wrt_basis
|
||||||
[Fintype ι]
|
[Fintype ι]
|
||||||
(v : Basis ι ℝ E)
|
(v : Basis ι ℝ E)
|
||||||
(hv : Orthonormal ℝ v)
|
(_ : Orthonormal ℝ v)
|
||||||
(f : E → F) :
|
(f : E → F) :
|
||||||
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]
|
||||||
|
|
||||||
|
|
||||||
|
theorem LaplaceIndep'
|
||||||
|
[Fintype ι] [DecidableEq ι]
|
||||||
|
(v₁ : Basis ι ℝ E)
|
||||||
|
(hv₁ : Orthonormal ℝ v₁)
|
||||||
|
(v₂ : Basis ι ℝ E)
|
||||||
|
(hv₂ : Orthonormal ℝ v₂)
|
||||||
|
(f : E → F)
|
||||||
|
: (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
|
||||||
|
|
||||||
|
funext z
|
||||||
|
unfold Laplace_wrt_basis
|
||||||
|
let XX := LaplaceIndep v₁ hv₁ v₂ hv₂ (iteratedFDeriv ℝ 2 f z)
|
||||||
|
have vector_vs_function
|
||||||
|
{v : E}
|
||||||
|
: ![v, v] = (fun _ => v) := by
|
||||||
|
funext i
|
||||||
|
by_cases h : i = 0
|
||||||
|
· rw [h]
|
||||||
|
simp
|
||||||
|
· rw [Fin.eq_one_of_neq_zero i h]
|
||||||
|
simp
|
||||||
|
conv =>
|
||||||
|
left
|
||||||
|
arg 2
|
||||||
|
intro i
|
||||||
|
rw [vector_vs_function]
|
||||||
|
conv =>
|
||||||
|
right
|
||||||
|
arg 2
|
||||||
|
intro i
|
||||||
|
rw [vector_vs_function]
|
||||||
|
assumption
|
||||||
|
|
||||||
|
|
||||||
|
theorem LaplaceIndep''
|
||||||
|
[Fintype ι₁] [DecidableEq ι₁]
|
||||||
|
(v₁ : Basis ι₁ ℝ E)
|
||||||
|
(hv₁ : Orthonormal ℝ v₁)
|
||||||
|
[Fintype ι₂] [DecidableEq ι₂]
|
||||||
|
(v₂ : Basis ι₂ ℝ E)
|
||||||
|
(hv₂ : Orthonormal ℝ v₂)
|
||||||
|
(f : E → F)
|
||||||
|
: (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
|
||||||
|
|
||||||
|
have b : ι₁ ≃ ι₂ := by
|
||||||
|
apply Fintype.equivOfCardEq
|
||||||
|
rw [← FiniteDimensional.finrank_eq_card_basis v₁]
|
||||||
|
rw [← FiniteDimensional.finrank_eq_card_basis v₂]
|
||||||
|
|
||||||
|
let v'₁ := Basis.reindex v₁ b
|
||||||
|
have hv'₁ : Orthonormal ℝ v'₁ := by
|
||||||
|
let A := Basis.reindex_apply v₁ b
|
||||||
|
have : ⇑v'₁ = v₁ ∘ b.symm := by
|
||||||
|
funext i
|
||||||
|
exact A i
|
||||||
|
rw [this]
|
||||||
|
let B := Orthonormal.comp hv₁ b.symm
|
||||||
|
apply B
|
||||||
|
exact Equiv.injective b.symm
|
||||||
|
rw [← LaplaceIndep' v'₁ hv'₁ v₂ hv₂ f]
|
||||||
|
|
||||||
|
unfold Laplace_wrt_basis
|
||||||
|
simp
|
||||||
|
funext z
|
||||||
|
|
||||||
|
rw [← Equiv.sum_comp b.symm]
|
||||||
|
apply Fintype.sum_congr
|
||||||
|
intro i₂
|
||||||
|
congr
|
||||||
|
rw [Basis.reindex_apply v₁ b i₂]
|
||||||
|
|
||||||
|
|
||||||
|
noncomputable def Laplace
|
||||||
|
(f : E → F)
|
||||||
|
: E → F := by
|
||||||
|
exact Laplace_wrt_basis (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal f
|
||||||
|
|
||||||
|
|
||||||
|
theorem LaplaceIndep'''
|
||||||
|
[Fintype ι] [DecidableEq ι]
|
||||||
|
(v : Basis ι ℝ E)
|
||||||
|
(hv : Orthonormal ℝ v)
|
||||||
|
(f : E → F)
|
||||||
|
: (Laplace f) = (Laplace_wrt_basis v hv f) := by
|
||||||
|
|
||||||
|
unfold Laplace
|
||||||
|
apply LaplaceIndep'' (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal v hv f
|
||||||
|
|
||||||
|
|
||||||
|
theorem Complex.Laplace'
|
||||||
|
(f : ℂ → F)
|
||||||
|
: (Laplace f) = fun z ↦ (iteratedFDeriv ℝ 2 f z) ![1, 1] + (iteratedFDeriv ℝ 2 f z) ![Complex.I, Complex.I] := by
|
||||||
|
|
||||||
|
rw [LaplaceIndep''' Complex.orthonormalBasisOneI.toBasis Complex.orthonormalBasisOneI.orthonormal f]
|
||||||
|
unfold Laplace_wrt_basis
|
||||||
|
simp
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue