OAI/Analysis/RieszRectifiability/Limits/PolynomialLeadingLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Leading homogeneous terms under dilation

Along an expanding sequence of positive radii, normalization by the total degree makes lower-degree powers vanish and preserves the top-degree power. Applying this limit to the finite homogeneous decomposition of a polynomial recovers its leading homogeneous component pointwise.

  1. def OAI.RieszRectifiability.polynomialExpansionRadius line 22
  2. theorem OAI.RieszRectifiability.polynomialExpansionRadius_pos line 24
  3. theorem OAI.RieszRectifiability.inverse_pow_mul_pow_of_le line 28
  4. theorem OAI.RieszRectifiability.inverse_polynomialExpansionRadius_tendsto line 35
  5. theorem OAI.RieszRectifiability.polynomial_scale_coefficient_tendsto line 41
  6. theorem OAI.RieszRectifiability.polynomial_normalized_dilation_tendsto line 54