OAI/Analysis/RieszRectifiability/Flatness/DegreeOnePolynomialAffine.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Affine representations of degree-one polynomials

Evaluation of a homogeneous degree-one complex polynomial on real Euclidean space is a continuous real-linear map. Splitting off the constant homogeneous component gives an affine representation for polynomials of degree at most one.

  1. theorem OAI.RieszRectifiability.homogeneous_degree_one_eval_linear line 18
  2. theorem OAI.RieszRectifiability.degree_one_polynomial_eval_affine line 46