OAI/Analysis/RCDHeat/SqrtPairSlope.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: SqrtPairSlope, EntropyMixture, SqrtMixture, MeasureMixture, CouplingMoment.

  1. theorem OAI.RegularPointCoordinates.sqrt_pair_increment line 15
  2. theorem OAI.RegularPointCoordinates.lipschitz_sqrt_pair line 21
  3. theorem OAI.RegularPointCoordinates.localSlope_le_sum_of_increment line 33
  4. theorem OAI.RegularPointCoordinates.localSlope_sqrt_pair line 55
  5. theorem OAI.RegularPointCoordinates.IsSlopeMajorant.sqrt_pair line 60
  6. theorem OAI.RegularPointCoordinates.mul_log_add_lower line 75
  7. theorem OAI.RegularPointCoordinates.mul_log_mul line 84
  8. theorem OAI.RegularPointCoordinates.entropy_mixture_bounds line 92
  9. theorem OAI.RegularPointCoordinates.entropy_mixture_integrable line 106
  10. theorem OAI.RegularPointCoordinates.entropy_mixture_integral_bounds line 130
  11. theorem OAI.RegularPointCoordinates.entropy_mixture_tendsto line 159
  12. def OAI.RegularPointCoordinates.sqrtMixture line 186
  13. theorem OAI.RegularPointCoordinates.sqrtMixture_sq line 189
  14. theorem OAI.RegularPointCoordinates.sqrtMixture_eq_pair line 193
  15. theorem OAI.RegularPointCoordinates.sqrtMixture_lipschitz line 197
  16. theorem OAI.RegularPointCoordinates.sqrtMixture_pos line 203
  17. theorem OAI.RegularPointCoordinates.sqrtMixture_exp_log_lipschitz line 208
  18. theorem OAI.RegularPointCoordinates.IsSlopeMajorant.sqrtMixture line 241
  19. theorem OAI.RegularPointCoordinates.sqrtMixture_majorant_tendsto line 249
  20. def OAI.RegularPointCoordinates.measureMixture line 262
  21. theorem OAI.RegularPointCoordinates.measureMixture_probability line 264
  22. theorem OAI.RegularPointCoordinates.measureMixture_map line 270
  23. theorem OAI.RegularPointCoordinates.measureMixture_self line 274
  24. theorem OAI.RegularPointCoordinates.measureMixture_integrable line 278
  25. theorem OAI.RegularPointCoordinates.measureMixture_absolutelyContinuous line 282
  26. theorem OAI.RegularPointCoordinates.withDensity_mixture line 286
  27. theorem OAI.RegularPointCoordinates.finiteSecondMoment_of_integrable_dist line 303
  28. theorem OAI.RegularPointCoordinates.transportCost_mixture line 312
  29. theorem OAI.RegularPointCoordinates.mixture_coupling line 317
  30. theorem OAI.RegularPointCoordinates.transportCost_mixture_tendsto line 326
  31. theorem OAI.RegularPointCoordinates.coupling_dist_sq_integrable line 341
  32. theorem OAI.RegularPointCoordinates.coupling_transportCost_ne_top line 355
  33. theorem OAI.RegularPointCoordinates.product_coupling line 366