OAI/Geometry/RCD/Heat/HeatActionBasepoint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

One action-gradient constant for all physical centers

The reference point used to construct the canonical kernel does not change the kernel, the compact heat factors, or their normalized action limits.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.canonicalHeatKernel_basepoint line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compactHeatFactor_basepoint line 28
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.fixedGaugeScaledPotential_basepoint line 36
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatConverges.basepoint line 44
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.uniform_centered_heat_action_realization line 53
  6. def OAI.RegularPointCoordinates.NoncollapsedRCD.centeredActionBound line 79
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.centeredActionBound_pos line 82