OAI/Analysis/AffineBernstein/SphereIsometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.linearIsometrySphereHomeomorph line 15
2. lemma OAI.AffineBernstein.linearIsometrySphereHomeomorph_coe line 19
3. lemma OAI.AffineBernstein.linearIsometrySphere_cone_preimage line 23
4. theorem OAI.AffineBernstein.linearIsometrySphere_measurePreserving line 47

   Source comment

   The Haar-induced sphere measure is preserved by every linear isometry. No surface-measure normalization or Jacobian identity is assumed.

   theorem linearIsometrySphere_measurePreserving (f : E ≃ₗᵢ[ℝ] F) :
       MeasurePreserving (linearIsometrySphereHomeomorph f)
         (volume : Measure E).toSphere (volume : Measure F).toSphere := by
   …

   Mentions: OAI.AffineBernstein.linearIsometrySphereHomeomorph