CompactSmoothExtension.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A compactly supported smooth extension agreeing near a prescribed compact subset of an open set. Its pointwise bound preserves bounded harmonic tests during Brownian localization.

lemma OAI.SLEExactGauge.exists_compact_smooth_extension line 14