OAI/Analysis/RieszRectifiability/Foundations/SubspaceTangentSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Subspace support of tangent measures

Compact-test convergence preserves containment of supports in a fixed closed set. Blowups centered in a linear subspace stay in that subspace, so their limits inherit the same support constraint. Intersecting with the normal hyperplane of a nonzero subspace vector strictly reduces the dimension, as needed for dimension reduction.

  1. theorem OAI.RieszRectifiability.compactTestConvergence_support_subset_closed line 22
  2. theorem OAI.RieszRectifiability.blowupMeasure_support_submodule line 31
  3. theorem OAI.RieszRectifiability.blowup_limit_support_submodule line 40
  4. theorem OAI.RieszRectifiability.normal_section_finrank_lt line 52