OAI/Analysis/RCDHeat/HeatFisher.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatFisher, HeatL1, EntropyBound, WeightedSlope, WeightedScaled, RadialCutoff.

  1. def OAI.RegularPointCoordinates.regularizedFisher line 20
  2. theorem OAI.RegularPointCoordinates.regularizedFisher_eq_integral line 23
  3. theorem OAI.RegularPointCoordinates.regularizedFisher_nonneg line 31
  4. theorem OAI.RegularPointCoordinates.heatAt_regularizedEntropy_antitoneOn line 36
  5. theorem OAI.RegularPointCoordinates.heatAt_regularizedEntropy_dissipation line 44
  6. theorem OAI.RegularPointCoordinates.regularizedFisher_integral_le line 52
  7. theorem OAI.RegularPointCoordinates.heatAt_integralOn_le line 73
  8. theorem OAI.RegularPointCoordinates.lp_integrableOn_of_finite line 92
  9. theorem OAI.RegularPointCoordinates.spanningSets_aecover line 98
  10. theorem OAI.RegularPointCoordinates.heatAt_integrable_of_nonneg line 105
  11. theorem OAI.RegularPointCoordinates.heatAt_integral_le_of_nonneg line 120
  12. theorem OAI.RegularPointCoordinates.heatAt_mono line 128
  13. theorem OAI.RegularPointCoordinates.heatAt_abs_le line 132
  14. theorem OAI.RegularPointCoordinates.heatAt_integrable line 141
  15. theorem OAI.RegularPointCoordinates.heatAt_integral_abs_le line 147
  16. theorem OAI.RegularPointCoordinates.regularizedEntropy_le line 161
  17. theorem OAI.RegularPointCoordinates.regularizedLog_exp_bound line 170
  18. theorem OAI.RegularPointCoordinates.regularizedPotential_le_mass line 186
  19. theorem OAI.RegularPointCoordinates.regularizedPotential_exp_le line 197
  20. theorem OAI.RegularPointCoordinates.regularizedReciprocal_eq line 208
  21. theorem OAI.RegularPointCoordinates.regularizedReciprocal_pos line 216
  22. theorem OAI.RegularPointCoordinates.regularizedReciprocal_inv_le line 221
  23. theorem OAI.RegularPointCoordinates.weighted_young line 227
  24. theorem OAI.RegularPointCoordinates.energyForm_weighted_young line 237
  25. theorem OAI.RegularPointCoordinates.energyForm_smul_right line 293
  26. theorem OAI.RegularPointCoordinates.weightedSlope_smul line 298
  27. theorem OAI.RegularPointCoordinates.energyForm_weighted_young_scaled line 307
  28. def OAI.RegularPointCoordinates.radialCutoff line 328
  29. theorem OAI.RegularPointCoordinates.radialCutoff_bounds line 331
  30. theorem OAI.RegularPointCoordinates.radialCutoff_eq_one line 334
  31. theorem OAI.RegularPointCoordinates.radialCutoff_eq_zero line 340
  32. theorem OAI.RegularPointCoordinates.radialCutoff_lipschitz line 346
  33. theorem OAI.RegularPointCoordinates.radialCutoff_hasCompactSupport line 364
  34. def OAI.RegularPointCoordinates.SobolevSpace.ofLipschitzCompact line 374
  35. theorem OAI.RegularPointCoordinates.SobolevSpace.ofLipschitzCompact_coe line 382
  36. theorem OAI.RegularPointCoordinates.SobolevSpace.ofLipschitzCompact_minimalSlope_le line 387
  37. def OAI.RegularPointCoordinates.radialSobolevCutoff line 397
  38. theorem OAI.RegularPointCoordinates.radialSobolevCutoff_coe line 401
  39. theorem OAI.RegularPointCoordinates.radialSobolevCutoff_slope_le line 405