OAI/Geometry/RCD/Heat/BoundedHeatMixedMovingDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mixed Hessian errors under the actual bounded moving densities

Only the second direction has a uniform gradient bound. The first direction has small energy against the same moving weight as the Hessian integral.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_heat_mixed_moving_density line 22