OAI/Geometry/RCD/Heat/HeatWeightedRows.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exponentially weighted L² bounds for canonical heat-kernel rows

Testing the weighted evaluation functional on its own weighted row gives the dual estimate. The continuous kernel is constructed from the semigroup; no Gaussian bound is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_weighted_row line 24