Maps of the complex plane in real coordinates

A map f : ℂ → ℂ of the plane, read in the real coordinates ℝ × ℝ ≃ ℂ given by Complex.equivRealProdCLM, is TauCeti.Complex.realChart f. When f has complex derivative f', the real derivative of its real chart is multiplication by f' (TauCeti.Complex.hasFDerivAt_realChart, TauCeti.Complex.fderiv_realChart_apply), whose real determinant is |f'|², so the Jacobian determinant of the real chart is nonnegative (TauCeti.Complex.det_fderiv_realChart, TauCeti.Complex.det_fderiv_realChart_nonneg), and a map that is C^n over ℂ is C^n over ℝ in real coordinates (TauCeti.Complex.contDiff_realChart). The real chart of an injective map is injective (TauCeti.Complex.realChart_injective).

noncomputable def TauCeti.Complex.realChart (f : ℂ → ℂ) : ℝ × ℝ → ℝ × ℝ

A map f : ℂ → ℂ of the plane, written in the real coordinates ℝ × ℝ ≃ ℂ.

theorem TauCeti.Complex.realChart_apply (f : ℂ → ℂ) (z : ℝ × ℝ) : realChart f z = Complex.equivRealProdCLM (f (Complex.equivRealProdCLM.symm z))

@[simp]

theorem TauCeti.Complex.equivRealProdCLM_symm_realChart (f : ℂ → ℂ) (z : ℝ × ℝ) : Complex.equivRealProdCLM.symm (realChart f z) = f (Complex.equivRealProdCLM.symm z)

In complex coordinates, the real chart of f is f.

theorem TauCeti.Complex.realChart_equivRealProdCLM (f : ℂ → ℂ) (w : ℂ) : realChart f (Complex.equivRealProdCLM w) = Complex.equivRealProdCLM (f w)

The real chart of f at the real coordinates of w is the real coordinates of f w.

theorem TauCeti.Complex.hasFDerivAt_realChart {f : ℂ → ℂ} {f' : ℂ} {w : ℝ × ℝ} (hf : HasDerivAt f f' (Complex.equivRealProdCLM.symm w)) : HasFDerivAt (realChart f) (↑Complex.equivRealProdCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ f') ∘SL ↑Complex.equivRealProdCLM.symm) w

In real coordinates, the derivative of a map with complex derivative f' is multiplication by f'.

theorem TauCeti.Complex.fderiv_realChart_apply {f : ℂ → ℂ} {f' : ℂ} {w : ℝ × ℝ} (hf : HasDerivAt f f' (Complex.equivRealProdCLM.symm w)) (v : ℝ × ℝ) : (fderiv ℝ (realChart f) w) v = Complex.equivRealProdCLM (f' * Complex.equivRealProdCLM.symm v)

theorem TauCeti.Complex.det_fderiv_realChart {f : ℂ → ℂ} {f' : ℂ} {w : ℝ × ℝ} (hf : HasDerivAt f f' (Complex.equivRealProdCLM.symm w)) : (fderiv ℝ (realChart f) w).det = Complex.normSq f'

In real coordinates, the Jacobian determinant of a map with complex derivative f' is |f'|².

theorem TauCeti.Complex.det_fderiv_realChart_nonneg {f : ℂ → ℂ} {f' : ℂ} {w : ℝ × ℝ} (hf : HasDerivAt f f' (Complex.equivRealProdCLM.symm w)) : 0 ≤ (fderiv ℝ (realChart f) w).det

In real coordinates, the Jacobian determinant of a map with a complex derivative is nonnegative.

theorem TauCeti.Complex.contDiff_realChart {f : ℂ → ℂ} {n : WithTop ℕ∞} (hf : ContDiff ℂ n f) : ContDiff ℝ n (realChart f)

A map that is C^n over ℂ is C^n over ℝ in real coordinates.

theorem TauCeti.Complex.realChart_injective {f : ℂ → ℂ} (hf : Function.Injective f) : Function.Injective (realChart f)

The real chart of an injective map is injective.