OAI/Analysis/RCDHeat/NormalizedCutoff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: NormalizedCutoff, DensityFactorEntropy, DensityResidual, DominatedCouplingRecovery, BoundedSobolevDescent.

  1. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.normalized_cutoff_recovery line 19
  2. theorem OAI.RegularPointCoordinates.density_factor_entropy_tendsto line 122
  3. theorem OAI.RegularPointCoordinates.density_residual_lintegral_tendsto_zero line 161
  4. theorem OAI.RegularPointCoordinates.dominated_density_coupling_recovery line 197
  5. theorem OAI.RegularPointCoordinates.FullCD.bounded_sobolev_HWI line 320