OAI/Geometry/RCD/Transport/RenyiPathSemicontinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Semicontinuity for supported Rényi paths and continuity of the chord

  1. theorem OAI.RegularPointCoordinates.continuous_sigma_nonpos_time line 13
  2. theorem OAI.RegularPointCoordinates.continuous_reducedChord line 27
  3. theorem OAI.RegularPointCoordinates.upperSemicontinuous_renyiIntegral line 38
  4. theorem OAI.RegularPointCoordinates.upperSemicontinuous_supported_renyiPath line 51
  5. theorem OAI.RegularPointCoordinates.renyiIntegral_ne_top_of_support line 67
  6. theorem OAI.RegularPointCoordinates.ge_continuous_of_dense line 76
  7. theorem OAI.RegularPointCoordinates.continuousAt_of_upperSemicontinuous_lower line 84