OAI/Geometry/RCD/Sobolev/UniformSlicesSpacetimeL2GoodSet.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strong spacetime convergence with bounds at good times

A single countable exceptional time set is null for Lebesgue measure. The amplitude bound is needed only at good interior times; values on the exceptional set and outside the time cylinder are unrestricted.

  1. theorem OAI.RegularPointCoordinates.uniform_slices_spacetime_L2_on_good_times line 19