OAI/Analysis/RieszRectifiability/Flatness/PlaneTestExtensions.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact ambient extensions of plane tests

An adjoint coordinate projection extends a test function from an affine plane. A radial cutoff makes the extension compactly supported while retaining its values on the plane and explicit uniform and Lipschitz bounds.

  1. theorem OAI.RieszRectifiability.exists_compact_ambient_plane_test line 23
  2. theorem OAI.RieszRectifiability.exists_compact_ambient_directional_test line 82