OAI/Geometry/RCD/Heat/TimeLowerEnvelope.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A bounded monotone envelope of prescribed time slices

The baseline makes the supremum nonempty at every real time, including times before the first prescribed slice.

  1. def OAI.RegularPointCoordinates.timeLowerEnvelope line 17
  2. theorem OAI.RegularPointCoordinates.envelope_nonempty line 20
  3. theorem OAI.RegularPointCoordinates.envelope_bddAbove line 24
  4. theorem OAI.RegularPointCoordinates.timeLowerEnvelope_bounds line 32
  5. theorem OAI.RegularPointCoordinates.timeLowerEnvelope_monotone line 42
  6. theorem OAI.RegularPointCoordinates.sample_le_timeLowerEnvelope line 50
  7. theorem OAI.RegularPointCoordinates.timeLowerEnvelope_le_sample line 55
  8. theorem OAI.RegularPointCoordinates.timeLowerEnvelope_countable_discontinuities line 63