Uniformly compact vorticity of the canonical packet solution

All finite packet horizons contain the maximal open lifespan. H³ stability therefore passes their common vorticity support to every shorter ordinary Euler evolution, and hence to the canonical maximal field itself.

Zero initial vorticity remains zero along every genuine finite-stage particle trajectory. The proof uses the conserved antisymmetric pairing of the particle frame and its time derivative.

Conservation of the antisymmetric frame pairing for a particle flow whose acceleration gradient is a symmetric operator.

theorem Euler.ComparatorBridge.frame_wronskian_constant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F G H B : ℝ → E →L[ℝ] E) (T : ℝ) (hT : 0 < T) (hF : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt F (G t) (Set.Icc 0 T) t) (hG : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt G (H t) (Set.Icc 0 T) t) (hH : ∀ t ∈ Set.Icc 0 T, ∀ (v : E), (H t) v = -(B t) ((F t) v)) (hB : ∀ t ∈ Set.Icc 0 T, (↑(B t)).IsSymmetric) (v w : E) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : inner ℝ ((G t) v) ((F t) w) - inner ℝ ((F t) v) ((G t) w) = inner ℝ ((G 0) v) ((F 0) w) - inner ℝ ((F 0) v) ((G 0) w)

theorem Euler.ComparatorBridge.strain_symmetric_of_frame_wronskian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (F G H B S J : ℝ → E →L[ℝ] E) (T : ℝ) (hT : 0 < T) (hF : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt F (G t) (Set.Icc 0 T) t) (hG : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt G (H t) (Set.Icc 0 T) t) (hH : ∀ t ∈ Set.Icc 0 T, ∀ (v : E), (H t) v = -(B t) ((F t) v)) (hB : ∀ t ∈ Set.Icc 0 T, (↑(B t)).IsSymmetric) (hS : ∀ t ∈ Set.Icc 0 T, ∀ (v : E), (G t) v = (S t) ((F t) v)) (hJ : ∀ t ∈ Set.Icc 0 T, ∀ (v : E), (F t) ((J t) v) = v) (hzero : (↑(S 0)).IsSymmetric) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : (↑(S t)).IsSymmetric

An initially symmetric Eulerian velocity gradient stays symmetric. The two frame identities identify that gradient as G * F⁻¹.

Curl Matrix Symmetry

theorem EulerMeanBoundary.curlMatrix_eq_zero_iff_isSymmetric (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : curlMatrix A = 0 ↔ (↑A).IsSymmetric

The curl vanishes precisely when the real derivative matrix is symmetric.

The scalar pressure of a finite packet evolution is spatially smooth because its actual gradient is smooth. Its curvature operator is therefore symmetric, as required by the particle-map vorticity transport argument.

theorem EulerParentPacketFrames.Evolution.pressure_contDiff {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => E.pressure (↑t, x)

theorem EulerParentPacketFrames.Evolution.curvature_symmetric {A : Parent} (E : Evolution A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (↑((A.curvature.field t) x)).IsSymmetric

theorem EulerParentPacketFrames.Evolution.strain_symmetric_along_label {A : Parent} (E : Evolution A) (x : EulerSmoothLimit.Space) (hzero : (↑((A.strain.field A.zeroTime) x)).IsSymmetric) (t : ↑(Set.Icc 0 A.T)) : (↑((A.strain.field t) x)).IsSymmetric

theorem EulerParentPacketFrames.Evolution.curl_eq_zero_along_position {A : Parent} (E : Evolution A) (a : EulerSmoothLimit.Space) (hzero : EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => E.velocity (0, x)) a = 0) (t : ↑(Set.Icc 0 A.T)) : EulerMeanCutoffCurl.vectorCurl (fun (x : EulerSmoothLimit.Space) => E.velocity (↑t, x)) (A.position t a) = 0

This statement needs only the actual parent Euler evolution, with no additional Sobolev regularity or support hypotheses.

Uniform confinement of the constructed particle maps

Each selected successor retains the proved quarter-power displacement bound for its change of particle labels. Composition adds displacements without a factor involving the parent derivative. The scale construction already bounds the sum of these quarter-power costs. Thus all stages carry every fixed ball of initial labels into one fixed ball of physical positions.

This is a statement about the actual selected packet family, not an assumed bound on its velocity or velocity gradients. Vorticity confinement additionally requires its transport identity along these particle maps.

theorem EulerParentPacketFrames.Parent.child_displacement_norm_le (A : Parent) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) {M δ : ℝ} (hparent : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖(A.displacement.field t) x‖ ≤ M) (hsmall : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖(G.displacementField k m A.ell ⋯ t).field x‖ ≤ δ) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : ‖((A.child G k m hgraph nextEll hnext hnext1).displacement.field t) x‖ ≤ M + δ

theorem EulerPacketInduction.Stage.forwardNext_displacement_norm_le {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} (P : Stage S 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) {M : ℝ} (hparent : ∀ (t : ↑(Set.Icc 0 P.parent.T)) (x : EulerSmoothLimit.Space), ‖(P.parent.displacement.field t) x‖ ≤ M) (t : ↑(Set.Icc 0 (P.forwardNext hq hB).parent.T)) (x : EulerSmoothLimit.Space) : ‖((P.forwardNext hq hB).parent.displacement.field t) x‖ ≤ M + EulerPacketSourceScaleSequence.frequency S.J S.X 0 ^ (-(1 / 4))

theorem EulerPacketInduction.Stage.joinedNext_displacement_norm_le {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) {M : ℝ} (hparent : ∀ (t : ↑(Set.Icc 0 P.parent.T)) (x : EulerSmoothLimit.Space), ‖(P.parent.displacement.field t) x‖ ≤ M) (t : ↑(Set.Icc 0 (P.joinedNext hn hq hB).parent.T)) (x : EulerSmoothLimit.Space) : ‖((P.joinedNext hn hq hB).parent.displacement.field t) x‖ ≤ M + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))

theorem EulerPacketInduction.Stage.successor_displacement_norm_le {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) {M : ℝ} (hparent : ∀ (t : ↑(Set.Icc 0 P.parent.T)) (x : EulerSmoothLimit.Space), ‖(P.parent.displacement.field t) x‖ ≤ M) (t : ↑(Set.Icc 0 (P.successor hq hB).parent.T)) (x : EulerSmoothLimit.Space) : ‖((P.successor hq hB).parent.displacement.field t) x‖ ≤ M + EulerPacketSourceScaleSequence.frequency S.J S.X n ^ (-(1 / 4))

theorem EulerPacketInduction.stages_displacement_norm_le_partial_sum {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) (t : ↑(Set.Icc 0 (stages S hq hB n).parent.T)) (x : EulerSmoothLimit.Space) : ‖((stages S hq hB n).parent.displacement.field t) x‖ ≤ ‖(stages S hq hB 0).parent.displacement.field‖ + ∑ i ∈ Finset.range n, EulerPacketSourceScaleSequence.frequency S.J S.X i ^ (-(1 / 4))

noncomputable def EulerPacketInduction.particleDisplacementCap {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) : ℝ

Particle displacement cap, given by ‖(stages S hq hB 0).parent.displacement.field‖ + S.δ.

Equations

• EulerPacketInduction.particleDisplacementCap S hq hB = ‖(EulerPacketInduction.stages S hq hB 0).parent.displacement.field‖ + S.δ

theorem EulerPacketInduction.stages_displacement_norm_le {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) (t : ↑(Set.Icc 0 (stages S hq hB n).parent.T)) (x : EulerSmoothLimit.Space) : ‖((stages S hq hB n).parent.displacement.field t) x‖ ≤ particleDisplacementCap S hq hB

theorem EulerPacketInduction.stages_position_mapsTo_closedBall {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (R : ℝ) (n : ℕ) (t : ↑(Set.Icc 0 (stages S hq hB n).parent.T)) : Set.MapsTo ((stages S hq hB n).parent.position t) (Metric.closedBall 0 R) (Metric.closedBall 0 (R + particleDisplacementCap S hq hB))

theorem EulerPacketInduction.packets_position_mapsTo_closedBall (R : ℝ) (n : ℕ) (t : ↑(Set.Icc 0 (packets n).parent.T)) : Set.MapsTo ((packets n).parent.position t) (Metric.closedBall 0 R) (Metric.closedBall 0 (R + particleDisplacementCap constructionScales ⋯ ⋯))

Confinement by summable changes of particle labels

The packet construction composes particle maps as Xₙ₊₁ = Xₙ ∘ Yₙ. Bounding the displacement of this composition costs the sum of the two displacements, without a derivative bound on Xₙ. Consequently summable changes of labels confine the images of every fixed initial ball uniformly over all stages, including when the velocity gradients are unbounded.

The horizon predicate permits the time intervals to shrink with the stage. The hypotheses below are explicit: this file does not yet assert their instantiation for the packet choices made by the development.

theorem Euler.ComparatorBridge.displacement_comp_le {E : Type u_1} [NormedAddCommGroup E] (X Y : E → E) {M δ : ℝ} (hX : ∀ (x : E), ‖X x - x‖ ≤ M) (hY : ∀ (x : E), ‖Y x - x‖ ≤ δ) (x : E) : ‖X (Y x) - x‖ ≤ M + δ

theorem Euler.ComparatorBridge.support_subset_of_transport {E : Type u_1} {F : Type u_2} [Zero F] (X Y : E → E) (w₀ w : E → F) {K L : Set E} (hright : ∀ (x : E), X (Y x) = x) (hmap : Set.MapsTo X K L) (hinitial : Function.support w₀ ⊆ K) (htransport : ∀ (a : E), w₀ a = 0 → w (X a) = 0) : Function.support w ⊆ L

A transported quantity that starts supported in K remains supported in the region containing its transported labels. Only preservation of zero is needed; the transported quantity need not be constant along trajectories.

theorem Euler.ComparatorBridge.stage_displacement_le_partial_sum {E : Type u_1} [NormedAddCommGroup E] {Time : Type u_2} (H : ℕ → Time → Prop) (X Y : ℕ → Time → E → E) (M : ℝ) (δ : ℕ → ℝ) (hbase : ∀ (t : Time), H 0 t → ∀ (x : E), ‖X 0 t x - x‖ ≤ M) (hnest : ∀ (n : ℕ) (t : Time), H (n + 1) t → H n t) (hstep : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), X (n + 1) t x = X n t (Y n t x)) (hsmall : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), ‖Y n t x - x‖ ≤ δ n) (n : ℕ) (t : Time) (ht : H n t) (x : E) : ‖X n t x - x‖ ≤ M + ∑ i ∈ Finset.range n, δ i

theorem Euler.ComparatorBridge.stage_displacement_le_of_partial_sums {E : Type u_1} [NormedAddCommGroup E] {Time : Type u_2} (H : ℕ → Time → Prop) (X Y : ℕ → Time → E → E) (M : ℝ) (δ : ℕ → ℝ) (hbase : ∀ (t : Time), H 0 t → ∀ (x : E), ‖X 0 t x - x‖ ≤ M) (hnest : ∀ (n : ℕ) (t : Time), H (n + 1) t → H n t) (hstep : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), X (n + 1) t x = X n t (Y n t x)) (hsmall : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), ‖Y n t x - x‖ ≤ δ n) {C : ℝ} (hC : ∀ (n : ℕ), ∑ i ∈ Finset.range n, δ i ≤ C) (n : ℕ) (t : Time) (ht : H n t) (x : E) : ‖X n t x - x‖ ≤ M + C

theorem Euler.ComparatorBridge.stage_mapsTo_closedBall_of_partial_sums {E : Type u_1} [NormedAddCommGroup E] {Time : Type u_2} (H : ℕ → Time → Prop) (X Y : ℕ → Time → E → E) (M : ℝ) (δ : ℕ → ℝ) (hbase : ∀ (t : Time), H 0 t → ∀ (x : E), ‖X 0 t x - x‖ ≤ M) (hnest : ∀ (n : ℕ) (t : Time), H (n + 1) t → H n t) (hstep : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), X (n + 1) t x = X n t (Y n t x)) (hsmall : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), ‖Y n t x - x‖ ≤ δ n) {C : ℝ} (hC : ∀ (n : ℕ), ∑ i ∈ Finset.range n, δ i ≤ C) (R : ℝ) (n : ℕ) (t : Time) (ht : H n t) : Set.MapsTo (X n t) (Metric.closedBall 0 R) (Metric.closedBall 0 (R + M + C))

theorem Euler.ComparatorBridge.stage_displacement_le_tsum {E : Type u_1} [NormedAddCommGroup E] {Time : Type u_2} (H : ℕ → Time → Prop) (X Y : ℕ → Time → E → E) (M : ℝ) (δ : ℕ → ℝ) (hbase : ∀ (t : Time), H 0 t → ∀ (x : E), ‖X 0 t x - x‖ ≤ M) (hnest : ∀ (n : ℕ) (t : Time), H (n + 1) t → H n t) (hstep : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), X (n + 1) t x = X n t (Y n t x)) (hsmall : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), ‖Y n t x - x‖ ≤ δ n) (hδ : Summable δ) (hδ0 : ∀ (n : ℕ), 0 ≤ δ n) (n : ℕ) (t : Time) (ht : H n t) (x : E) : ‖X n t x - x‖ ≤ M + ∑' (i : ℕ), δ i

theorem Euler.ComparatorBridge.stage_mapsTo_closedBall {E : Type u_1} [NormedAddCommGroup E] {Time : Type u_2} (H : ℕ → Time → Prop) (X Y : ℕ → Time → E → E) (M : ℝ) (δ : ℕ → ℝ) (hbase : ∀ (t : Time), H 0 t → ∀ (x : E), ‖X 0 t x - x‖ ≤ M) (hnest : ∀ (n : ℕ) (t : Time), H (n + 1) t → H n t) (hstep : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), X (n + 1) t x = X n t (Y n t x)) (hsmall : ∀ (n : ℕ) (t : Time), H (n + 1) t → ∀ (x : E), ‖Y n t x - x‖ ≤ δ n) (hδ : Summable δ) (hδ0 : ∀ (n : ℕ), 0 ≤ δ n) (R : ℝ) (n : ℕ) (t : Time) (ht : H n t) : Set.MapsTo (X n t) (Metric.closedBall 0 R) (Metric.closedBall 0 (R + M + ∑' (i : ℕ), δ i))

Common initial support of every constructed packet stage

The selected forward and joined corrections retain the common initial support. Therefore every finite stage has initial velocity, all its spatial derivatives, and initial vorticity supported in the closed ball of radius two.

The curl of a differentiable field has support inside the support of that field. This elementary locality fact does not assume spatial norm bounds.

theorem EulerMeanCutoffCurl.tsupport_vectorCurl_subset (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : Differentiable ℝ f) : tsupport (vectorCurl f) ⊆ tsupport f

theorem EulerPacketInduction.Stage.joinedNext_initial_support {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hP : (tsupport fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2) : (tsupport fun (x : EulerSmoothLimit.Space) => (P.joinedNext hn hq hB).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.Stage.successor_initial_support {q : ℕ} {B : ℝ} {S : EulerPacketInductionScales.Scales (↑q) B} {n : ℕ} (P : Stage S n) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (hP : (tsupport fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2) : (tsupport fun (x : EulerSmoothLimit.Space) => (P.successor hq hB).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.stages_initial_support {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) : (tsupport fun (x : EulerSmoothLimit.Space) => (stages S hq hB n).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.stages_initial_derivatives_support {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n m : ℕ) : tsupport (iteratedFDeriv ℝ m fun (x : EulerSmoothLimit.Space) => (stages S hq hB n).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.stages_initial_curl_support {q : ℕ} {B : ℝ} (S : EulerPacketInductionScales.Scales (↑q) B) (hq : EulerParentNeighborThreshold.requiredExponent ≤ q) (hB : EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant ≤ B) (n : ℕ) : tsupport (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => (stages S hq hB n).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.packets_initial_support (n : ℕ) : (tsupport fun (x : EulerSmoothLimit.Space) => (packets n).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

theorem EulerPacketInduction.packets_initial_curl_support (n : ℕ) : tsupport (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => (packets n).state.evolution.velocity (0, x)) ⊆ Metric.closedBall 0 2

Every packet horizon covers the canonical lifespan

The horizons of the actual recursive family decrease. If its limiting datum had an evolution through any one of those horizons, comparison with the tail of the packet family would bound the divergent activation gradients. This applies the proved varying-horizon H³ stability theorem.

theorem EulerPacketInduction.packets_horizon_succ (n : ℕ) : (packets (n + 1)).parent.T = (packets n).nextHorizon

theorem EulerPacketInduction.packets_horizon_antitone : Antitone fun (n : ℕ) => (packets n).parent.T

theorem EulerPacketInduction.initialDatum_no_packet_horizon (N : ℕ) : ¬EulerOrdinarySobolev.HasEulerEvolution initialDatum (packets N).parent.T

theorem EulerPacketInduction.lifespan_le_packet_horizon (n : ℕ) : lifespan.duration ≤ (packets n).parent.T

Convergence of ordinary Euler velocities in the initial H³ norm gives pointwise convergence of their curls at every time in their common interval.

theorem EulerOrdinarySobolev.Evolution.sampled_h3_tendsto_of_initial_h3 {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (V : ℕ → Evolution T hT) (hinit : Filter.Tendsto (fun (n : ℕ) => tensorNorm 3 (U.difference (V n) ⟨0, ⋯⟩)) Filter.atTop (nhds 0)) (times : ℕ → ↑(Set.Icc 0 T)) : Filter.Tendsto (fun (n : ℕ) => tensorNorm 3 (U.difference (V n) (times n))) Filter.atTop (nhds 0)

theorem EulerOrdinarySobolev.Evolution.curl_tendsto_of_initial_h3 {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (V : ℕ → Evolution T hT) (hinit : Filter.Tendsto (fun (n : ℕ) => tensorNorm 3 (U.difference (V n) ⟨0, ⋯⟩)) Filter.atTop (nhds 0)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (n : ℕ) => EulerMeanCutoffCurl.vectorCurl ((V n).velocity t).field x) Filter.atTop (nhds (EulerMeanCutoffCurl.vectorCurl (U.velocity t).field x))

Every selected finite packet has vorticity supported in one fixed ball throughout its horizon. Initial support, the actual vorticity transport law, and the summable particle-map displacement bound supply the three ingredients.

theorem EulerPacketInduction.packets_vorticity_support (n : ℕ) (t : ↑(Set.Icc 0 (packets n).parent.T)) : tsupport (EulerMeanCutoffCurl.vectorCurl fun (x : EulerSmoothLimit.Space) => (packets n).state.evolution.velocity (↑t, x)) ⊆ Metric.closedBall 0 (2 + particleDisplacementCap constructionScales ⋯ ⋯)

def EulerPacketInduction.canonicalVorticityBall : Set EulerSmoothLimit.Space

Canonical vorticity ball, given by Metric.closedBall 0 (2 + particleDisplacementCap constructionScales le_rfl le_rfl).

Equations

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

theorem EulerPacketInduction.canonicalVorticityBall_compact : IsCompact canonicalVorticityBall

theorem EulerPacketInduction.evolution_vorticity_support (S : ℝ) (hS : 0 < S) (hSL : S < lifespan.duration) (t : ↑(Set.Icc 0 S)) : tsupport (EulerMeanCutoffCurl.vectorCurl ((lifespan.evolution S hS hSL).velocity t).field) ⊆ canonicalVorticityBall

theorem EulerPacketInduction.canonical_vorticity_support (t : lifespan.Time) : tsupport (EulerMeanCutoffCurl.vectorCurl (lifespan.maximalVelocity t)) ⊆ canonicalVorticityBall

theorem EulerPacketInduction.canonical_vorticity_eq_zero_outside (t : lifespan.Time) (x : EulerSmoothLimit.Space) (hx : x ∉ canonicalVorticityBall) : EulerMeanCutoffCurl.vectorCurl (lifespan.maximalVelocity t) x = 0

theorem EulerPacketInduction.canonical_vorticity_hasCompactSupport (t : lifespan.Time) : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl (lifespan.maximalVelocity t))