ExpandingPointedCompactness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One subsequence for locally bounded functions on expanding pointed balls

Only eventual data on each fixed ball is needed. Missing initial terms are filled by zero in the compactness proof, leaving every original tail intact.

theorem OAI.RegularPointCoordinates.expanding_pointed_function_compactness line 18