CompactWeightedDensityIntegral.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The compact-factor integral is the integral of its actual density

An endpoint law supported on a compact set is used through its exact pushforward density. This identifies the heat factors with integrals against bounded, compactly supported functions on the original space.

theorem OAI.RegularPointCoordinates.compact_weighted_density_integral line 19