OAI/Analysis/RCDHeat/WeightedCutoff.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: WeightedCutoff, MeasurableGluing, PointwiseMinimal, BoundedMultiplier, VaryingMultiplier, DerivativeSlope.

  1. def OAI.RegularPointCoordinates.clipUnit line 21
  2. theorem OAI.RegularPointCoordinates.clipUnit_lipschitz line 24
  3. theorem OAI.RegularPointCoordinates.clipUnit_bounds line 28
  4. theorem OAI.RegularPointCoordinates.clipUnit_eq_self line 32
  5. theorem OAI.RegularPointCoordinates.clipUnit_zero line 36
  6. theorem OAI.RegularPointCoordinates.eLpNorm_mul_eq_weight line 39
  7. theorem OAI.RegularPointCoordinates.exists_weighted_lipschitz_cutoff line 60
  8. def OAI.RegularPointCoordinates.unitMultiplier line 97
  9. theorem OAI.RegularPointCoordinates.unitMultiplier_coe line 103
  10. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.measurable_blend line 111
  11. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.inf line 155
  12. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_le line 187
  13. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_nonneg line 206
  14. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_add_le line 210
  15. def OAI.RegularPointCoordinates.boundedMultiplier line 223
  16. theorem OAI.RegularPointCoordinates.boundedMultiplier_coe line 228
  17. theorem OAI.RegularPointCoordinates.boundedMultiplier_norm_le line 232
  18. theorem OAI.RegularPointCoordinates.lpMultiplier_tendsto_of_ae line 243
  19. theorem OAI.RegularPointCoordinates.lpMultiplier_tendsto_of_ae_of_tendsto line 305
  20. theorem OAI.RegularPointCoordinates.localSlope_comp_hasDerivAt line 334