Documentation

TauCeti.Analysis.Complex.Euclidean.Four

The real coordinates of ℂ² #

The L² product WithLp 2 (ℂ × ℂ) is linearly isometric to Euclidean four-space through the real coordinates (z, w) ↦ (Re z, Im z, Re w, Im w).

Main definitions #

source
noncomputable def TauCeti.complexProdToEuclideanFour :
WithLp 2 (ℂ × ℂ) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4)

The linear isometry ℂ² ≃ ℝ⁴, (z, w) ↦ (Re z, Im z, Re w, Im w), from the L² product WithLp 2 (ℂ × ℂ) to Euclidean four-space. It applies Complex.orthonormalBasisOneI.repr to each factor and then concatenates the two coordinate vectors along finSumFinEquiv.

Instances For
    source
    @[simp]
    theorem TauCeti.complexProdToEuclideanFour_apply (x : WithLp 2 (ℂ × ℂ)) :
    complexProdToEuclideanFour x = !₂[x.fst.re, x.fst.im, x.snd.re, x.snd.im]
    source
    @[simp]
    theorem TauCeti.complexProdToEuclideanFour_symm_apply (y : EuclideanSpace ℝ (Fin 4)) :
    complexProdToEuclideanFour.symm y = WithLp.toLp 2 ({ re := y.ofLp 0, im := y.ofLp 1 }, { re := y.ofLp 2, im := y.ofLp 3 })