Documentation

TauCeti.Analysis.Complex.Euclidean.Space

Real coordinates of complex vectors #

complexToRealEuclidean identifies a finite complex vector with its real and imaginary coordinate blocks as a real continuous linear equivalence. It uses the product topology on complex vectors and the Euclidean topology on the real coordinates, so both directions are measurable for the Borel structures. complexToRealPi is the same splitting with plain functions ι ⊕ ι → ℝ as target, the coordinate spaces in which semialgebraic subsets of complex coordinate spaces are formed.

source
noncomputable def TauCeti.complexToRealEuclidean (ι : Type u_1) [Fintype ι] :
(ι → ℂ) ≃L[ℝ] EuclideanSpace ℝ (ι ⊕ ι)

Split a complex vector into its real and imaginary coordinate blocks, as a real continuous linear equivalence.

Instances For
    source
    @[simp]
    theorem TauCeti.complexToRealEuclidean_apply (ι : Type u_1) [Fintype ι] (z : ι → ℂ) (k : ι ⊕ ι) :
    ((complexToRealEuclidean ι) z).ofLp k = Sum.elim (fun (i : ι) => (z i).re) (fun (i : ι) => (z i).im) k
    source
    @[simp]
    theorem TauCeti.inner_complexToRealEuclidean (ι : Type u_1) [Fintype ι] (z w : ι → ℂ) :
    inner ℝ ((complexToRealEuclidean ι) z) ((complexToRealEuclidean ι) w) = (star z ⬝ᵥ w).re

    The real Euclidean pairing of split coordinates is the real part of the complex Hermitian pairing.

    source
    theorem TauCeti.complexToRealEuclidean_symm_apply (ι : Type u_1) [Fintype ι] (x : EuclideanSpace ℝ (ι ⊕ ι)) (i : ι) :
    (complexToRealEuclidean ι).symm x i = ↑(x.ofLp (Sum.inl i)) + ↑(x.ofLp (Sum.inr i)) * Complex.I

    Recombine the two real coordinate blocks into a complex vector.

    source
    @[simp]
    theorem TauCeti.complexToRealEuclidean_symm_apply_re (ι : Type u_1) [Fintype ι] (x : EuclideanSpace ℝ (ι ⊕ ι)) (i : ι) :
    ((complexToRealEuclidean ι).symm x i).re = x.ofLp (Sum.inl i)
    source
    @[simp]
    theorem TauCeti.complexToRealEuclidean_symm_apply_im (ι : Type u_1) [Fintype ι] (x : EuclideanSpace ℝ (ι ⊕ ι)) (i : ι) :
    ((complexToRealEuclidean ι).symm x i).im = x.ofLp (Sum.inr i)
    source
    noncomputable def TauCeti.complexToRealPi (ι : Type u_1) [Fintype ι] :
    (ι → ℂ) ≃L[ℝ] ι ⊕ ι → ℝ

    Split a complex vector into its real and imaginary coordinate blocks, with plain functions ι ⊕ ι → ℝ as target: Sum.inl i is the real part and Sum.inr i the imaginary part of the i-th coordinate. This is TauCeti.complexToRealEuclidean followed by forgetting the Euclidean structure.

    Instances For
      source
      @[simp]
      theorem TauCeti.complexToRealPi_apply (ι : Type u_1) [Fintype ι] (z : ι → ℂ) (k : ι ⊕ ι) :
      (complexToRealPi ι) z k = Sum.elim (fun (i : ι) => (z i).re) (fun (i : ι) => (z i).im) k
      source
      theorem TauCeti.ofLp_complexToRealEuclidean (ι : Type u_1) [Fintype ι] (z : ι → ℂ) :
      ((complexToRealEuclidean ι) z).ofLp = (complexToRealPi ι) z

      Forgetting the Euclidean structure of TauCeti.complexToRealEuclidean gives TauCeti.complexToRealPi.

      source
      @[simp]
      theorem TauCeti.complexToRealPi_symm_apply (ι : Type u_1) [Fintype ι] (a : ι ⊕ ι → ℝ) (i : ι) :
      (complexToRealPi ι).symm a i = ↑(a (Sum.inl i)) + ↑(a (Sum.inr i)) * Complex.I

      Recombine two real coordinate blocks into a complex vector.