OAI/Geometry/RCD/Sobolev/CompactTestHarmonicReplacements.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual harmonic candidates built from prescribed Euclidean tests

The recovered boundary values and harmonic replacements live in the original Sobolev spaces. Both global L2 and rescaled energy bounds retain the physical outer-ball normalization.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_test_harmonic_replacements line 21