OAI/Analysis/RieszRectifiability/Projections/ProjectionDiskCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Euclidean coordinates for projection disks

An orthonormal basis identifies a finite-dimensional subspace with Euclidean space. Composing this isometry with orthogonal projection preserves projection norms and transfers coverage of closed disks into these coordinates.

  1. theorem OAI.RieszRectifiability.exists_projection_disk_coordinates line 20