LocalPoissonFullBochnerMeasure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Full continuous-test Bochner measures for local Poisson data

The three-halves interior ratio leaves room for the good cutoff inside an eightfold working ball. The identity holds on every continuous compactly supported Sobolev test and retains all of the positive measure.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.local_poisson_full_bochner_measure line 23