From c1766f6a38d58e091e24657dfe72e8d4f23b7b35 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 24 Jun 2024 17:30:30 +0200 Subject: [PATCH] Update laplace2.lean --- Nevanlinna/laplace2.lean | 218 +++++++++++++++++++++++++++++++++------ 1 file changed, 186 insertions(+), 32 deletions(-) diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean index 6f4830d..b8d8388 100644 --- a/Nevanlinna/laplace2.lean +++ b/Nevanlinna/laplace2.lean @@ -25,57 +25,211 @@ lemma vectorPresentation simp -theorem LaplaceIndep +theorem BilinearCalc [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) (hv₁ : Orthonormal ℝ v₁) (v₂ : Basis ι ℝ E) (hv₂ : Orthonormal ℝ v₂) - (f : E → F) : - ∑ i, iteratedFDeriv ℝ 2 f z ![v₁ i, v₁ i] = ∑ i, iteratedFDeriv ℝ 2 f z ![v₂ i, v₂ i] := by + (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) : + ∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by - have (v : E) : v = ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j) := - sorry + have vector_vs_function + {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 => right arg 2 intro i - rw [this (v₂ i)] - rw [this (v₂ i)] + rw [vectorPresentation v₁ hv₁ (v₂ i)] + rw [BilinearCalc] + rw [Finset.sum_comm] conv => right arg 2 - intro i - --rw [ContinuousMultilinearMap.map_sum_finset] + intro y + rw [← Finset.sum_smul] + rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))] + rw [vector_vs_function] + simp - 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 - -noncomputable def Laplace₁ (n : ℕ) (f : EuclideanSpace ℝ (Fin n) → F) : EuclideanSpace ℝ (Fin n) → F := by - let e : Fin n → EuclideanSpace ℝ (Fin n) := fun i ↦ EuclideanSpace.single i (1 : ℝ) - exact fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![e i, e i] + 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 + intro r₀ + rw [Fintype.sum_eq_single r₀ xx] + rw [orthonormal_iff_ite.1 hv₁] + apply sum_congr + rfl + intro x _ + rw [vector_vs_function] + simp -noncomputable def Laplace₂ +noncomputable def Laplace_wrt_basis [Fintype ι] (v : Basis ι ℝ E) - (hv : Orthonormal ℝ v) + (_ : Orthonormal ℝ v) (f : E → F) : E → F := 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 +