OAI/Geometry/RCD/Harmonic/HarmonicOpenBallCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One harmonic value limit on the whole open Euclidean ball

The exhaustion is used only to construct the function. Convergence holds on every strictly smaller physical ball through the original maps. Identification of the Euclidean weak equation is a separate step.

  1. theorem OAI.RegularPointCoordinates.harmonic_open_ball_value_compactness line 19