nevanlinna/Nevanlinna/laplace2.lean

258 lines
6.5 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.PiL2
--import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Analysis.Calculus.ContDiff.Bounds
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.LinearAlgebra.Basis
import Mathlib.LinearAlgebra.Contraction
open BigOperators
open Finset
lemma OrthonormalBasis.sum_repr'
{𝕜 : Type*} [RCLike 𝕜]
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
[Fintype ι]
(b : OrthonormalBasis ι 𝕜 E)
(v : E) :
v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
nth_rw 1 [← (b.sum_repr v)]
simp_rw [b.repr_apply_apply v]
noncomputable def realInnerAsElementOfDualTensorprod
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace E]
: TensorProduct E E →ₗ[] := TensorProduct.lift bilinFormOfRealInner
noncomputable def dual'
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [CompleteSpace E] [FiniteDimensional E]
: (TensorProduct E E →ₗ[] ) ≃ₗ[] TensorProduct E E := by
let d := InnerProductSpace.toDual E
let e := d.toLinearEquiv
let a := TensorProduct.congr e e
let b := homTensorHomEquiv E E
sorry
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
theorem InvariantTensor
[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]
simp_rw [L.map_smul_univ]
sorry
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]
simp_rw [L.map_smul_univ]
sorry
/-
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₁ : OrthonormalBasis ι E)
(v₂ : OrthonormalBasis ι E)
(L : ContinuousMultilinearMap (fun (_ : Fin 2) ↦ E) F) :
∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by
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 [v₁.sum_repr' (v₂ i)]
rw [BilinearCalc]
rw [Finset.sum_comm]
conv =>
right
arg 2
intro y
rw [← Finset.sum_smul]
rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))]
rw [vector_vs_function]
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
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_wrt_basis
[Fintype ι]
(v : Basis ι E)
(_ : Orthonormal v)
(f : E → F) :
E → F :=
fun z ↦ ∑ i, iteratedFDeriv 2 f z ![v i, v i]
theorem LaplaceIndep'
[Fintype ι] [DecidableEq ι]
(v₁ : OrthonormalBasis ι E)
(v₂ : OrthonormalBasis ι E)
(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