OAI/Geometry/RCD/Sobolev/UniformSlicesWeightedLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted spacetime value pairings along the common subsequence

Spatial and temporal tests need only be integrable. Uniform slice bounds and the common countable exceptional set provide the domination.

  1. theorem OAI.RegularPointCoordinates.uniform_slices_weighted_spacetime_limit line 16