OAI/Analysis/RCDHeat/HeatHopfZero.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatHopfZero, HeatKuwadaZero, RCDHeatTransportZero, HeatWasserstein, ActionDescentSqueeze.

  1. theorem OAI.RegularPointCoordinates.integral_mulLp_continuous line 21
  2. theorem OAI.RegularPointCoordinates.heat_hopf_entropy_dual_zero line 34
  3. theorem OAI.RegularPointCoordinates.heat_coupling_entropy_zero line 105
  4. theorem OAI.RegularPointCoordinates.heat_coupling_fisher_action_nonneg line 129
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_optimal_transport_action_nonneg line 153
  6. theorem OAI.RegularPointCoordinates.boltzmannEntropy_heatMeasure_eq line 192
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_wasserstein_HWI line 202
  8. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_wasserstein_entropy_action line 260
  9. theorem OAI.RegularPointCoordinates.tendsto_speed_of_action_descent line 306
  10. theorem OAI.RegularPointCoordinates.entropy_action_descent_right_speed line 333