Short-time compact vorticity from finite-energy truncations

The auxiliary characteristics are global flows of compact solenoidal truncations. The construction does not require global trajectories of the untruncated Comparator velocity.

Actual backward particle flows of smooth finite-energy truncations. The maps are clamped outside the chosen interval, preserving volume at every real parameter. Reversing from the other endpoint recovers the original coefficient and supplies the forward paths used in local trapping arguments.

def Euler.ComparatorBridge.TruncatedBackwardFlow.reverseTime (T : ℝ) (hT1 : T ≤ 1) : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 1))

Time reversal into the original unit interval.

Equations

• Euler.ComparatorBridge.TruncatedBackwardFlow.reverseTime T hT1 = { toFun := fun (s : ↑(Set.Icc 0 T)) => ⟨T - ↑s, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def Euler.ComparatorBridge.TruncatedBackwardFlow.reverseField {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT1 : T ≤ 1) : SmoothTimeField (↑(Set.Icc 0 T)) E E

Minus the original velocity at reversed time.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.reverseField_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT1 : T ≤ 1) (s : ↑(Set.Icc 0 T)) (x : E) : ((reverseField A T hT1).field s) x = -(A.field ((reverseTime T hT1) s)) x

noncomputable def Euler.ComparatorBridge.TruncatedBackwardFlow.flowData {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) : EulerBoundedLipschitzFlow.Data E

The existing global Picard construction for the reversed field.

Equations

• Euler.ComparatorBridge.TruncatedBackwardFlow.flowData A T hT hT1 = EulerSmoothBanachFlow.flowData T hT (Euler.ComparatorBridge.TruncatedBackwardFlow.reverseField A T hT1)

noncomputable def Euler.ComparatorBridge.TruncatedBackwardFlow.homeomorph {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (s : ℝ) : E ≃ₜ E

Backward flow homeomorphisms, clamped outside the chosen interval.

Equations

• Euler.ComparatorBridge.TruncatedBackwardFlow.homeomorph A T hT hT1 s = (Euler.ComparatorBridge.TruncatedBackwardFlow.flowData A T hT hT1).flowHomeomorph 0 ↑(Set.projIcc 0 T hT s)

noncomputable def Euler.ComparatorBridge.TruncatedBackwardFlow.velocity {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (s : ℝ) (x : E) : E

The globally defined, endpoint-extended backward coefficient.

Equations

• Euler.ComparatorBridge.TruncatedBackwardFlow.velocity A T hT hT1 s x = (Euler.ComparatorBridge.TruncatedBackwardFlow.flowData A T hT hT1).velocity s x

@[simp]

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.velocity_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (s : ℝ) (x : E) : velocity A T hT hT1 s x = -(A.field ((reverseTime T hT1) (Set.projIcc 0 T hT s))) x

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.velocity_eq_realField {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (s : ℝ) (hs : s ∈ Set.Icc 0 T) (x : E) : velocity A T hT hT1 s x = -SmoothTimeField.realField 1 ⋯ A (T - s) x

On the interval, the velocity is the original field at reversed time.

@[simp]

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.homeomorph_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (s : ℝ) (x : E) : (homeomorph A T hT hT1 s) x = (flowData A T hT hT1).forward (↑(Set.projIcc 0 T hT s)) x

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.homeomorph_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (x : E) : (homeomorph A T hT hT1 0) x = x

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.homeomorph_joint_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) : Continuous fun (sx : ℝ × E) => (homeomorph A T hT hT1 sx.1) sx.2

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.velocity_joint_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) : Continuous (Function.uncurry (velocity A T hT hT1))

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.curve_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (x : E) : Continuous fun (s : ℝ) => (homeomorph A T hT hT1 s) x

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.speed_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (x : E) : Continuous fun (s : ℝ) => velocity A T hT hT1 s ((homeomorph A T hT hT1 s) x)

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.curve_hasDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (x : E) (s : ℝ) (hs : s ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => (homeomorph A T hT hT1 r) x) (velocity A T hT hT1 s ((homeomorph A T hT hT1 s) x)) s

noncomputable def Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (a : E) (r : ℝ) : E

A trajectory in the original time direction.

Equations

• Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath A T hT hT1 a r = (Euler.ComparatorBridge.TruncatedBackwardFlow.flowData A T hT hT1).flow T (T - r) a

@[simp]

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (a : E) : endpointPath A T hT hT1 a 0 = a

@[simp]

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath_end {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (a : E) : endpointPath A T hT hT1 a T = (homeomorph A T hT hT1 T).symm a

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (a : E) : Continuous (endpointPath A T hT hT1 a)

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath_hasDerivAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (a : E) (r : ℝ) (hr : r ∈ Set.Ioo 0 T) : HasDerivAt (endpointPath A T hT hT1 a) (SmoothTimeField.realField 1 ⋯ A r (endpointPath A T hT hT1 a r)) r

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.endpointPath_hasDerivAt_field {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (a : E) (r : ℝ) (hr : r ∈ Set.Ioo 0 T) : HasDerivAt (endpointPath A T hT hT1 a) ((A.field ⟨r, ⋯⟩) (endpointPath A T hT hT1 a r)) r

The same derivative with the original subtype-indexed coefficient.

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.reverseField_divergence {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT1 : T ≤ 1) (hdiv : ∀ (t : ↑(Set.Icc 0 1)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (s : ↑(Set.Icc 0 T)) (x : E) : (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑((reverseField A T hT1).field s)) x) = 0

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.homeomorph_measurePreserving {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hdiv : ∀ (t : ↑(Set.Icc 0 1)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (s : ℝ) : MeasureTheory.MeasurePreserving (⇑(homeomorph A T hT hT1 s)) μ μ

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.velocity_memLp {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) [MeasurableSpace E] (μ : MeasureTheory.Measure E) (hmem : ∀ (t : ↑(Set.Icc 0 1)), MeasureTheory.MemLp (⇑(A.field t)) 2 μ) (s : ℝ) : MeasureTheory.MemLp (velocity A T hT hT1 s) 2 μ

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.velocity_energy {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) [MeasurableSpace E] (μ : MeasureTheory.Measure E) (energy : ℝ) (henergy : ∀ (t : ↑(Set.Icc 0 1)), ∫ (x : E), ‖(A.field t) x‖ ^ 2 ∂μ ≤ energy) (s : ℝ) : ∫ (x : E), ‖velocity A T hT hT1 s x‖ ^ 2 ∂μ ≤ energy

theorem Euler.ComparatorBridge.TruncatedBackwardFlow.action_joint_measurable {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : SmoothTimeField (↑(Set.Icc 0 1)) E E) (T : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) : MeasureTheory.AEStronglyMeasurable (fun (sx : ℝ × E) => ‖velocity A T hT hT1 sx.1 ((homeomorph A T hT hT1 sx.1) sx.2)‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)

No vorticity arriving from spatial infinity

The flow hypotheses below describe globally defined approximations to backward characteristics. Their kinetic energy is uniformly bounded. On paths which stay inside the approximation radius, nonzero endpoint vorticity must come from the initial vorticity support. Initial support is trapped by the inverse endpoint maps in one common ball. These hypotheses exclude all nonzero vorticity outside that ball; no global pointwise velocity bound is needed.

structure Euler.ComparatorBridge.BackwardVorticityFlows (T energy supportRadius : ℝ) (K : Set (EuclideanSpace ℝ (Fin 3))) (w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) : Type

Approximate backward characteristics for a vorticity field at one time. The parameter R is the spatial radius on which transport is valid. The time parameter s runs backward from the endpoint (s=0) to the initial time (s=T).

• flow : ℝ → ℝ → EuclideanSpace ℝ (Fin 3) ≃ₜ EuclideanSpace ℝ (Fin 3)

  Flow of BackwardVorticityFlows, of type ℝ → ℝ → ℝ³ ≃ₜ ℝ³.

• velocity : ℝ → ℝ → EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)

  Velocity field of BackwardVorticityFlows, of type ℝ → ℝ → ℝ³ → ℝ³.

• time_nonneg : 0 ≤ T
• preserves_volume (R s : ℝ) : MeasureTheory.MeasurePreserving (⇑(self.flow R s)) MeasureTheory.volume MeasureTheory.volume
• initial_map (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) : (self.flow R 0) x = x
• joint_measurable (R : ℝ) : MeasureTheory.AEStronglyMeasurable (fun (sx : ℝ × EuclideanSpace ℝ (Fin 3)) => ‖self.velocity R sx.1 ((self.flow R sx.1) sx.2)‖ ^ 2) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod MeasureTheory.volume)
• velocity_memLp (R s : ℝ) : MeasureTheory.MemLp (self.velocity R s) 2 MeasureTheory.volume
• energy_bound (R s : ℝ) : ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖self.velocity R s x‖ ^ 2 ≤ energy
• curve_continuous (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) : ContinuousOn (fun (s : ℝ) => (self.flow R s) x) (Set.Icc 0 T)
• speed_continuous (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) : ContinuousOn (fun (s : ℝ) => self.velocity R s ((self.flow R s) x)) (Set.Icc 0 T)
• curve_derivative (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) (s : ℝ) : s ∈ Set.Ioo 0 T → HasDerivAt (fun (r : ℝ) => (self.flow R r) x) (self.velocity R s ((self.flow R s) x)) s
• initial_support : Function.support w₀ ⊆ K
• transport_nonzero (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) : (∀ s ∈ Set.Icc 0 T, ‖(self.flow R s) x‖ < R) → w x ≠ 0 → w₀ ((self.flow R T) x) ≠ 0
• forward_trap (R : ℝ) (a : EuclideanSpace ℝ (Fin 3)) : a ∈ K → ‖(self.flow R T).symm a‖ ≤ supportRadius

theorem Euler.ComparatorBridge.BackwardVorticityFlows.escapes {T energy supportRadius : ℝ} {K : Set (EuclideanSpace ℝ (Fin 3))} {w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (F : BackwardVorticityFlows T energy supportRadius K w₀ w) (R : ℝ) (x : EuclideanSpace ℝ (Fin 3)) (hx : supportRadius < ‖x‖) (hw : w x ≠ 0) : ∃ s ∈ Set.Icc 0 T, R ≤ ‖(F.flow R s) x‖

A nonzero-vorticity endpoint outside the trapped support has to leave every approximation ball when traced backward.

theorem Euler.ComparatorBridge.BackwardVorticityFlows.measure_nonzero_outside_le {T energy supportRadius : ℝ} {K : Set (EuclideanSpace ℝ (Fin 3))} {w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (F : BackwardVorticityFlows T energy supportRadius K w₀ w) (S : Set (EuclideanSpace ℝ (Fin 3))) (hS : MeasurableSet S) (hfinite : MeasureTheory.volume S ≠ ⊤) (K₀ R : ℝ) (hKR : K₀ < R) (hSbound : ∀ x ∈ S, ‖x‖ ≤ K₀) (hSoutside : ∀ x ∈ S, supportRadius < ‖x‖) (hSnonzero : ∀ x ∈ S, w x ≠ 0) : MeasureTheory.volume.real S ≤ energy * T ^ 2 / (R - K₀) ^ 2

Every bounded measurable set of nonzero vorticity outside the support ball has the quantitative escape bound.

theorem Euler.ComparatorBridge.BackwardVorticityFlows.measure_nonzero_outside_eq_zero {T energy supportRadius : ℝ} {K : Set (EuclideanSpace ℝ (Fin 3))} {w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (F : BackwardVorticityFlows T energy supportRadius K w₀ w) (S : Set (EuclideanSpace ℝ (Fin 3))) (hS : MeasurableSet S) (hfinite : MeasureTheory.volume S ≠ ⊤) (K₀ : ℝ) (hSbound : ∀ x ∈ S, ‖x‖ ≤ K₀) (hSoutside : ∀ x ∈ S, supportRadius < ‖x‖) (hSnonzero : ∀ x ∈ S, w x ≠ 0) : MeasureTheory.volume.real S = 0

Sending the approximation radius to infinity rules out a positive measure set of bounded nonzero-vorticity endpoints outside the trapped ball.

theorem Euler.ComparatorBridge.BackwardVorticityFlows.zero_outside {T energy supportRadius : ℝ} {K : Set (EuclideanSpace ℝ (Fin 3))} {w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (F : BackwardVorticityFlows T energy supportRadius K w₀ w) (hw : Continuous w) (x : EuclideanSpace ℝ (Fin 3)) (hx : supportRadius < ‖x‖) : w x = 0

Continuity removes the null exceptional set: vorticity vanishes pointwise outside the common ball containing the transported initial support.

theorem Euler.ComparatorBridge.BackwardVorticityFlows.support_subset_closedBall {T energy supportRadius : ℝ} {K : Set (EuclideanSpace ℝ (Fin 3))} {w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (F : BackwardVorticityFlows T energy supportRadius K w₀ w) (hw : Continuous w) : Function.support w ⊆ Metric.closedBall 0 supportRadius

The transported field is supported in one fixed compact ball.

theorem Euler.ComparatorBridge.BackwardVorticityFlows.hasCompactSupport {T energy supportRadius : ℝ} {K : Set (EuclideanSpace ℝ (Fin 3))} {w₀ w : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} (F : BackwardVorticityFlows T energy supportRadius K w₀ w) (hw : Continuous w) : HasCompactSupport w

Short-time confinement uses a velocity bound only inside the trapping ball.

theorem EulerComparatorLocalFlow.norm_sub_le_mul_of_hasDerivAt_Ioo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X X' : ℝ → E) {T M : ℝ} (hT : 0 < T) (hM : 0 ≤ M) (hX : ContinuousOn X (Set.Icc 0 T)) (hderiv : ∀ s ∈ Set.Ioo 0 T, HasDerivAt X (X' s) s) (hbound : ∀ s ∈ Set.Ioo 0 T, ‖X' s‖ ≤ M) : ‖X T - X 0‖ ≤ M * T

The mean-value bound up to both endpoints, with derivatives required only in the interior.

theorem EulerComparatorLocalFlow.norm_lt_of_local_speed_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (X : ℝ → E) (V : ℝ → E → E) {δ A B M : ℝ} (hM : 0 ≤ M) (hAB : A < B) (hsmall : δ * M < B - A) (hX : ContinuousOn X (Set.Icc 0 δ)) (hderiv : ∀ s ∈ Set.Ioo 0 δ, HasDerivAt X (V s (X s)) s) (hinitial : ‖X 0‖ ≤ A) (hbound : ∀ s ∈ Set.Icc 0 δ, ∀ (x : E), ‖x‖ ≤ B → ‖V s x‖ ≤ M) (t : ℝ) : t ∈ Set.Icc 0 δ → ‖X t‖ < B

A trajectory cannot first leave the ball before the local speed budget is exhausted. No bound on the velocity outside ‖x‖ ≤ B is used.

theorem EulerComparatorLocalFlow.exists_local_speed_budget {E : Type u_1} [NormedAddCommGroup E] [ProperSpace E] (u : ℝ → E → E) {A B : ℝ} (hAB : A < B) (hu : ContinuousOn (Function.uncurry u) (Set.Icc 0 1 ×ˢ Metric.closedBall 0 B)) : ∃ (δ : ℝ) (M : ℝ), 0 < δ ∧ δ ≤ 1 ∧ 0 < M ∧ δ * M < B - A ∧ ∀ s ∈ Set.Icc 0 δ, ∀ (x : E), ‖x‖ ≤ B → ‖u s x‖ ≤ M

Compactness supplies a common speed bound and positive time budget on a fixed ball.

Nonzero vorticity cannot disappear on an existing reverse-time particle trajectory of a Comparator solution.

theorem Euler.EulerExistenceAndSmoothnessR3.vorticity_ne_zero_along_reverse_trajectory {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (X : ℝ → EulerSmoothLimit.Space) (T : ℝ) (hT : 0 ≤ T) (hX : ContinuousOn X (Set.Icc 0 T)) (hXd : ∀ s ∈ Set.Ioo 0 T, HasDerivAt X (-v (X s) (T - s)) s) (hne : EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => v x T) (X 0) ≠ 0) : EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => v x 0) (X T) ≠ 0

A reverse-time particle path carrying nonzero vorticity at time T reaches a point with nonzero initial vorticity.

theorem Euler.EulerExistenceAndSmoothnessR3.vorticity_ne_zero_along_reverse_trajectory_of_agrees {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (X : ℝ → EulerSmoothLimit.Space) (w : ℝ → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (T : ℝ) (hT : 0 ≤ T) (hX : ContinuousOn X (Set.Icc 0 T)) (hXd : ∀ s ∈ Set.Ioo 0 T, HasDerivAt X (-w s (X s)) s) (hw : ∀ s ∈ Set.Ioo 0 T, w s (X s) = v (X s) (T - s)) (hne : EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => v x T) (X 0) ≠ 0) : EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => v x 0) (X T) ≠ 0

A path for a modified reverse-time velocity has the same nonzero vorticity transport whenever that velocity agrees with Euler along the path.

theorem Euler.EulerExistenceAndSmoothnessR3.exists_local_trapping_constants {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (hc : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl u₀)) : ∃ (A : ℝ) (M : ℝ) (δ : ℝ), 0 < A ∧ 0 < M ∧ 0 < δ ∧ δ ≤ 1 ∧ δ * M < 1 ∧ (∀ x ∈ tsupport (EulerMeanCutoffCurl.vectorCurl u₀), ‖x‖ ≤ A) ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ A + 1 → ‖v x t‖ ≤ M

One compact spacetime cylinder supplies a common local speed bound and one positive trapping time for every truncation agreeing on that cylinder.

theorem Euler.EulerExistenceAndSmoothnessR3.truncation_realField_agrees {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} (F : ComparatorBridge.FiniteEnergyTruncationFamily v) (R : ℝ) (hR : 0 < R) (r : ℝ) (hr : r ∈ Set.Icc 0 1) (x : EulerSmoothLimit.Space) (hx : ‖x‖ < R) : SmoothTimeField.realField 1 ⋯ (F.coefficient R) r x = v x r

noncomputable def Euler.EulerExistenceAndSmoothnessR3.locallyTrappedBackwardFlows {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (F : ComparatorBridge.FiniteEnergyTruncationFamily v) (A M δ T : ℝ) (hA : 0 < A) (hM : 0 < M) (hδ1 : δ ≤ 1) (hδM : δ * M < 1) (hT : T ∈ Set.Icc 0 δ) (hAbound : ∀ x ∈ tsupport (EulerMeanCutoffCurl.vectorCurl u₀), ‖x‖ ≤ A) (hspeed : ∀ t ∈ Set.Icc 0 1, ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ A + 1 → ‖v x t‖ ≤ M) : ComparatorBridge.BackwardVorticityFlows T F.energy (A + 1) (tsupport (EulerMeanCutoffCurl.vectorCurl u₀)) (EulerMeanCutoffCurl.vectorCurl u₀) (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => v x T)

The approximation radius is enlarged to include the one fixed trapping ball. This gives valid approximants even for nonpositive requested radii.

Equations

• One or more equations did not get rendered due to their size.

theorem Euler.EulerExistenceAndSmoothnessR3.local_compact_vorticity_of_truncationFamily {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (F : ComparatorBridge.FiniteEnergyTruncationFamily v) (hc : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl u₀)) : ∃ (δ : ℝ) (B : ℝ), 0 < δ ∧ ∀ t ∈ Set.Icc 0 δ, tsupport (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => v x t) ⊆ Metric.closedBall 0 B

Finite-energy solenoidal truncations imply compact vorticity for a uniform positive interval, using only the Comparator solution assumptions.

theorem Euler.EulerExistenceAndSmoothnessR3.local_compact_vorticity {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (hc : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl u₀)) : ∃ (δ : ℝ) (B : ℝ), 0 < δ ∧ ∀ t ∈ Set.Icc 0 δ, tsupport (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => v x t) ⊆ Metric.closedBall 0 B

Compact initial vorticity stays in one compact ball for a positive time for every Comparator solution. The auxiliary global trajectories are those of the explicitly constructed finite-energy solenoidal truncations.