Real dual directions in the complex plane

Every real continuous linear functional on ℂ is a dot product with a unique planar coefficient vector. A nonzero functional is therefore a positive multiple of the unit directional functional indexed by the argument of that coefficient vector. This elementary identification lets abstract separating hyperplanes be converted to the angle-indexed support halfspaces used by the smooth support-curve construction.

theorem realContinuousLinearMap_apply_eq_re_im (f : ℂ →L[ℝ] ℝ) (z : ℂ) : f z = z.re * f 1 + z.im * f Complex.I

A real continuous linear functional on ℂ is determined by its values on the real basis vectors 1 and I.

noncomputable def realContinuousLinearMapCoefficient (f : ℂ →L[ℝ] ℝ) : ℂ

The coefficient vector associated with a planar real continuous linear functional.

Equations

• realContinuousLinearMapCoefficient f = { re := f 1, im := f Complex.I }

@[simp]

theorem realContinuousLinearMapCoefficient_re (f : ℂ →L[ℝ] ℝ) : (realContinuousLinearMapCoefficient f).re = f 1

@[simp]

theorem realContinuousLinearMapCoefficient_im (f : ℂ →L[ℝ] ℝ) : (realContinuousLinearMapCoefficient f).im = f Complex.I

theorem realContinuousLinearMapCoefficient_ne_zero {f : ℂ →L[ℝ] ℝ} (hf : f ≠ 0) : realContinuousLinearMapCoefficient f ≠ 0

A nonzero planar functional has a nonzero coefficient vector.

theorem exists_pos_mul_polytopeDirectionalValue_eq_realContinuousLinearMap {f : ℂ →L[ℝ] ℝ} (hf : f ≠ 0) : ∃ (c : ℝ) (theta : ℝ), 0 < c ∧ ∀ (z : ℂ), c * polytopeDirectionalValue z theta = f z

Every nonzero real continuous linear functional on the complex plane is a positive multiple of one of the unit angle-indexed directional functionals.