Related estimates used together by the same construction modules.

Source (21) for the actual physical graph change of labels. The arbitrary small frequency losses are absorbed before the child estimate, and the resulting exponent is exactly 10(s+2).

Applying the child composition estimate to the actual physical graph flow. The input fields are the concrete displacement, velocity and acceleration constructed from the periodic corrected packet.

theorem EulerPhysicalChildFields.inner_eq_forward {P T : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) : (fun (x : EulerSmoothLimit.Space) => x + (G.displacementField k m ell hell t).field x) = (EulerSmoothBanachFlow.flowData T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell)).forward ↑t

noncomputable def EulerPhysicalChildFields.data {P T : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (D V W : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : 1 ≤ K) (hD : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (D t)) (hV : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hW : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (W t)) (M R : ℝ) (hM : 1 ≤ M) (hR : 1 ≤ R) (hd : ∀ (t : ↑(Set.Icc 0 T)), (G.displacementField k m ell hell t).HasJetBound M R) (hv : ∀ (t : ↑(Set.Icc 0 T)), (G.velocityField k m ell hell t).HasJetBound M R) (hw : ∀ (t : ↑(Set.Icc 0 T)), (G.accelerationFieldL2 k m ell hell t).HasJetBound M R) (hds : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field M R) (hvs : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field M R) (t : ↑(Set.Icc 0 T)) : EulerChildParticleFieldBounds.Data

Data, bundling parentDisplacement, parentVelocity, parentAcceleration, K and the required compatibility proofs.

Equations

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

theorem EulerPhysicalChildFields.data_inner {P T : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (D V W : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : 1 ≤ K) (hD : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (D t)) (hV : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hW : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (W t)) (M R : ℝ) (hM : 1 ≤ M) (hR : 1 ≤ R) (hd : ∀ (t : ↑(Set.Icc 0 T)), (G.displacementField k m ell hell t).HasJetBound M R) (hv : ∀ (t : ↑(Set.Icc 0 T)), (G.velocityField k m ell hell t).HasJetBound M R) (hw : ∀ (t : ↑(Set.Icc 0 T)), (G.accelerationFieldL2 k m ell hell t).HasJetBound M R) (hds : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field M R) (hvs : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field M R) (t : ↑(Set.Icc 0 T)) : (data G k m hgraph ell hell D V W K hK hD hV hW M R hM hR hd hv hw hds hvs t).inner = (EulerSmoothBanachFlow.flowData T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell)).forward ↑t

noncomputable def EulerPhysicalChildFields.childAmplitude (K M : ℝ) : ℝ

Child amplitude, given by K+M+9*((embeddingCost*K)*K)*M+9*(((embeddingCost*K)*K)*(4*K))*M^2.

Equations

• EulerPhysicalChildFields.childAmplitude K M = K + M + 9 * (EulerPacketParentLabelBounds.embeddingCost * K * K) * M + 9 * (EulerPacketParentLabelBounds.embeddingCost * K * K * (4 * K)) * M ^ 2

def EulerPhysicalChildFields.childRadius (K M R : ℝ) : ℝ

Child radius, given by (1+R)*((1+M)*(16*K)+2)+R.

Equations

• EulerPhysicalChildFields.childRadius K M R = (1 + R) * ((1 + M) * (16 * K) + 2) + R

theorem EulerPhysicalChildFields.fields_jet_bound {P T : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (D V W : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : 1 ≤ K) (hD : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (D t)) (hV : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hW : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (W t)) (M R : ℝ) (hM : 1 ≤ M) (hR : 1 ≤ R) (hd : ∀ (t : ↑(Set.Icc 0 T)), (G.displacementField k m ell hell t).HasJetBound M R) (hv : ∀ (t : ↑(Set.Icc 0 T)), (G.velocityField k m ell hell t).HasJetBound M R) (hw : ∀ (t : ↑(Set.Icc 0 T)), (G.accelerationFieldL2 k m ell hell t).HasJetBound M R) (hds : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field M R) (hvs : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field M R) (t : ↑(Set.Icc 0 T)) : have E := data G k m hgraph ell hell D V W K hK hD hV hW M R hM hR hd hv hw hds hvs t; E.childDisplacement.HasJetBound (childAmplitude K M) (childRadius K M R) ∧ E.childVelocity.HasJetBound (childAmplitude K M) (childRadius K M R) ∧ E.childAcceleration.HasJetBound (childAmplitude K M) (childRadius K M R)

theorem EulerPhysicalChildFields.fields_label_bound {P T : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (D V W : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : 1 ≤ K) (hD : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (D t)) (hV : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hW : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (W t)) (M R : ℝ) (hM : 1 ≤ M) (hR : 1 ≤ R) (hd : ∀ (t : ↑(Set.Icc 0 T)), (G.displacementField k m ell hell t).HasJetBound M R) (hv : ∀ (t : ↑(Set.Icc 0 T)), (G.velocityField k m ell hell t).HasJetBound M R) (hw : ∀ (t : ↑(Set.Icc 0 T)), (G.accelerationFieldL2 k m ell hell t).HasJetBound M R) (hds : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field M R) (hvs : ∀ (t : ↑(Set.Icc 0 T)), EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field M R) (J : ℝ) (ha : EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 3) 6 (childRadius K M R) (childAmplitude K M) ≤ J) (hr : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 3) (childRadius K M R) ≤ J) (t : ↑(Set.Icc 0 T)) : have E := data G k m hgraph ell hell D V W K hK hD hV hW M R hM hR hd hv hw hds hvs t; EulerPacketParentLabelBounds.HasLabelBound J E.childDisplacement ∧ EulerPacketParentLabelBounds.HasLabelBound J E.childVelocity ∧ EulerPacketParentLabelBounds.HasLabelBound J E.childAcceleration

The explicit polynomial losses of child composition fit the manuscript's C*=10(s+2). This includes the sum of the three actual physical-label Hs word norms, not just a separate bound for each field.

theorem EulerChildParticleFieldBounds.Data.amplitude_le_power (G : Data) (k : ℝ) (hk1 : 1 ≤ k) (hbig : 2 + 45 * EulerPacketParentLabelBounds.embeddingCost ≤ k) (hK : G.K ≤ k) (hM : G.amp ≤ k) : G.amplitude ≤ k ^ 6

theorem EulerChildParticleFieldBounds.Data.radius_le_power (G : Data) (k : ℝ) (hk : 69 ≤ k) (hK : G.K ≤ k) (hM : G.amp ≤ k) (hR : G.rad ≤ k ^ 2) : G.radius ≤ k ^ 5

theorem EulerChildParticleFieldBounds.Data.source_physical_label_bound (G : Data) (q : ℕ) (k : ℝ) (hk : 69 ≤ k) (hbig : 2 + 45 * EulerPacketParentLabelBounds.embeddingCost ≤ k) (hcost : EulerSobolevSourceExponent.fixedCost q ≤ k) (hK : G.K ≤ k) (hM : G.amp ≤ k) (hR : G.rad ≤ k ^ 2) (n : ℕ) : EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q G.childDisplacement.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q G.childVelocity.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q G.childAcceleration.toLp ⋯ n ≤ (k ^ (10 * (q + 2))) ^ (n + 1) * ↑n.factorial ^ 2

theorem EulerPhysicalChildFields.coarsen_graph_bounds (k ell : ℝ) (hk : 1 ≤ k) (hell : 0 < ell) (hi : ell⁻¹ ≤ k ^ (3 / 4)) (A B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (ha : A.HasJetBound (k ^ (-(1 / 2) + 1 / 4)) (ell⁻¹ * k ^ (1 + 1 / 4))) (hb : B.HasJetBound (k ^ (-(1 / 2) + 1 / 4)) (ell⁻¹ * k ^ (1 + 1 / 4))) (hc : C.HasJetBound (k ^ (1 / 4)) (ell⁻¹ * k ^ (1 + 1 / 4))) (has : EulerGevrey.HasSupBound A.field (k ^ (-(1 / 2) + 1 / 4)) (ell⁻¹ * k ^ (1 + 1 / 4))) (hbs : EulerGevrey.HasSupBound B.field (k ^ (-(1 / 2) + 1 / 4)) (ell⁻¹ * k ^ (1 + 1 / 4))) : A.HasJetBound k (k ^ 2) ∧ B.HasJetBound k (k ^ 2) ∧ C.HasJetBound k (k ^ 2) ∧ EulerGevrey.HasSupBound A.field k (k ^ 2) ∧ EulerGevrey.HasSupBound B.field k (k ^ 2)

theorem EulerPhysicalChildFields.exists_source_child_fields {P T : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (D V W : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : 1 ≤ K) (hD : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (D t)) (hV : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hW : ∀ (t : ↑(Set.Icc 0 T)), EulerPacketParentLabelBounds.HasLabelBound K (W t)) (q : ℕ) (hk : 69 ≤ k) (hKk : K ≤ k) (hbig : 2 + 45 * EulerPacketParentLabelBounds.embeddingCost ≤ k) (hcost : EulerSobolevSourceExponent.fixedCost q ≤ k) (hb : ∀ (t : ↑(Set.Icc 0 T)), (G.displacementField k m ell hell t).HasJetBound k (k ^ 2) ∧ (G.velocityField k m ell hell t).HasJetBound k (k ^ 2) ∧ (G.accelerationFieldL2 k m ell hell t).HasJetBound k (k ^ 2) ∧ EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field k (k ^ 2) ∧ EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field k (k ^ 2)) : ∃ (E : ↑(Set.Icc 0 T) → EulerChildParticleFieldBounds.Data), (∀ (t : ↑(Set.Icc 0 T)), (E t).parentDisplacement = D t ∧ (E t).parentVelocity = V t ∧ (E t).parentAcceleration = W t ∧ (E t).displacement = G.displacementField k m ell hell t ∧ (E t).velocity = G.velocityField k m ell hell t ∧ (E t).acceleration = G.accelerationFieldL2 k m ell hell t ∧ (E t).inner = (EulerSmoothBanachFlow.flowData T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell)).forward ↑t) ∧ ∀ (t : ↑(Set.Icc 0 T)) (n : ℕ), EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (E t).childDisplacement.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (E t).childVelocity.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q (E t).childAcceleration.toLp ⋯ n ≤ (k ^ (10 * (q + 2))) ^ (n + 1) * ↑n.factorial ^ 2

The quarter-power physical-flow bounds follow from the same tiny-power source comparison and one parent-independent numerical margin.

Frequency arithmetic for the genuine graph-flow estimates. Fixed source constants affect only the frequency threshold. The power losses can be made arbitrarily small, independently of any truncation order.

noncomputable def EulerPacketGraphFlowFrequency.inputExponent (ε : ℝ) : ℝ

Input exponent, given by min (ε/6) (1/4).

Equations

• EulerPacketGraphFlowFrequency.inputExponent ε = min (ε / 6) (1 / 4)

theorem EulerPacketGraphFlowFrequency.inputExponent_pos (ε : ℝ) (hε : 0 < ε) : 0 < inputExponent ε

theorem EulerPacketGraphFlowFrequency.inputExponent_le_quarter (ε : ℝ) : inputExponent ε ≤ 1 / 4

theorem EulerPacketGraphFlowFrequency.six_inputExponent_le (ε : ℝ) : 6 * inputExponent ε ≤ ε

theorem EulerPacketGraphFlowFrequency.physical_bounds_of_power (ε η K k B R T C1 ell : ℝ) (hη : 0 < η) (_hηq : η ≤ 1 / 4) (hηε : 6 * η ≤ ε) (hK : 0 ≤ K) (hB : 0 ≤ B) (hR : 0 ≤ R) (hT : 0 ≤ T) (hC1 : 0 ≤ C1) (hk : 1 ≤ k) (hell : 0 < ell) (hw : 71 ≤ k ^ η) (hKw : K ≤ k ^ η) (hRw : R ≤ k ^ η) (hTw : T ≤ k ^ η) (hCw : C1 ≤ k ^ η) (hroot : 2 ≤ k ^ (1 / 2 - η)) (hsmall : B ≤ 2 * k ^ (-(1 / 2))) : K * (T * B) * (1 + EulerSmoothFlowGevrey.flowRadius B R T R) ≤ k ^ (-(1 / 2) + ε) ∧ K * B * (1 + EulerSmoothFlowGevrey.flowRadius B R T R) ≤ k ^ (-(1 / 2) + ε) ∧ K * (C1 + 3 * B ^ 2 * R) * (1 + EulerSmoothFlowGevrey.flowRadius B R T (6 * R)) ≤ k ^ ε ∧ ell⁻¹ * (4 * EulerSmoothFlowGevrey.flowRadius B R T R * (1 + k)) ≤ ell⁻¹ * k ^ (1 + ε) ∧ ell⁻¹ * (4 * EulerSmoothFlowGevrey.flowRadius B R T (6 * R) * (1 + k)) ≤ ell⁻¹ * k ^ (1 + ε)

theorem EulerPacketGraphFlowFrequency.physical_bounds_eventually (ε K : ℝ) (hε : 0 < ε) (hK : 0 ≤ K) : ∀ᶠ (k : ℝ) in Filter.atTop, ∀ (B R T C1 ell : ℝ), 0 ≤ B → 0 ≤ R → 0 ≤ T → 0 ≤ C1 → 0 < ell → R ≤ k ^ inputExponent ε → T ≤ k ^ inputExponent ε → C1 ≤ k ^ inputExponent ε → B ≤ 2 * k ^ (-(1 / 2)) → K * (T * B) * (1 + EulerSmoothFlowGevrey.flowRadius B R T R) ≤ k ^ (-(1 / 2) + ε) ∧ K * B * (1 + EulerSmoothFlowGevrey.flowRadius B R T R) ≤ k ^ (-(1 / 2) + ε) ∧ K * (C1 + 3 * B ^ 2 * R) * (1 + EulerSmoothFlowGevrey.flowRadius B R T (6 * R)) ≤ k ^ ε ∧ ell⁻¹ * (4 * EulerSmoothFlowGevrey.flowRadius B R T R * (1 + k)) ≤ ell⁻¹ * k ^ (1 + ε) ∧ ell⁻¹ * (4 * EulerSmoothFlowGevrey.flowRadius B R T (6 * R) * (1 + k)) ≤ ell⁻¹ * k ^ (1 + ε)

Uniform bounds needed for composition with the physical graph flow. The small lifted displacement controls positive derivatives of the physical coordinate change without a physical-frequency Grönwall bound.

theorem EulerPhysicalGraphFlowBounds.Data.displacement_sup_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field (G.B * T) (ell⁻¹ * (4 * G.R * EulerCylinderGraphGevrey.graphFactor k m))

theorem EulerPhysicalGraphFlowBounds.Data.velocity_sup_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field G.B (ell⁻¹ * (EulerSmoothFlowGevrey.flowRadius G.B G.R T G.R * EulerCylinderGraphGevrey.graphFactor k m))

theorem EulerPhysicalGraphFlowBounds.Data.physical_positive_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) (n : ℕ) (hn : 0 < n) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n ((EulerSmoothBanachFlow.flowData T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell)).forward ↑t) x‖ ≤ (1 + G.B * T) * (1 + ell⁻¹ * (4 * G.R * EulerCylinderGraphGevrey.graphFactor k m)) ^ n * ↑n.factorial ^ 2

theorem EulerPacketGraphFlowFrequency.physical_bounds_of_costs (K B R T C1 k ell : ℝ) (hK : 0 ≤ K) (hB : 0 ≤ B) (hR : 0 ≤ R) (hT : 0 ≤ T) (hC1 : 0 ≤ C1) (hk : 1 ≤ k) (hell : 0 < ell) (hw : max 71 K ≤ k ^ (1 / 24)) (hroot : 16 ≤ k ^ (1 / 4)) (hRk : R ≤ EulerPacketSourceFrequency.smallPower k) (hTk : T ≤ EulerPacketSourceFrequency.smallPower k) (hCk : C1 ≤ EulerPacketSourceFrequency.smallPower k) (hsmall : B ≤ 2 * k ^ (-(1 / 2))) : K * (T * B) * (1 + EulerSmoothFlowGevrey.flowRadius B R T R) ≤ k ^ (-(1 / 4)) ∧ K * B * (1 + EulerSmoothFlowGevrey.flowRadius B R T R) ≤ k ^ (-(1 / 4)) ∧ K * (C1 + 3 * B ^ 2 * R) * (1 + EulerSmoothFlowGevrey.flowRadius B R T (6 * R)) ≤ k ^ (1 / 4) ∧ ell⁻¹ * (4 * EulerSmoothFlowGevrey.flowRadius B R T R * (1 + k)) ≤ ell⁻¹ * k ^ (5 / 4) ∧ ell⁻¹ * (4 * EulerSmoothFlowGevrey.flowRadius B R T (6 * R) * (1 + k)) ≤ ell⁻¹ * k ^ (5 / 4)

theorem EulerPhysicalGraphFlowBounds.data_field_bounds_explicit (P T : ℝ) [Fact (0 < P)] (G : Data P T) (k : ℝ) (hC : G.C = G.B) (hS : G.S = G.R) (hS1 : G.S₁ = G.R) (hk : 1 ≤ k) (hw : max 71 √(2 / P + 2 * P) ≤ k ^ (1 / 24)) (hroot : 16 ≤ k ^ (1 / 4)) (hB : G.B ≤ 2 * k ^ (-(1 / 2))) (hR : G.R ≤ EulerPacketSourceFrequency.smallPower k) (hC1 : G.C₁ ≤ EulerPacketSourceFrequency.smallPower k) (hT : T ≤ EulerPacketSourceFrequency.smallPower k) (m : EulerLiftedGradientSpace.Vector3) (hm : ‖m‖ = 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : (G.displacementField k m ell hell t).HasJetBound (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ (G.velocityField k m ell hell t).HasJetBound (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ (G.accelerationFieldL2 k m ell hell t).HasJetBound (k ^ (1 / 4)) (ell⁻¹ * k ^ (5 / 4))

theorem EulerPhysicalGraphFlowBounds.data_sup_bounds_explicit (P T : ℝ) [Fact (0 < P)] (G : Data P T) (k : ℝ) (hk : 1 ≤ k) (hw : 71 ≤ k ^ (1 / 24)) (hroot : 16 ≤ k ^ (1 / 4)) (hB : G.B ≤ 2 * k ^ (-(1 / 2))) (hR : G.R ≤ EulerPacketSourceFrequency.smallPower k) (hT : T ≤ EulerPacketSourceFrequency.smallPower k) (m : EulerLiftedGradientSpace.Vector3) (hm : ‖m‖ = 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : EulerGevrey.HasSupBound (G.displacementField k m ell hell t).field (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ EulerGevrey.HasSupBound (G.velocityField k m ell hell t).field (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4))

Fixed smooth matrix coefficients preserve the finite packet's inverse-frequency normalization with an explicit, frequency-independent cost. This also applies to the actual inverse-frame time derivative.

theorem EulerPacketCylinderField.MatrixCoefficient.normalized_approximation_bound {P T : ℝ} [Fact (0 < P)] {coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (K : MatrixCoefficient T coef) {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath K.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) {R k B C₁ C₂ : ℝ} (hG : G.WordBound 6 R (k⁻¹ * C₁ + k⁻¹ ^ 2 * C₂ + 2 * B * (k⁻¹ * B) ^ 3) 0) (hR : 0 ≤ R) (hKR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hk : 4 ≤ k) (hB0 : 0 ≤ B) (hB : B ≤ k ^ (1 / 100)) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) : ((K.multiply G).smul k).WordBound 6 R (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) 6 Rc C * (C₁ + C₂ + 1)) 0