Growth of the activation gradient

The frame decomposes the strain at the origin into a rank-one shear, a background and a remainder. The shear dominates the other terms and diverges with the stage index. The argument only needs GrowthData; the Stage results retain the full-stage interface.

theorem EulerPacketInductionScales.activationMargin_le_half : activationMargin ≤ 1 / 2

theorem EulerPacketInductionScales.Scales.previousShear_ge_index {c B : ℝ} (S : Scales c B) (n : ℕ) : ↑n + 1 ≤ EulerPacketSourceScaleSequence.previousShear S.J S.X n

noncomputable def EulerPacketInduction.GrowthData.activationGradient {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : GrowthData S n) : ℝ

The norm of the spatial velocity gradient at the packet centre and activation time.

Equations

• P.activationGradient = ‖fderiv ℝ (fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (P.time, x)) 0‖

theorem EulerPacketInduction.GrowthData.gradient_lower {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : GrowthData S n) (hn : n ≠ 0) : EulerPacketSourceScaleSequence.previousShear S.J S.X n / 2 ≤ P.activationGradient

The leading shear gives a gradient lower bound after subtracting the background and remainder controlled by the frame estimates.

theorem EulerPacketInduction.GrowthData.gradient_atTop {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} (P : (n : ℕ) → GrowthData S n) : Filter.Tendsto (fun (n : ℕ) => (P n).activationGradient) Filter.atTop Filter.atTop

Activation gradients diverge along any family of growth data.

noncomputable def EulerPacketInduction.Stage.activationGradient {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : ℝ

The norm of the spatial velocity gradient at the stage's activation point.

Equations

• P.activationGradient = ‖fderiv ℝ (fun (x : EulerSmoothLimit.Space) => P.state.evolution.velocity (P.time, x)) 0‖

theorem EulerPacketInduction.Stage.gradient_lower {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (hn : n ≠ 0) : EulerPacketSourceScaleSequence.previousShear S.J S.X n / 2 ≤ P.activationGradient

A full stage satisfies the growth estimate through its growth data.

theorem EulerPacketInduction.Stage.gradient_atTop {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} (P : (n : ℕ) → Stage S n) : Filter.Tendsto (fun (n : ℕ) => (P n).activationGradient) Filter.atTop Filter.atTop

The activation gradients of a family of full stages diverge.