OAI/Geometry/RCD/Metric/PositiveCompactCoreApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive bounded approximation by the actual compact Laplacian core

Heat regularization followed by the fixed interior cutoff preserves both positivity and the original amplitude bound. The convergence is in H1.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.positive_compact_core_approximation line 18