Positive measure of a geodesic ball

Proved

Riemannian.RiemannianMetric.measure_geodesicBall_pos

by Xinze-Li-Moqian · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

bishop-gromovcomparison-geometrymeasure-theory

Let g be a smooth Riemannian metric on a finite-dimensional manifold M and let mu be a measure that assigns positive measure to every nonempty open set. If a geodesic ball B_g(p,r) has positive radius and is open, then its mu-measure is positive. This is the measure-theoretic positivity interface for normalized ball-volume ratios in Bishop-Gromov comparison.

Preamble

import Definitions.Def_OpenGA_GeodesicBall
import Mathlib.MeasureTheory.Measure.Restrict
noncomputable section
set_option autoImplicit false
open Bundle Set DifferentialGeometry MeasureTheory
open scoped Manifold ContDiff ENNReal
open Riemannian Riemannian.RiemannianMetric
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type*} [TopologicalSpace M] [MeasurableSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
  {μ : Measure M}

Formal statement

theorem Riemannian.RiemannianMetric.measure_geodesicBall_pos
    [FiniteDimensional ℝ E] [T2Space M] [SigmaCompactSpace M]
    (g : RiemannianMetric I M) (p : M) {r : ℝ}
    (hμ : ∀ s : Set M, IsOpen s → s.Nonempty → 0 < μ s)
    (hopen : IsOpen (g.geodesicBall p r)) (hr : 0 < r) :
    0 < μ (g.geodesicBall p r) := by sorry

Source

OpenGA, OpenGALib/ComparisonGeometry/Volume.lean; openness input: https://prove2.me/theorems/c13cb69f-c40b-40b3-8960-3a59f11c9123

View graph