OAI/Geometry/RCD/Harmonic/RadialTimeSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One-sided CD support bounds at an arbitrary contraction time

Only the initial density bound is retained. This is the contribution which survives when the other endpoint concentrates at the pole.

  1. theorem OAI.RegularPointCoordinates.cd_time_renyi_lower line 19
  2. def OAI.RegularPointCoordinates.timeSupportFactor line 47
  3. theorem OAI.RegularPointCoordinates.timeSupportFactor_scale line 50
  4. theorem OAI.RegularPointCoordinates.FullCD.exists_time_ac_support_bound line 64