OAI/Analysis/Mahler/CoordinateSphere.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MahlerStokes.finite_radiusSq_slice line 9
2. theorem OAI.MahlerStokes.volume_coordSphere line 21

   Source documentation

   Coordinate Euclidean spheres have zero Lebesgue measure.

   theorem volume_coordSphere {n : ℕ} (R : ℝ) :
       volume {x : Fin (n+1) → ℝ | radiusSq x = R^2} = 0 := by
   …

   Mentions: OAI.MahlerStokes.radiusSq

3. theorem OAI.MahlerStokes.coordAnnulus_ae_eq_puncture line 42

   Source documentation

   Removing the closed inner ball changes no volume integral.

   theorem coordAnnulus_ae_eq_puncture {n : ℕ} (a R : ℝ) :
       coordAnnulus (n+1) a R =ᵐ[volume]
         coordBall (n+1) R \ coordClosedBall (n+1) a := by
   …

   Mentions: OAI.MahlerStokes.coordAnnulus, OAI.MahlerStokes.coordBall, OAI.MahlerStokes.coordClosedBall