Kinetic action bounds for flow escape

These estimates are independent of Euler and of the Comparator statement. They expose the flow and energy hypotheses needed to exclude arrival from spatial infinity. In particular, no global bound on the pointwise velocity or its derivatives is used in the escape estimate.

theorem Euler.ComparatorBridge.norm_integral_sq_le_action {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (V : α → E) (hV : MeasureTheory.MemLp V 2 μ) : ‖∫ (t : α), V t ∂μ‖ ^ 2 ≤ μ.real Set.univ * ∫ (t : α), ‖V t‖ ^ 2 ∂μ

Cauchy--Schwarz for a vector-valued integral against a finite measure.

theorem Euler.ComparatorBridge.curve_displacement_sq_le_action {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (a b : ℝ) (hab : a ≤ b) (X V : ℝ → E) (hX : ContinuousOn X (Set.Icc a b)) (hV : ContinuousOn V (Set.Icc a b)) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt X (V t) t) : ‖X b - X a‖ ^ 2 ≤ (b - a) * ∫ (t : ℝ) in Set.Icc a b, ‖V t‖ ^ 2

The displacement of a differentiable curve is bounded by its kinetic action.

theorem Euler.ComparatorBridge.curve_escape_sq_le_action {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T K R s : ℝ) (hT : 0 ≤ T) (hKR : K ≤ R) (hs : s ∈ Set.Icc 0 T) (X V : ℝ → E) (hX : ContinuousOn X (Set.Icc 0 T)) (hV : ContinuousOn V (Set.Icc 0 T)) (hderiv : ∀ t ∈ Set.Ioo 0 T, HasDerivAt X (V t) t) (hstart : ‖X 0‖ ≤ K) (hescape : R ≤ ‖X s‖) : (R - K) ^ 2 ≤ T * ∫ (t : ℝ) in Set.Icc 0 T, ‖V t‖ ^ 2

A curve reaching radius R from radius at most K pays at least (R-K)^2 / T in action over [0,T].

theorem Euler.ComparatorBridge.flow_action_integrable_and_bound {E : Type u_1} [NormedAddCommGroup E] {α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν] (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] (X : α → β → β) (V : α → β → E) (hX : ∀ (t : α), MeasureTheory.MeasurePreserving (X t) μ μ) (hXe : ∀ (t : α), MeasurableEmbedding (X t)) (hm : MeasureTheory.AEStronglyMeasurable (fun (tx : α × β) => ‖V tx.1 (X tx.1 tx.2)‖ ^ 2) (ν.prod μ)) (hV : ∀ (t : α), MeasureTheory.MemLp (V t) 2 μ) (energy : ℝ) (henergy : ∀ (t : α), ∫ (x : β), ‖V t x‖ ^ 2 ∂μ ≤ energy) : MeasureTheory.Integrable (fun (x : β) => ∫ (t : α), ‖V t (X t x)‖ ^ 2 ∂ν) μ ∧ ∫ (x : β), ∫ (t : α), ‖V t (X t x)‖ ^ 2 ∂ν ∂μ ≤ ν.real Set.univ * energy

A measure-preserving flow converts the Eulerian energy bound into an integrable action with the same time-integrated bound.

theorem Euler.ComparatorBridge.escape_measure_le_of_action {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (S : Set α) (hS : MeasurableSet S) (hfinite : μ S ≠ ⊤) (action : α → ℝ) (ha : MeasureTheory.Integrable action μ) (ha0 : ∀ (x : α), 0 ≤ action x) (T K R energy : ℝ) (hT : 0 ≤ T) (hKR : K < R) (haenergy : ∫ (x : α), action x ∂μ ≤ T * energy) (hescape : ∀ x ∈ S, (R - K) ^ 2 ≤ T * action x) : μ.real S ≤ energy * T ^ 2 / (R - K) ^ 2

Markov's action estimate for any measurable family of escaping curves. The hypothesis on the integral of action is obtained by volume preservation and the Eulerian kinetic-energy bound.

theorem Euler.ComparatorBridge.flow_escape_measure_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) [MeasureTheory.SFinite μ] (T K R energy : ℝ) (hT : 0 ≤ T) (hKR : K < R) (X V : ℝ → E → E) (hX : ∀ (t : ℝ), MeasureTheory.MeasurePreserving (X t) μ μ) (hXe : ∀ (t : ℝ), MeasurableEmbedding (X t)) (hm : MeasureTheory.AEStronglyMeasurable (fun (tx : ℝ × E) => ‖V tx.1 (X tx.1 tx.2)‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (hV : ∀ (t : ℝ), MeasureTheory.MemLp (V t) 2 μ) (henergy : ∀ (t : ℝ), ∫ (x : E), ‖V t x‖ ^ 2 ∂μ ≤ energy) (hcurve : ∀ (x : E), ContinuousOn (fun (t : ℝ) => X t x) (Set.Icc 0 T)) (hspeed : ∀ (x : E), ContinuousOn (fun (t : ℝ) => V t (X t x)) (Set.Icc 0 T)) (hderiv : ∀ (x : E), ∀ t ∈ Set.Ioo 0 T, HasDerivAt (fun (r : ℝ) => X r x) (V t (X t x)) t) (S : Set E) (hS : MeasurableSet S) (hfinite : μ S ≠ ⊤) (hstart : ∀ x ∈ S, ‖X 0 x‖ ≤ K) (hescape : ∀ x ∈ S, ∃ t ∈ Set.Icc 0 T, R ≤ ‖X t x‖) : μ.real S ≤ energy * T ^ 2 / (R - K) ^ 2

A finite-energy measure-preserving flow can carry at most energy * T^2 / (R-K)^2 measure of points from radius K to radius R. The escaped set need not have a measurable choice of its hitting time.