OAI/Analysis/RCDHeat/UpperLipschitzEnvelope.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: UpperLipschitzEnvelope, CompactMajorant, ProperTransportDuality.

  1. def OAI.RegularPointCoordinates.upperLipschitzEnvelope line 15
  2. theorem OAI.RegularPointCoordinates.upperLipschitzEnvelope_bdd line 17
  3. theorem OAI.RegularPointCoordinates.le_upperLipschitzEnvelope line 22
  4. theorem OAI.RegularPointCoordinates.upperLipschitzEnvelope_nonpos line 26
  5. theorem OAI.RegularPointCoordinates.upperLipschitzEnvelope_lipschitz line 31
  6. theorem OAI.RegularPointCoordinates.upperLipschitzEnvelope_tendsto line 50
  7. def OAI.RegularPointCoordinates.compactUpperApprox line 85
  8. theorem OAI.RegularPointCoordinates.compactUpperApprox_bounds line 87
  9. theorem OAI.RegularPointCoordinates.compactUpperApprox_tendsto line 96
  10. theorem OAI.RegularPointCoordinates.compactUpperApprox_hasCompactSupport line 106
  11. theorem OAI.RegularPointCoordinates.compactUpperApprox_lipschitz line 109
  12. theorem OAI.RegularPointCoordinates.compactUpperApprox_integral_tendsto line 117
  13. theorem OAI.RegularPointCoordinates.exists_support_sublinear line 144
  14. def OAI.RegularPointCoordinates.BoundedTransport.separatedSum line 188
  15. theorem OAI.RegularPointCoordinates.BoundedTransport.bounded_continuous_integrable line 191
  16. theorem OAI.RegularPointCoordinates.BoundedTransport.separatedSum_integral_mono line 193
  17. def OAI.RegularPointCoordinates.BoundedTransport.transportEnvelopeValues line 208
  18. def OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope line 211
  19. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelopeValues_nonempty line 214
  20. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelopeValues_bddBelow line 223
  21. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_le line 237
  22. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_separatedSum line 241
  23. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_zero line 248
  24. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_add line 253
  25. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_smul_le line 273
  26. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_smul line 288
  27. theorem OAI.RegularPointCoordinates.BoundedTransport.transportEnvelope_support line 306
  28. def OAI.RegularPointCoordinates.BoundedTransport.cutoff line 341
  29. theorem OAI.RegularPointCoordinates.BoundedTransport.cutoff_bounds line 350
  30. theorem OAI.RegularPointCoordinates.BoundedTransport.cutoff_eq_one line 353
  31. theorem OAI.RegularPointCoordinates.BoundedTransport.cutoff_tendsto line 359
  32. theorem OAI.RegularPointCoordinates.BoundedTransport.cutoff_prod line 365
  33. theorem OAI.RegularPointCoordinates.BoundedTransport.cutoff_integral_tendsto line 379
  34. theorem OAI.RegularPointCoordinates.BoundedTransport.positive_transport_representation line 402
  35. theorem OAI.RegularPointCoordinates.BoundedTransport.proper_transport_primal_dual line 524
  36. theorem OAI.RegularPointCoordinates.BoundedTransport.coupling_sequence_compact line 569
  37. def OAI.RegularPointCoordinates.BoundedTransport.truncatedCost line 619
  38. theorem OAI.RegularPointCoordinates.BoundedTransport.truncatedCost_apply line 624
  39. theorem OAI.RegularPointCoordinates.BoundedTransport.truncatedCost_nonneg line 626
  40. theorem OAI.RegularPointCoordinates.BoundedTransport.truncatedCost_mono line 628
  41. theorem OAI.RegularPointCoordinates.BoundedTransport.truncatedCost_iSup line 632
  42. theorem OAI.RegularPointCoordinates.BoundedTransport.coupling_of_truncations line 647
  43. theorem OAI.RegularPointCoordinates.BoundedTransport.coupling_of_dual_bound line 692