Update laplace2.lean

This commit is contained in:
Stefan Kebekus 2024-06-27 06:35:02 +02:00
parent 07f4ff610b
commit c59e12a468
1 changed files with 37 additions and 16 deletions

View File

@ -12,13 +12,35 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDim
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
lemma vectorPresentation'
[Fintype ι]
(b : OrthonormalBasis ι E)
--(hb : Orthonormal b)
(v : E) :
v = ∑ i, ⟪b i, v⟫_ • (b i) := by
let A := b.sum_repr v
let i : ι := by sorry
let B := b.repr v i
nth_rw 1 [← (b.sum_repr v)]
apply Fintype.sum_congr
intro i
--let A := b.repr v
--have : (b.repr v) = ((OrthonormalBasis.toBasis b).repr v) := by tauto
rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
simp
lemma vectorPresentation
[Fintype ι]
(b : Basis ι E)
(hb : Orthonormal b)
(v : E) :
v = ∑ i, ⟪b i, v⟫_ • (b i) := by
nth_rw 1 [← (b.sum_repr v)]
nth_rw 1 [← (b.sum_repr v)]
apply Fintype.sum_congr
intro i
rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
@ -31,7 +53,7 @@ theorem BilinearCalc
(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
@ -67,7 +89,7 @@ lemma fin_sum
rw [← Fintype.sum_prod_type']
apply Fintype.sum_equiv (finTwoArrowEquiv ι)
intro x
dsimp
dsimp
theorem LaplaceIndep
@ -80,9 +102,9 @@ theorem LaplaceIndep
∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by
have vector_vs_function
{y : Fin 2 → ι}
{y : Fin 2 → ι}
{v : ι → E}
: (fun i => v (y i)) = ![v (y 0), v (y 1)] := by
: (fun i => v (y i)) = ![v (y 0), v (y 1)] := by
funext i
by_cases h : i = 0
· rw [h]
@ -107,13 +129,13 @@ theorem LaplaceIndep
simp
rw [fin_sum (fun i₀ ↦ (fun i₁ ↦ ⟪v₁ i₀, v₁ i₁⟫_ • L ![v₁ i₀, v₁ i₁]))]
have xx {r₀ : ι} : ∀ r₁ : ι, r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ • L ![v₁ r₀, v₁ r₁] = 0 := by
intro r₁ hr₁
rw [orthonormal_iff_ite.1 hv₁]
simp
tauto
conv =>
right
arg 2
@ -142,7 +164,7 @@ theorem LaplaceIndep'
(hv₁ : Orthonormal v₁)
(v₂ : Basis ι E)
(hv₂ : Orthonormal v₂)
(f : E → F)
(f : E → F)
: (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
funext z
@ -150,7 +172,7 @@ theorem LaplaceIndep'
let XX := LaplaceIndep v₁ hv₁ v₂ hv₂ (iteratedFDeriv 2 f z)
have vector_vs_function
{v : E}
: ![v, v] = (fun _ => v) := by
: ![v, v] = (fun _ => v) := by
funext i
by_cases h : i = 0
· rw [h]
@ -177,7 +199,7 @@ theorem LaplaceIndep''
[Fintype ι₂] [DecidableEq ι₂]
(v₂ : Basis ι₂ E)
(hv₂ : Orthonormal v₂)
(f : E → F)
(f : E → F)
: (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
have b : ι₁ ≃ ι₂ := by
@ -186,9 +208,9 @@ theorem LaplaceIndep''
rw [← FiniteDimensional.finrank_eq_card_basis v₂]
let v'₁ := Basis.reindex v₁ b
have hv'₁ : Orthonormal v'₁ := by
have hv'₁ : Orthonormal v'₁ := by
let A := Basis.reindex_apply v₁ b
have : ⇑v'₁ = v₁ ∘ b.symm := by
have : ⇑v'₁ = v₁ ∘ b.symm := by
funext i
exact A i
rw [this]
@ -209,7 +231,7 @@ theorem LaplaceIndep''
noncomputable def Laplace
(f : E → F)
(f : E → F)
: E → F := by
exact Laplace_wrt_basis (stdOrthonormalBasis E).toBasis (stdOrthonormalBasis E).orthonormal f
@ -218,11 +240,11 @@ theorem LaplaceIndep'''
[Fintype ι] [DecidableEq ι]
(v : Basis ι E)
(hv : Orthonormal v)
(f : E → F)
(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
apply LaplaceIndep'' (stdOrthonormalBasis E).toBasis (stdOrthonormalBasis E).orthonormal v hv f
theorem Complex.Laplace'
@ -232,4 +254,3 @@ theorem Complex.Laplace'
rw [LaplaceIndep''' Complex.orthonormalBasisOneI.toBasis Complex.orthonormalBasisOneI.orthonormal f]
unfold Laplace_wrt_basis
simp