OAI/Analysis/RCDHeat/ProbabilityCutoff.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: ProbabilityCutoff, DensityFactorLaws, EntropyCutoff, HeatGeneralHWI, HeatFiniteHWI, HeatFullHWI.

  1. theorem OAI.RegularPointCoordinates.probability_cutoff_factors line 19
  2. theorem OAI.RegularPointCoordinates.realDensity_probability line 80
  3. theorem OAI.RegularPointCoordinates.realDensity_entropy line 86
  4. theorem OAI.RegularPointCoordinates.withDensity_real_rnDeriv line 93
  5. theorem OAI.RegularPointCoordinates.density_factor_entropy_integrable line 102
  6. theorem OAI.RegularPointCoordinates.entropy_cutoff_recovery line 133
  7. theorem OAI.RegularPointCoordinates.FullCD.heat_wasserstein_HWI line 202
  8. theorem OAI.RegularPointCoordinates.FullCD.heat_HWI_finite line 253
  9. theorem OAI.RegularPointCoordinates.FullCD.heat_wasserstein_HWI_finite line 350