The measured reference anchor is positive

Proved

OpenGA.MeasuredReferenceBall.anchor_pos

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

bishop-gromovgeometric-analysispoincare-conjecture

For a measured reference ball with normalization $v>0$ , its anchor satisfies

a=\mu(B_g(p,r))/v>0.

Openness and positive radius give strictly positive measure. The finite-measure hypothesis permits passage from extended nonnegative values to a positive real number.

Preamble

import Definitions.Def_OpenGA_MeasuredReferenceBall
set_option autoImplicit false
open MeasureTheory Set Filter
open scoped Manifold ContDiff ENNReal BigOperators Topology

open OpenGA

Formal statement

theorem OpenGA.MeasuredReferenceBall.anchor_pos (B : MeasuredReferenceBall) : 0 < B.anchor := by sorry

Source

https://github.com/MathNetwork/OpenGA/blob/feat/prove2me-differential-geometry/OpenGALib/ComparisonGeometry/MeasuredSurgery.lean

View graph