The actual three fields in the chain rule for X(t,Y(t,a)) have Gevrey L² bounds. The parent is controlled by its physical-label H⁶ norm, and Y preserves volume. The new radius is linear in the inner radius, with only polynomial dependence on the parent and amplitudes.

The classical label Sobolev norm also bounds the actual L² tensor jets, so a parent satisfying (21) supplies every outer L² input needed by the volume-preserving composition estimate.

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp_le_wordSum (A : SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : ‖A.jetLp n‖ ≤ EulerParameterWordGevrey.wordSum EulerPacketParentLabelBounds.direction (fun (a : EulerSmoothLimit.Space) => (translation a) A.toLp) n 0

theorem EulerLpTranslation.SmoothL2Field.norm_jetLp_le_classicalBlock (A : SmoothL2Field EulerSmoothLimit.Space) (q n : ℕ) : ‖A.jetLp n‖ ≤ EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q A.toLp ⋯ n

theorem EulerLpTranslation.SmoothL2Field.hasJetBound_of_labelBound (A : SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (h : EulerPacketParentLabelBounds.HasLabelBound K A) : A.HasJetBound K K

theorem EulerLpTranslation.SmoothL2Field.sup_bound_of_labelBound (A : SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (h : EulerPacketParentLabelBounds.HasLabelBound K A) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n A.field x‖ ≤ EulerPacketParentLabelBounds.embeddingCost * K * K ^ n * ↑n.factorial ^ 2

structure EulerChildParticleFieldBounds.Data : Type

Data, collecting parentDisplacement, parentVelocity, parentAcceleration, K, K_one, parentDisplacement_bound and their compatibility conditions.

• parentDisplacement : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Parent displacement of Data, of type SmoothL2Field Space.

• parentVelocity : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Parent velocity of Data, of type SmoothL2Field Space.

• parentAcceleration : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Parent acceleration of Data, of type SmoothL2Field Space.

• K : ℝ

  K of Data, of type ℝ.

• K_one : 1 ≤ self.K
• parentDisplacement_bound : EulerPacketParentLabelBounds.HasLabelBound self.K self.parentDisplacement
• parentVelocity_bound : EulerPacketParentLabelBounds.HasLabelBound self.K self.parentVelocity
• parentAcceleration_bound : EulerPacketParentLabelBounds.HasLabelBound self.K self.parentAcceleration
• displacement : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Displacement of Data, of type SmoothL2Field Space.

• velocity : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Velocity field of Data, of type SmoothL2Field Space.

• acceleration : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Acceleration of Data, of type SmoothL2Field Space.

• amp : ℝ

  Amp of Data, of type ℝ.

• rad : ℝ

  Rad of Data, of type ℝ.

• amp_one : 1 ≤ self.amp
• rad_one : 1 ≤ self.rad
• displacement_bound : self.displacement.HasJetBound self.amp self.rad
• velocity_bound : self.velocity.HasJetBound self.amp self.rad
• acceleration_bound : self.acceleration.HasJetBound self.amp self.rad
• displacement_sup : EulerGevrey.HasSupBound self.displacement.field self.amp self.rad
• velocity_sup : EulerGevrey.HasSupBound self.velocity.field self.amp self.rad
• volume_preserving : MeasureTheory.MeasurePreserving (fun (x : EulerSmoothLimit.Space) => x + self.displacement.field x) MeasureTheory.volume MeasureTheory.volume

def EulerChildParticleFieldBounds.Data.inner (G : Data) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Inner, given by x+G.displacement.field x.

Equations

• G.inner x = x + G.displacement.field x

def EulerChildParticleFieldBounds.Data.compositionRadius (G : Data) (s : ℝ) : ℝ

Composition radius, given by (1+G.rad)*((1+G.amp)*s+2).

Equations

• G.compositionRadius s = (1 + G.rad) * ((1 + G.amp) * s + 2)

def EulerChildParticleFieldBounds.Data.radius (G : Data) : ℝ

Radius, given by G.compositionRadius (16*G.K)+G.rad.

Equations

• G.radius = G.compositionRadius (16 * G.K) + G.rad

noncomputable def EulerChildParticleFieldBounds.Data.firstAmplitude (G : Data) : ℝ

First amplitude, given by (embeddingCost*G.K)*G.K.

Equations

• G.firstAmplitude = EulerPacketParentLabelBounds.embeddingCost * G.K * G.K

noncomputable def EulerChildParticleFieldBounds.Data.secondAmplitude (G : Data) : ℝ

Second amplitude, given by G.firstAmplitude*(4*G.K).

Equations

• G.secondAmplitude = G.firstAmplitude * (4 * G.K)

noncomputable def EulerChildParticleFieldBounds.Data.amplitude (G : Data) : ℝ

Amplitude, given by G.K+G.amp+9*G.firstAmplitude*G.amp+9*G.secondAmplitude*G.amp^2.

Equations

• G.amplitude = G.K + G.amp + 9 * G.firstAmplitude * G.amp + 9 * G.secondAmplitude * G.amp ^ 2

theorem EulerChildParticleFieldBounds.Data.K_nonneg (G : Data) : 0 ≤ G.K

theorem EulerChildParticleFieldBounds.Data.amp_nonneg (G : Data) : 0 ≤ G.amp

theorem EulerChildParticleFieldBounds.Data.rad_nonneg (G : Data) : 0 ≤ G.rad

theorem EulerChildParticleFieldBounds.Data.compositionRadius_nonneg (G : Data) (s : ℝ) (hs : 0 ≤ s) : 0 ≤ G.compositionRadius s

theorem EulerChildParticleFieldBounds.Data.radius_nonneg (G : Data) : 0 ≤ G.radius

theorem EulerChildParticleFieldBounds.Data.rad_le_radius (G : Data) : G.rad ≤ G.radius

theorem EulerChildParticleFieldBounds.Data.firstAmplitude_nonneg (G : Data) : 0 ≤ G.firstAmplitude

theorem EulerChildParticleFieldBounds.Data.secondAmplitude_nonneg (G : Data) : 0 ≤ G.secondAmplitude

theorem EulerChildParticleFieldBounds.Data.amplitude_nonneg (G : Data) : 0 ≤ G.amplitude

theorem EulerChildParticleFieldBounds.Data.compositionRadius_le_radius (G : Data) (s : ℝ) (hs : s ≤ 16 * G.K) : G.compositionRadius s ≤ G.radius

theorem EulerChildParticleFieldBounds.Data.inner_smooth (G : Data) : ContDiff ℝ (↑⊤) G.inner

theorem EulerChildParticleFieldBounds.Data.inner_positive (G : Data) (n : ℕ) (hn : 0 < n) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n G.inner x‖ ≤ (1 + G.amp) * (1 + G.rad) ^ n * ↑n.factorial ^ 2

noncomputable def EulerChildParticleFieldBounds.Data.parentComposed (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : EulerPacketParentLabelBounds.HasLabelBound G.K U) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Parent composed, constructed using composeField.

Equations

• G.parentComposed U hU = EulerLpTranslation.SmoothL2Field.composeField G.inner ⋯ ⋯ (1 + G.amp) (1 + G.rad) ⋯ ⋯ ⋯ U G.K G.K ⋯ ⋯ ⋯

theorem EulerChildParticleFieldBounds.Data.parentComposed_bound (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : EulerPacketParentLabelBounds.HasLabelBound G.K U) : (G.parentComposed U hU).HasJetBound G.K G.radius

noncomputable def EulerChildParticleFieldBounds.Data.firstCoefficient (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

First coefficient, given by fderiv ℝ U.field (G.inner x).

Equations

• G.firstCoefficient U x = fderiv ℝ U.field (G.inner x)

noncomputable def EulerChildParticleFieldBounds.Data.secondCoefficient (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Second coefficient, given by fderiv ℝ (fderiv ℝ U.field) (G.inner x).

Equations

• G.secondCoefficient U x = fderiv ℝ (fderiv ℝ U.field) (G.inner x)

theorem EulerChildParticleFieldBounds.Data.firstCoefficient_smooth (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (G.firstCoefficient U)

theorem EulerChildParticleFieldBounds.Data.secondCoefficient_smooth (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (G.secondCoefficient U)

theorem EulerChildParticleFieldBounds.Data.firstCoefficient_bound (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : EulerPacketParentLabelBounds.HasLabelBound G.K U) : EulerGevrey.HasSupBound (G.firstCoefficient U) G.firstAmplitude G.radius

theorem EulerChildParticleFieldBounds.Data.secondCoefficient_bound (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : EulerPacketParentLabelBounds.HasLabelBound G.K U) : EulerGevrey.HasSupBound (G.secondCoefficient U) G.secondAmplitude G.radius

theorem EulerChildParticleFieldBounds.Data.velocity_bound_radius (G : Data) : G.velocity.HasJetBound G.amp G.radius

theorem EulerChildParticleFieldBounds.Data.acceleration_bound_radius (G : Data) : G.acceleration.HasJetBound G.amp G.radius

theorem EulerChildParticleFieldBounds.Data.displacement_bound_radius (G : Data) : G.displacement.HasJetBound G.amp G.radius

theorem EulerChildParticleFieldBounds.Data.velocity_sup_radius (G : Data) : EulerGevrey.HasSupBound G.velocity.field G.amp G.radius

noncomputable def EulerChildParticleFieldBounds.Data.firstTerm (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : EulerPacketParentLabelBounds.HasLabelBound G.K U) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

First term, constructed using productField.

Equations

• G.firstTerm U hU = EulerLpTranslation.SmoothL2Field.productField (G.firstCoefficient U) ⋯ G.velocity G.firstAmplitude G.amp G.radius ⋯ ⋯ ⋯ ⋯ ⋯

theorem EulerChildParticleFieldBounds.Data.firstTerm_bound (G : Data) (U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : EulerPacketParentLabelBounds.HasLabelBound G.K U) : (G.firstTerm U hU).HasJetBound (3 * G.firstAmplitude * G.amp) G.radius

noncomputable def EulerChildParticleFieldBounds.Data.quadraticCoefficient (G : Data) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Quadratic coefficient, given by G.secondCoefficient G.parentDisplacement x (G.velocity.field x).

Equations

• G.quadraticCoefficient x = (G.secondCoefficient G.parentDisplacement x) (G.velocity.field x)

theorem EulerChildParticleFieldBounds.Data.quadraticCoefficient_smooth (G : Data) : ContDiff ℝ (↑⊤) G.quadraticCoefficient

theorem EulerChildParticleFieldBounds.Data.quadraticCoefficient_bound (G : Data) : EulerGevrey.HasSupBound G.quadraticCoefficient (3 * G.secondAmplitude * G.amp) G.radius

noncomputable def EulerChildParticleFieldBounds.Data.quadraticTerm (G : Data) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Quadratic term, constructed using productField.

Equations

• G.quadraticTerm = EulerLpTranslation.SmoothL2Field.productField G.quadraticCoefficient ⋯ G.velocity (3 * G.secondAmplitude * G.amp) G.amp G.radius ⋯ ⋯ ⋯ ⋯ ⋯

theorem EulerChildParticleFieldBounds.Data.quadraticTerm_bound (G : Data) : G.quadraticTerm.HasJetBound (9 * G.secondAmplitude * G.amp ^ 2) G.radius

noncomputable def EulerChildParticleFieldBounds.Data.accelerationTerm (G : Data) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Acceleration term, constructed using productField.

Equations

• G.accelerationTerm = EulerLpTranslation.SmoothL2Field.productField (G.firstCoefficient G.parentDisplacement) ⋯ G.acceleration G.firstAmplitude G.amp G.radius ⋯ ⋯ ⋯ ⋯ ⋯

theorem EulerChildParticleFieldBounds.Data.accelerationTerm_bound (G : Data) : G.accelerationTerm.HasJetBound (3 * G.firstAmplitude * G.amp) G.radius

noncomputable def EulerChildParticleFieldBounds.Data.childDisplacement (G : Data) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Child displacement, given by addField (G.parentComposed G.parentDisplacement G.parentDisplacement_bound) G.displacement.

Equations

• G.childDisplacement = (G.parentComposed G.parentDisplacement ⋯).addField G.displacement

noncomputable def EulerChildParticleFieldBounds.Data.childVelocity (G : Data) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Child velocity, constructed using addField.

Equations

• G.childVelocity = ((G.parentComposed G.parentVelocity ⋯).addField G.velocity).addField (G.firstTerm G.parentDisplacement ⋯)

noncomputable def EulerChildParticleFieldBounds.Data.childAcceleration (G : Data) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Child acceleration, constructed using addField.

Equations

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

theorem EulerChildParticleFieldBounds.Data.childDisplacement_bound (G : Data) : G.childDisplacement.HasJetBound G.amplitude G.radius

theorem EulerChildParticleFieldBounds.Data.childVelocity_bound (G : Data) : G.childVelocity.HasJetBound G.amplitude G.radius

theorem EulerChildParticleFieldBounds.Data.childAcceleration_bound (G : Data) : G.childAcceleration.HasJetBound G.amplitude G.radius

theorem EulerChildParticleFieldBounds.Data.childDisplacement_apply (G : Data) (x : EulerSmoothLimit.Space) : G.childDisplacement.field x = G.parentDisplacement.field (G.inner x) + G.displacement.field x

theorem EulerChildParticleFieldBounds.Data.childVelocity_apply (G : Data) (x : EulerSmoothLimit.Space) : G.childVelocity.field x = G.parentVelocity.field (G.inner x) + G.velocity.field x + (fderiv ℝ G.parentDisplacement.field (G.inner x)) (G.velocity.field x)

theorem EulerChildParticleFieldBounds.Data.childAcceleration_apply (G : Data) (x : EulerSmoothLimit.Space) : G.childAcceleration.field x = G.parentAcceleration.field (G.inner x) + (fderiv ℝ G.parentVelocity.field (G.inner x)) (G.velocity.field x) + (fderiv ℝ G.parentVelocity.field (G.inner x)) (G.velocity.field x) + ((fderiv ℝ (fderiv ℝ G.parentDisplacement.field) (G.inner x)) (G.velocity.field x)) (G.velocity.field x) + G.acceleration.field x + (fderiv ℝ G.parentDisplacement.field (G.inner x)) (G.acceleration.field x)

theorem EulerChildParticleFieldBounds.Data.child_label_bounds (G : Data) (K : ℝ) (ha : EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) 6 G.radius G.amplitude ≤ K) (hr : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) G.radius ≤ K) : EulerPacketParentLabelBounds.HasLabelBound K G.childDisplacement ∧ EulerPacketParentLabelBounds.HasLabelBound K G.childVelocity ∧ EulerPacketParentLabelBounds.HasLabelBound K G.childAcceleration