OAI/Analysis/RCDHeat/RestrictedDensity.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: RestrictedDensity, MeasurableDistortion, PointwiseCD, LogCosh, DensityLogMidpoint, DimensionalEntropyIntegral.

  1. lemma OAI.RegularPointCoordinates.map_restrict_of_ae_factor line 20
  2. lemma OAI.RegularPointCoordinates.rnDeriv_normalized_map_restrict line 32
  3. lemma OAI.RegularPointCoordinates.rnDeriv_normalized_map_restrict_rpow line 52
  4. lemma OAI.RegularPointCoordinates.renyiIntegral_eq_inverse_density line 66

    Distinct definitions of this name: OAI/Geometry/RCD/Transport/RenyiInverseDensity.lean:13 (different declaration text). Qualify references as OAI.RegularPointCoordinates.renyiIntegral_eq_inverse_density@path.

  5. lemma OAI.RegularPointCoordinates.measurable_sigma line 87
  6. lemma OAI.RegularPointCoordinates.measurable_tau line 98
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_plan_pointwise_fullCD line 119
  8. lemma OAI.RegularPointCoordinates.hasDerivAt_log_cosh line 244
  9. lemma OAI.RegularPointCoordinates.hasDerivAt_sinh_div_cosh line 248
  10. lemma OAI.RegularPointCoordinates.convexOn_log_cosh line 256
  11. lemma OAI.RegularPointCoordinates.log_cosh_tangent line 264
  12. lemma OAI.RegularPointCoordinates.exp_average_cosh line 279
  13. lemma OAI.RegularPointCoordinates.log_exp_average line 284
  14. lemma OAI.RegularPointCoordinates.dimensional_log_midpoint line 288
  15. lemma OAI.RegularPointCoordinates.density_dimensional_log_midpoint line 313
  16. lemma OAI.RegularPointCoordinates.dimensional_log_midpoint_integral line 348