OAI/Geometry/RCD/Heat/CompactHeatLocalVelocityHessianLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual local velocity Hessian converges on the common law subsequence

The forward diagonal has a spatial L1 limit. The mixed osmotic term tends to zero against the actual densities. The exact physical coefficient is 1/4.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.local_velocity_hessian_limit_of_forward line 27
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.local_velocity_intrinsic_hessian_limit line 166
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.local_velocity_hessian_limit line 228