OAI/Analysis/RieszRectifiability/Kernel/PolynomialDegreeDrop.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the top homogeneous component

The homogeneous decomposition expresses the remainder after subtracting a polynomial's top component as a sum of strictly lower components. If the original total degree is positive, the finite-sum degree bound makes this a strict degree reduction.

  1. theorem OAI.RieszRectifiability.polynomial_sub_top_eq_lower_sum line 17
  2. theorem OAI.RieszRectifiability.polynomial_sub_top_degree_lt line 24