Surgery profiles with uniform area evolution
DefinitionOpenGA_SurgeryAreaEvolutionDatafinite-extinctiongeometric-analysiswidth
Measured radial surgery data and scalar/width profiles, with uniform area-evolution data on each event-free interval. The width comparison inequality is not assumed: it is obtained by integrating the area derivative estimates. Radial comparison, the removed-volume budget, scalar estimates, and jump inequalities remain explicit hypotheses.
Definition code
import Definitions.Def_OpenGA_WidthAreaEvolutionData
import Definitions.Def_OpenGA_MeasuredSurgeryComparisonData
set_option autoImplicit false
open Set Filter
open scoped Topology
namespace OpenGA
structure SurgeryAreaEvolutionData (initialWidth finalTime : ℝ) where
volumeControl : MeasuredRadialSurgeryData
events_inside : volumeControl.events ⊆ Ioo 0 finalTime
finalTime_pos : 0 < finalTime
scalar : ℝ → ℝ → ℝ
width : ℝ → ℝ → ℝ
scalar_cont : ∀ a b, EventFreeInterval volumeControl.events finalTime a b →
ContinuousOn (scalar a) (Icc a b)
width_cont : ∀ a b, EventFreeInterval volumeControl.events finalTime a b →
ContinuousOn (width a) (Icc a b)
scalar_initial : -6 ≤ scalar 0 0
width_initial : width 0 0 ≤ initialWidth
width_nonneg : ∀ a b, EventFreeInterval volumeControl.events finalTime a b →
∀ t ∈ Icc a b, 0 ≤ width a t
scalar_slope : ∀ a b, EventFreeInterval volumeControl.events finalTime a b →
∀ t ∈ Ico a b, ∀ q : ℝ, q < (2 / 3 : ℝ) * (scalar a t) ^ 2 →
∀ᶠ s in 𝓝[>] t, q < slope (scalar a) t s
area_evolution : ∀ a b, EventFreeInterval volumeControl.events finalTime a b →
∀ t ∈ Ico a b, Nonempty (WidthAreaEvolutionData (width a) t (scalar a t))
scalar_jump : ∀ a b c,
EventFreeInterval volumeControl.events finalTime a b →
EventFreeInterval volumeControl.events finalTime b c → scalar a b ≤ scalar b b
width_jump : ∀ a b c,
EventFreeInterval volumeControl.events finalTime a b →
EventFreeInterval volumeControl.events finalTime b c → width b b ≤ width a b
end OpenGA
Source