SphericalMeasureCharts.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Compact smooth coordinate-face charts and a Lipschitz projection for the actual unit three-sphere. These are used only to establish finite positive Hausdorff mass; no spherical integration formula is assumed.

abbrev OAI.PositiveEinsteinFour.Angular.ThreeSpace line 18
def OAI.PositiveEinsteinFour.Angular.faceSign line 20
theorem OAI.PositiveEinsteinFour.Angular.faceSign_ne_zero line 22
def OAI.PositiveEinsteinFour.Angular.faceVector line 25
theorem OAI.PositiveEinsteinFour.Angular.faceVector_ne_zero line 28
theorem OAI.PositiveEinsteinFour.Angular.faceVector_contDiff line 34
def OAI.PositiveEinsteinFour.Angular.faceChart line 45
theorem OAI.PositiveEinsteinFour.Angular.faceChart_contDiff line 48
theorem OAI.PositiveEinsteinFour.Angular.faceChart_lipschitz line 53
theorem OAI.PositiveEinsteinFour.Angular.exists_faceChart line 60
Source documentation
The eight normalized cube faces cover the sphere using a fixed compact three-dimensional parameter ball.
```
theorem exists_faceChart (q : Directions) :
    ∃ i : Fin 4, ∃ t : Bool, ∃ u ∈ Metric.closedBall (0 : ThreeSpace) 2,
      faceChart i t u = q.val := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.Directions, OAI.PositiveEinsteinFour.Angular.ThreeSpace, OAI.PositiveEinsteinFour.Angular.faceChart
def OAI.PositiveEinsteinFour.Angular.tailProjection line 116
Source documentation
Dropping one coordinate does not increase Euclidean distance.
```
def tailProjection (v : FourSpace) : ThreeSpace :=
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.ThreeSpace
theorem OAI.PositiveEinsteinFour.Angular.tailProjection_norm_le line 119
theorem OAI.PositiveEinsteinFour.Angular.tailProjection_lipschitz line 126
theorem OAI.PositiveEinsteinFour.Angular.ball_subset_tailProjection_sphere line 135
Source documentation
The projection of the actual sphere contains a nonempty open ball.
```
theorem ball_subset_tailProjection_sphere :
    Metric.ball (0 : ThreeSpace) 1 ⊆
      tailProjection '' {v : FourSpace | ‖v‖ = 1} := by
…
```
Mentions: OAI.PositiveEinsteinFour.Angular.ThreeSpace, OAI.PositiveEinsteinFour.Angular.tailProjection