InitialConeFromInterval.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The initial cone only uses the driving derivative inside its interval; no continuation of that derivative beyond the terminal time is needed.

lemma OAI.SLEExactGauge.exists_initial_reverse_cone_of_interval_derivative line 14