OAI/Analysis/RieszRectifiability/Flatness/QuadraticHyperplaneTangent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Hyperplane tangents from a quadratic support constraint

Blowups turn the quadratic constraint into a halfspace condition, while vanishing positive normal moments force the limiting support into its boundary hyperplane. Intrinsic growth then rules out the resulting nonzero tangent measure.

  1. theorem OAI.RieszRectifiability.blowup_support_quadratic_constraint line 23
  2. theorem OAI.RieszRectifiability.quadratic_blowup_limit_support_in_normal_hyperplane line 35
  3. theorem OAI.RieszRectifiability.intrinsic_quadratic_annular_bound_impossible line 60