Uniform area derivatives imply width comparison
ProvedOpenGA.nonempty_widthComparisonData_of_areaEvolutionfinite-extinctionwidth
Integrate the derivative upper bound on a common short interval using the mean-value inequality. The extra term given by the initial area gap divided by the interval length consumes at most that gap. The area-energy inequality bounds the initial slice supremum by the finite energy cap. Taking the supremum of the evolved slices gives exactly the short-time area comparison required by WidthComparisonData. The common interval and cutoff are essential hypotheses; pointwise variation of a single surface is insufficient.
Preamble
import Definitions.Def_OpenGA_WidthAreaEvolutionData set_option autoImplicit false open Set Filter open scoped Topology open OpenGA
Formal statement
theorem OpenGA.nonempty_widthComparisonData_of_areaEvolution {width : ℝ → ℝ} {time scalar : ℝ}
(D : WidthAreaEvolutionData width time scalar) :
Nonempty (WidthComparisonData width time scalar) := by sorrySource