Source-only budgets for the actual mean solver on the cylinder. The radius and inverse guards are fixed before the forcing amplitude, shift, or grade. The output fields are the genuine velocity, time derivative, and gradient of the normalized scalar pressure constructed by the source solver.

Fixed coefficient budgets for the actual mean packet inverse

These data contain only bounds on the prescribed coefficients and their fixed inverse costs. The external radius is chosen before the forcing grade or its scalar envelope, which is restored separately by homogeneity.

The source boundary operator has uniform Gevrey bounds under physical cutoff rescaling.

Factorial bounds for actual spatial derivatives of the localized Newtonian operator family.

@[instance_reducible]

noncomputable def EulerMeanBoundary.instPotentialOperatorNormedGroup : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanGradientTest.homogeneousSpace)

Reuse the additive structure of potential operators in derivative bounds.

Equations

• EulerMeanBoundary.instPotentialOperatorNormedGroup = inferInstance

@[instance_reducible]

noncomputable def EulerMeanBoundary.instCurlOperatorNormedGroup : NormedAddCommGroup (↥EulerMeanGradientTest.homogeneousSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Reuse the additive structure of curl operators in derivative bounds.

Equations

• EulerMeanBoundary.instCurlOperatorNormedGroup = inferInstance

@[instance_reducible]

noncomputable def EulerMeanBoundary.instPotentialOperatorNormedSpace : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanGradientTest.homogeneousSpace)

Reuse the scalar structure of potential operators in derivative bounds.

Equations

• EulerMeanBoundary.instPotentialOperatorNormedSpace = inferInstance

@[instance_reducible]

noncomputable def EulerMeanBoundary.instCurlOperatorNormedSpace : NormedSpace ℝ (↥EulerMeanGradientTest.homogeneousSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Reuse the scalar structure of curl operators in derivative bounds.

Equations

• EulerMeanBoundary.instCurlOperatorNormedSpace = inferInstance

theorem EulerMeanBoundary.majorant_four_radius (R : ℝ) (hR : 0 ≤ R) (n : ℕ) : EulerGevrey.majorant R 0 n ≤ EulerGevrey.majorant (4 * R) 0 n

theorem EulerMeanBoundary.majorant_next_four_radius (R : ℝ) (hR : 0 ≤ R) (n : ℕ) : EulerGevrey.majorant R 0 (n + 1) ≤ R * EulerGevrey.majorant (4 * R) 0 n

One extra derivative costs a fixed factor in the Gevrey radius, not a factorial shift.

noncomputable def EulerMeanBoundary.cutoffGevreyAmplitude (supportRadius coefficientRadius coefficientSize : ℝ) : ℝ

Cutoff gevrey amplitude, constructed using 3.

Equations

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

theorem EulerMeanBoundary.cutoffGevreyAmplitude_nonneg (R Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) : 0 ≤ cutoffGevreyAmplitude R Rc C

theorem EulerMeanBoundary.cutoffOperation_gevrey {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Cutoff → E) (hadd : ∀ (χ ψ : Cutoff), L (χ.add ψ) = L χ + L ψ) (hsmul : ∀ (χ : Cutoff) (c : ℝ), L (χ.scale c) = c • L χ) (hsub : ∀ (χ ψ : Cutoff), L (χ.sub ψ) = L χ - L ψ) (hbound : ∀ (χ : Cutoff), ‖L χ‖ ≤ cutoffBound χ) (χ : Cutoff) (R Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => L (χ.translate b)) a‖ ≤ cutoffGevreyAmplitude R Rc C * EulerGevrey.majorant (4 * Rc) 0 n

theorem EulerMeanBoundary.cutoffCurl_gevrey (χ : Cutoff) (R Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => cutoffCurl (χ.translate b)) a‖ ≤ cutoffGevreyAmplitude R Rc C * EulerGevrey.majorant (4 * Rc) 0 n

theorem EulerMeanBoundary.weakPotential_gevrey (χ : Cutoff) (R Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => weakPotential (χ.translate b)) a‖ ≤ cutoffGevreyAmplitude R Rc C * EulerGevrey.majorant (4 * Rc) 0 n

theorem EulerMeanBoundary.mixedBoundaryOperator_iteratedFDeriv_le (χ ψ : Cutoff) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => mixedBoundaryOperator (χ.translate b) (ψ.translate b)) a‖ ≤ ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ‖iteratedFDeriv ℝ k (fun (b : EulerSmoothLimit.Space) => cutoffCurl (χ.translate b)) a‖ * ‖iteratedFDeriv ℝ (n - k) (fun (b : EulerSmoothLimit.Space) => weakPotential (ψ.translate b)) a‖

The true derivatives split between the two cutoff positions by the bilinear derivative rule.

theorem EulerMeanBoundary.mixedBoundaryOperator_gevrey (χ ψ : Cutoff) (Rχ Rψ Rc Cχ Cψ : ℝ) (hRc : 0 ≤ Rc) (hCχ : 0 ≤ Cχ) (hCψ : 0 ≤ Cψ) (hsχ : tsupport χ.field ⊆ Metric.closedBall 0 Rχ) (hsψ : tsupport ψ.field ⊆ Metric.closedBall 0 Rψ) (hbχ : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ Cχ * EulerGevrey.majorant Rc 0 n) (hbψ : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n ψ.field x‖ ≤ Cψ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => mixedBoundaryOperator (χ.translate b) (ψ.translate b)) a‖ ≤ 3 * cutoffGevreyAmplitude Rχ Rc Cχ * cutoffGevreyAmplitude Rψ Rc Cψ * EulerGevrey.majorant (4 * Rc) 0 n

Factorial estimates follow from the genuine operator family, at every order and parameter.

noncomputable def EulerMeanBoundary.cutoffUnitBallFactor : ℝ

Cutoff unit ball factor, given by (Real.pi * 4 / 3) ^ (1/3 : ℝ).

Equations

• EulerMeanBoundary.cutoffUnitBallFactor = (Real.pi * 4 / 3) ^ (1 / 3)

theorem EulerMeanBoundary.cutoffUnitBallFactor_nonneg : 0 ≤ cutoffUnitBallFactor

theorem EulerMeanBoundary.closedBall_volume_oneThird (R : ℝ) (hR : 0 ≤ R) : (MeasureTheory.volume (Metric.closedBall 0 R)).toReal ^ (1 / 3) = R * cutoffUnitBallFactor

noncomputable def EulerMeanBoundary.scaledCutoffGevreySize : ℝ

Scaled cutoff gevrey size, given by (9 * (1 + 3 / EulerGevreyCutoff.bumpMass)^2)^3.

Equations

• EulerMeanBoundary.scaledCutoffGevreySize = (9 * (1 + 3 / EulerGevreyCutoff.bumpMass) ^ 2) ^ 3

theorem EulerMeanBoundary.scaledCutoffGevreySize_nonneg : 0 ≤ scaledCutoffGevreySize

theorem EulerMeanBoundary.scaledCutoff_scaledRadiusGevrey (ℓ : ℝ) (hℓ : 0 < ℓ) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (scaledCutoff ℓ hℓ).field x‖ ≤ scaledCutoffGevreySize * EulerGevrey.majorant (256 * ℓ) 0 n

The exact scaling factor is retained, so the L³ derivative term will cancel the support radius.

theorem EulerMeanBoundary.scaledCutoff_support_ball (ℓ : ℝ) (hℓ : 0 < ℓ) : tsupport (scaledCutoff ℓ hℓ).field ⊆ Metric.closedBall 0 (2 * ℓ⁻¹)

noncomputable def EulerMeanBoundary.scaledCutoffOperatorAmplitude : ℝ

This is one fixed dimensional constant, independent of the physical scale.

Equations

• EulerMeanBoundary.scaledCutoffOperatorAmplitude = 3 * EulerMeanCutoffCurl.cutoffCurlConstant * EulerMeanBoundary.scaledCutoffGevreySize * (1 + 512 * EulerMeanBoundary.cutoffUnitBallFactor)

theorem EulerMeanBoundary.scaledCutoffOperatorAmplitude_nonneg : 0 ≤ scaledCutoffOperatorAmplitude

theorem EulerMeanBoundary.scaledCutoff_amplitude (ℓ : ℝ) (hℓ : 0 < ℓ) : cutoffGevreyAmplitude (2 * ℓ⁻¹) (256 * ℓ) scaledCutoffGevreySize = scaledCutoffOperatorAmplitude

theorem EulerMeanBoundary.scaled_majorant_le (ℓ : ℝ) (hℓ : 0 ≤ ℓ) (hℓ1 : ℓ ≤ 1) (n : ℕ) : EulerGevrey.majorant (4 * (256 * ℓ)) 0 n ≤ EulerGevrey.majorant 1024 0 n

theorem EulerMeanBoundary.scaledCutoffCurl_gevrey (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => cutoffCurl ((scaledCutoff ℓ hℓ).translate b)) a‖ ≤ scaledCutoffOperatorAmplitude * EulerGevrey.majorant 1024 0 n

theorem EulerMeanBoundary.scaledWeakPotential_gevrey (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => weakPotential ((scaledCutoff ℓ hℓ).translate b)) a‖ ≤ scaledCutoffOperatorAmplitude * EulerGevrey.majorant 1024 0 n

noncomputable def EulerMeanBoundary.scaledBoundaryOperatorAmplitude : ℝ

Scaled boundary operator amplitude, given by 3 * scaledCutoffOperatorAmplitude^2.

Equations

• EulerMeanBoundary.scaledBoundaryOperatorAmplitude = 3 * EulerMeanBoundary.scaledCutoffOperatorAmplitude ^ 2

theorem EulerMeanBoundary.scaledBoundaryOperatorAmplitude_nonneg : 0 ≤ scaledBoundaryOperatorAmplitude

theorem EulerMeanBoundary.scaledBoundaryOperator_contDiff (ℓ : ℝ) (hℓ : 0 < ℓ) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => boundaryOperator ((scaledCutoff ℓ hℓ).translate a)

The source operator is genuinely smooth in the entire spatial translation parameter.

theorem EulerMeanBoundary.scaledBoundaryOperator_gevrey (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => boundaryOperator ((scaledCutoff ℓ hℓ).translate b)) a‖ ≤ scaledBoundaryOperatorAmplitude * EulerGevrey.majorant 1024 0 n

All actual operator derivatives have an unshifted Gevrey-two bound, uniformly for 0 < ℓ ≤ 1.

Genuine all-order spatial estimates for the translated mean inverse

The recurrence is proved for the actual coercive inverse. The translated solution is identified with the real spatial translation orbit before its iterated Fréchet derivatives are estimated. Coefficient and forcing amplitudes enter through explicit polynomials, independently of derivative order.

@[instance_reducible]

noncomputable def EulerMeanTranslatedGevrey.instMeanTranslatedGevrey1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedGevrey.instMeanTranslatedGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTranslatedGevrey.instMeanTranslatedGevrey2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedGevrey.instMeanTranslatedGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTranslatedGevrey.instMeanTranslatedGevrey3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedGevrey.instMeanTranslatedGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTranslatedGevrey.instMeanTranslatedGevrey4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedGevrey.instMeanTranslatedGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTranslatedGevrey.instMeanTranslatedGevrey5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedGevrey.instMeanTranslatedGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanTranslatedGevrey.instMeanTranslatedGevrey6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanTranslatedGevrey.instMeanTranslatedGevrey6 T = inferInstance

noncomputable def EulerMeanTranslatedGevrey.operatorAmplitude (T CF CF₁ CH CM CA L : ℝ) : ℝ

The proved polynomial amplitude for the actual fixed mean operator.

Equations

• EulerMeanTranslatedGevrey.operatorAmplitude T CF CF₁ CH CM CA L = 9 * (T * CF₁ + CF) ^ 2 * (1 + T ^ 2 / 2 * CH + T * (CM + |L| * CA))

def EulerMeanTranslatedGevrey.forcingAmplitude (T CF CF₁ Cf : ℝ) : ℝ

The proved polynomial amplitude of the actual forcing pullback.

Equations

• EulerMeanTranslatedGevrey.forcingAmplitude T CF CF₁ Cf = 3 * (T * (T * CF₁ + CF)) * Cf

theorem EulerMeanTranslatedGevrey.operatorAmplitude_nonneg (T CF CF₁ CH CM CA L : ℝ) (hT : 0 ≤ T) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCA : 0 ≤ CA) : 0 ≤ operatorAmplitude T CF CF₁ CH CM CA L

theorem EulerMeanTranslatedGevrey.forcingAmplitude_nonneg (T CF CF₁ Cf : ℝ) (hT : 0 ≤ T) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) : 0 ≤ forcingAmplitude T CF CF₁ Cf

theorem EulerMeanTranslatedGevrey.solution_translation_gevrey (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hH : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a H) (hM0 : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator a M0) (hA : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator a A) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM CA Cf : ℝ) (hRc : 0 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCA : 0 ≤ CA) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : c⁻¹ * operatorAmplitude T CF CF₁ CH CM CA L ≤ M) (hMD : c⁻¹ * forcingAmplitude T CF CF₁ Cf ≤ M) (hR : 2 * M * (Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator b M0) a‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (hAb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator b A) a‖ ≤ CA * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) a‖ ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hcoercive) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f))) x‖ ≤ EulerGevrey.majorant R (d + 1) n

Every actual spatial derivative of the solved mean field satisfies the factorial bound, with no assumed solution-jet recurrence.

Genuine fixed-Hq bounds for the constructed mean inverse

The input and output use the same ordered spatial words, the same fixed base Sobolev order, and the same radius. Only the known coefficient estimates are converted from tensor bounds. Their finite Sobolev cost is paid once, before applying the actual inverse recurrence.

@[instance_reducible]

noncomputable def EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedSobolevGevrey.instMeanFixedSobolevGevrey6 T = inferInstance

noncomputable def EulerMeanFixedSobolevGevrey.operatorBlockAmplitude (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc CF CF₁ CH CM CA L : ℝ) : ℝ

Coefficient-only amplitude of the full mean form in a fixed base order.

Equations

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

def EulerMeanFixedSobolevGevrey.forcingBlockAmplitude (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc CF CF₁ Cf : ℝ) : ℝ

Pulling back the right side is a multiplication in the same Sobolev block.

Equations

• EulerMeanFixedSobolevGevrey.forcingBlockAmplitude ι q T Rc CF CF₁ Cf = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc (T * (T * CF₁ + CF)) * Cf

theorem EulerMeanFixedSobolevGevrey.forcingOperator_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ (↑⊤) F) (hF₁ : ContDiff ℝ (↑⊤) F₁) (Rc CF CF₁ : ℝ) (hRc : 0 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F₁ x‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => -ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT (F y) (F₁ y))) x‖ ≤ T * (T * CF₁ + CF) * EulerGevrey.majorant Rc 0 n

Actual derivatives of the force-pullback operator, before applying it to any forcing. No forcing derivative is converted to a tensor norm.

theorem EulerMeanFixedSobolevGevrey.solution_translation_block_gevrey {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hc : 0 < c) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hH : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a H) (hM0 : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator a M0) (hA : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator a A) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM CA Cf : ℝ) (hRc : 0 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCA : 0 ≤ CA) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : EulerParameterWordGevrey.sobolevInverseCost c⁻¹ (operatorBlockAmplitude ι q T Rc CF CF₁ CH CM CA L) q * operatorBlockAmplitude ι q T Rc CF CF₁ CH CM CA L ≤ M) (hMD : EulerParameterWordGevrey.sobolevInverseCost c⁻¹ (operatorBlockAmplitude ι q T Rc CF CF₁ CH CM CA L) q * forcingBlockAmplitude ι q T Rc CF CF₁ Cf ≤ M) (hR : 2 * M * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b H) a‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator b M0) a‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (hAb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator b A) a‖ ≤ CA * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hcoercive) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f))) n x ≤ EulerGevrey.majorant R (d + 1) n

A genuine one-shift fixed-Hq estimate for the spatial orbit of the actual mean solution, at the identical forcing radius and with grade-independent constants. The fixed-Hq cost is computed from the original L² inverse.

The actual source mean coordinate inverse has Gevrey spatial bounds

The spatial lower bound, operator smoothness, cutoff derivatives, fixed-space transport, and inverse recurrence are all supplied by proved constructions. The remaining quantitative inputs are literal spatial derivatives of the given matrix coefficients and the actual translation derivatives of the forcing.

theorem EulerMeanSourceGevrey.translatedPath_bound (T : ℝ) (F : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hbound : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b (EulerMeanCoefficients.operatorPath T F.field)) a‖ ≤ C * EulerGevrey.majorant R 0 n

True spatial coefficient bounds become bounds for the conjugated operator path.

theorem EulerMeanSourceGevrey.translatedMultiplier_bound (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hbound : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑M0.field) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translateOperator b (EulerMeanCoefficients.multiplier M0.field)) a‖ ≤ C * EulerGevrey.majorant R 0 n

The initial matrix multiplier has the same literal spatial derivative bounds.

theorem EulerMeanSourceGevrey.sourceCoordinateSolver_translation_gevrey (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM Cf : ℝ) (hRc : 1024 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ * EulerMeanTranslatedGevrey.operatorAmplitude T CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L ≤ M) (hMD : (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ * EulerMeanTranslatedGevrey.forcingAmplitude T CF CF₁ Cf ≤ M) (hR : 2 * M * (Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₁.field t)) x‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑M0.field) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) a‖ ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) ((EulerMeanSourceFixedInverse.sourceCoordinateSolver T hT ℓ hℓ F F₁ H M0 FInv Be Bc L r hBe hBc hL hr hrquarter hext hcore hInv hF K hK hF0 hH hsmall) f)) a‖ ≤ EulerGevrey.majorant R (d + 1) n

The source coordinate solver obeys all-order genuine spatial estimates. Its coercivity and cutoff assumptions have already been discharged.

Concrete source estimates for the strong mean inverse

The literal source coefficient bounds and actual forcing orbit bounds imply the successive coordinate and physical-field factorial estimates. Coercivity, boundary cutoff calculus, Gram inversion, and time reconstruction are all proved constructions used by this theorem.

The actual source mean inverse preserves fixed Sobolev word estimates

The input and output are literal ordered spatial derivative blocks of actual L² translation orbits. Taking q=6 gives the fixed-H6 endpoint without spending six additional factorial shifts. All constants are independent of the grade.

theorem EulerMeanSourceSobolev.sourceCoordinateSolver_translation_block_gevrey {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM Cf : ℝ) (hRc : 1024 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L ≤ M) (hMD : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.forcingBlockAmplitude ι q T Rc CF CF₁ Cf ≤ M) (hR : 2 * M * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₁.field t)) x‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑M0.field) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) ((EulerMeanSourceFixedInverse.sourceCoordinateSolver T hT ℓ hℓ F F₁ H M0 FInv Be Bc L r hBe hBc hL hr hrquarter hext hcore hInv hF K hK hF0 hH hsmall) f)) n a ≤ EulerGevrey.majorant R (d + 1) n

Actual fixed-Hq source estimate, at one unchanged external radius and with one shift. All form coercivity and cutoff bounds are already proved.

theorem EulerMeanSourceStrongSobolev.velocity_translation_block_gevrey {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), ((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L (↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall) f)) f) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM Cf : ℝ) (hRc : 1024 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L ≤ M) (hMD : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.forcingBlockAmplitude ι q T Rc CF CF₁ Cf ≤ M) (hR : 2 * M * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₁.field t)) x‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑M0.field) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) n a ≤ EulerGevrey.majorant R (d + 1) n

The actual strong coordinate velocity inherits the bound of the actual source solver.

Uniform-time factorial bounds for the strong mean solution

The proved H¹ reconstruction estimates the continuous coordinate velocity. The actual continuous Gram inverse then controls acceleration and the physical time derivative. All bounds concern genuine spatial derivatives.

noncomputable def EulerMeanStrongContinuousGevrey.coordinateTraceCost (T : ℝ) : ℝ

The fixed H¹ trace cost for unit velocity and acceleration jet amplitudes.

Equations

• EulerMeanStrongContinuousGevrey.coordinateTraceCost T = T⁻¹ * √T + 2 * √T

theorem EulerMeanStrongContinuousGevrey.coordinateTraceCost_nonneg (T : ℝ) (hT : 0 ≤ T) : 0 ≤ coordinateTraceCost T

theorem EulerMeanVariationalInverse.StrongMeanEvolution.continuous_strong_spatial_gevrey {T : ℝ} {hT : 0 ≤ T} {FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)} {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : StrongMeanEvolution T hT FInv F F₁ A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hTpos : 0 < T) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (ha : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.acceleration) (hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) (Rc R CF CF₁ Cf : ℝ) (hRc : 0 ≤ Rc) (hR : 1 ≤ R) (hRcR : Rc ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) a‖ ≤ EulerGevrey.majorant R (d + 1) n) (hab : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.acceleration) a‖ ≤ EulerGevrey.majorant R (d + 2) n) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) fC) a‖ ≤ Cf * EulerGevrey.majorant R d n) (hstrong : 2 * EulerTimeLpGramGevrey.gramCost c CF (3 * CF * (Cf + 6 * CF₁ * EulerMeanStrongContinuousGevrey.coordinateTraceCost T)) * (Rc + 1) ≤ R) : (∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) (s.classicalAcceleration c hc hLower fC)) a‖ ≤ EulerGevrey.majorant R (d + 3) n) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.classicalPhysicalDerivative c hc hLower fC)) a‖ ≤ 3 * (CF₁ * EulerMeanStrongContinuousGevrey.coordinateTraceCost T + CF) * EulerGevrey.majorant R (d + 3) n

Actual continuous acceleration and B_t obey uniform-time spatial factorial bounds, with a fixed H¹ trace cost and one further Gram-inverse shift.

The genuine mean acceleration estimate in fixed-Hq external word blocks.

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ (L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev8 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev9 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev9 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanAccelerationSobolev.instMeanAccelerationSobolev10 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanAccelerationSobolev.instMeanAccelerationSobolev10 T = inferInstance

theorem EulerMeanAccelerationSobolev.meanAcceleration_translation_block_gevrey {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R CF CF₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf Cv) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) v) n a ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) (EulerMeanGramTranslation.meanAcceleration T hT F F₁ c hc hLower v f)) n a ≤ EulerGevrey.majorant R (d + 1) n

The actual acceleration of the constructed mean field spends one shift relative to its input blocks, at the same fixed Sobolev order and radius.

Actual spatial orbits of continuous mean acceleration

The ordinary solenoidal Gram inverse commutes with simultaneous translation of its data. This identifies the parameterized continuous solve with the genuine spatial orbit of the acceleration, including endpoint times.

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ (L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev8 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev9 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev9 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanContinuousSobolev.instMeanContinuousSobolev10 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanContinuousSobolev.instMeanContinuousSobolev10 T = inferInstance

theorem EulerMeanContinuousSobolev.meanAccelerationPath_translation_block_gevrey (T : ℝ) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T F) t) v‖ ^ 2) (v : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace)) (f : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T a) v) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) f) (Rc R CF CF₁ Cf Cv : ℝ) (hRc : 0 ≤ Rc) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (hCv : 0 ≤ Cv) (hstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf Cv) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) v) n a ≤ Cv * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation T b) (EulerMeanContinuousAcceleration.meanAccelerationPath T F F₁ c hc hLower v f)) n a ≤ EulerGevrey.majorant R (d + 1) n

Concrete source estimates for the strong mean inverse

The literal source coefficient bounds and actual forcing orbit bounds imply the successive coordinate and physical-field factorial estimates. Coercivity, boundary cutoff calculus, Gram inversion, and time reconstruction are all proved constructions used by this theorem.

Fixed-Hq bounds for the actual classical mean field and its time derivative

Starting with the proved weak inverse's one-shift coordinate bound, this result gives the actual continuous physical field at shift d+2 and its true within-time derivative at shift d+3. All use the identical external radius.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.strong_time_block_bounds {T : ℝ} {hT : 0 ≤ T} {FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)} {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : StrongMeanEvolution T hT FInv F F₁ A L u f) {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hTpos : 0 < T) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hRep : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC) (hFTime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) (Rc R CF CF₁ Cf : ℝ) (hRc : 0 ≤ Rc) (hR : 1 ≤ R) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (hstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hstrongC : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf (EulerMeanStrongContinuousGevrey.coordinateTraceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (hfCb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) fC) n a ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) n a ≤ EulerGevrey.majorant R (d + 1) n) : (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) s.continuousVelocity) n a ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF * EulerMeanStrongContinuousGevrey.coordinateTraceCost T * EulerGevrey.majorant R (d + 2) n) ∧ (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.classicalPhysicalDerivative c hc hLower fC)) n a ≤ 3 * (EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF₁ * EulerMeanStrongContinuousGevrey.coordinateTraceCost T + EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF) * EulerGevrey.majorant R (d + 3) n) ∧ ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT s.continuousVelocity) ((s.classicalPhysicalDerivative c hc hLower fC) t) (Set.Icc 0 T) ↑t

The true field and time derivative have same-radius fixed-Sobolev bounds. The time derivative is proved on [0,T], including within-set endpoints.

theorem EulerMeanSourceTimeSobolev.source_strong_time_block_bounds {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), ((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L (↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall) f)) f) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM Cf : ℝ) (hRc : 1024 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L ≤ M) (hMD : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.forcingBlockAmplitude ι q T Rc CF CF₁ Cf ≤ M) (hR : 2 * M * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₁.field t)) x‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑M0.field) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (hstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hstrongC : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf (EulerMeanStrongContinuousGevrey.coordinateTraceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hTpos : 0 < T) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hRep : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC) (hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) (hfCb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) fC) n a ≤ Cf * EulerGevrey.majorant R d n) : (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) s.continuousVelocity) n a ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF * EulerMeanStrongContinuousGevrey.coordinateTraceCost T * EulerGevrey.majorant R (d + 2) n) ∧ (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.classicalPhysicalDerivative (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) ⋯ ⋯ fC)) n a ≤ 3 * (EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF₁ * EulerMeanStrongContinuousGevrey.coordinateTraceCost T + EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF) * EulerGevrey.majorant R (d + 3) n) ∧ ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT s.continuousVelocity) ((s.classicalPhysicalDerivative (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) ⋯ ⋯ fC) t) (Set.Icc 0 T) ↑t

Literal source data and fixed-Hq forcing bounds imply the actual classical mean field at grade d+2 and its true time derivative at grade d+3, using the identical external radius throughout.

Fixed-Hq bounds for the actual physical mean pressure force

Starting with the proved weak inverse's one-shift coordinate bound, this result gives the actual continuous physical field at shift d+2 and its true within-time derivative at shift d+3. All use the identical external radius.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.pressure_time_block_bounds {T : ℝ} {hT : 0 ≤ T} {FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)} {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : StrongMeanEvolution T hT FInv F F₁ A L u f) {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (hTpos : 0 < T) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F) (hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁) (hv : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) s.velocityLp) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) (Rc R CF CF₁ Cf : ℝ) (hRc : 0 ≤ Rc) (hR : 1 ≤ R) (hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCf : 0 ≤ Cf) (hstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hstrongC : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf (EulerMeanStrongContinuousGevrey.coordinateTraceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (hfCb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) fC) n a ≤ Cf * EulerGevrey.majorant R d n) (hvb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T b) s.velocityLp) n a ≤ EulerGevrey.majorant R (d + 1) n) : (ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.pressurePath c hc hLower fC)) n a ≤ (Cf + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF + 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF₁ * EulerMeanStrongContinuousGevrey.coordinateTraceCost T) * EulerGevrey.majorant R (d + 3) n

The true pressure force retains the same radius and the time-derivative grade d+3.

Concrete source estimates for the strong mean inverse

The literal source coefficient bounds and actual forcing orbit bounds imply the successive coordinate and physical-field factorial estimates. Coercivity, boundary cutoff calculus, Gram inversion, and time reconstruction are all proved constructions used by this theorem.

theorem EulerMeanSourcePressureSobolev.source_pressure_block_bounds {ι : Type u_1} [Fintype ι] (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (hℓ1 : ℓ ≤ 1) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), ((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L (↑((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall) f)) f) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) (Rc R M CF CF₁ CH CM Cf : ℝ) (hRc : 1024 ≤ Rc) (hCF : 0 ≤ CF) (hCF₁ : 0 ≤ CF₁) (hCH : 0 ≤ CH) (hCM : 0 ≤ CM) (hCf : 0 ≤ Cf) (hM : 1 ≤ M) (hMC : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L ≤ M) (hMD : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity T F F₁ FInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q T Rc CF CF₁ CH CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude L) q * EulerMeanFixedSobolevGevrey.forcingBlockAmplitude ι q T Rc CF CF₁ Cf ≤ M) (hR : 2 * M * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hFb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ CF * EulerGevrey.majorant Rc 0 n) (hF₁b : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₁.field t)) x‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n) (hHb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(H.field t)) x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hMb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑M0.field) x‖ ≤ CM * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T b) f) n a ≤ Cf * EulerGevrey.majorant R d n) (hstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hstrongC : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) Rc CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc CF CF₁ Cf (EulerMeanStrongContinuousGevrey.coordinateTraceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hTpos : 0 < T) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) (hfCb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) fC) n a ≤ Cf * EulerGevrey.majorant R d n) : (ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) ⋯ ⋯ fC)) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.pressurePath (EulerMeanVariationalInverse.meanFrameCoercivity T FInv) ⋯ ⋯ fC)) n a ≤ (Cf + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF + 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF₁ * EulerMeanStrongContinuousGevrey.coordinateTraceCost T) * EulerGevrey.majorant R (d + 3) n

The literal source pressure force is smooth and has the same fixed-Hq grade as B_t.

structure EulerMeanPacketProvider.SobolevData (D : Data) (ι : Type u_1) [Fintype ι] (q : ℕ) (R : ℝ) : Type

Fixed coefficient and inverse budgets, with no conclusion about a solution.

• Rc : ℝ

  Rc of SobolevData, of type ℝ.

• M : ℝ

  M of SobolevData, of type ℝ.

• CF : ℝ

  CF of SobolevData, of type ℝ.

• CF₁ : ℝ

  CF₁ of SobolevData, of type ℝ.

• CH : ℝ

  CH of SobolevData, of type ℝ.

• CM : ℝ

  CM of SobolevData, of type ℝ.

• Cf : ℝ

  Cf of SobolevData, of type ℝ.

• radius_lower : 1024 ≤ self.Rc
• inverse_cost_lower : 1 ≤ self.M
• CF_nonneg : 0 ≤ self.CF
• CF₁_nonneg : 0 ≤ self.CF₁
• CH_nonneg : 0 ≤ self.CH
• CM_nonneg : 0 ≤ self.CM
• Cf_nonneg : 0 ≤ self.Cf
• operator_budget : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity D.T D.F D.F₁ D.opInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q D.T self.Rc self.CF self.CF₁ self.CH self.CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude D.L) q * EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q D.T self.Rc self.CF self.CF₁ self.CH self.CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude D.L ≤ self.M
• forcing_budget : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity D.T D.F D.F₁ D.opInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude ι q D.T self.Rc self.CF self.CF₁ self.CH self.CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude D.L) q * EulerMeanFixedSobolevGevrey.forcingBlockAmplitude ι q D.T self.Rc self.CF self.CF₁ self.Cf ≤ self.M
• radius_budget : 2 * self.M * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ R
• acceleration_budget : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower self.Rc self.CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q self.Rc self.CF self.CF₁ self.Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ R
• continuous_acceleration_budget : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q D.frameLower self.Rc self.CF (EulerParameterWordGevrey.accelerationBlockAmplitude ι q self.Rc self.CF self.CF₁ self.Cf (EulerMeanStrongContinuousGevrey.coordinateTraceCost D.T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ R
• frame_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ self.CF * EulerGevrey.majorant self.Rc 0 n
• frame_derivative_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ self.CF₁ * EulerGevrey.majorant self.Rc 0 n
• curvature_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.H.field t)) x‖ ≤ self.CH * EulerGevrey.majorant self.Rc 0 n
• initial_strain_bound (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑D.M0.field) x‖ ≤ self.CM * EulerGevrey.majorant self.Rc 0 n

noncomputable def EulerMeanPacketProvider.SobolevData.velocityAmplitude {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) : ℝ

Velocity amplitude, given by 3*sobolevCoefficientAmplitude ι q E.Rc E.CF*coordinateTraceCost D.T.

Equations

• E.velocityAmplitude = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q E.Rc E.CF * EulerMeanStrongContinuousGevrey.coordinateTraceCost D.T

noncomputable def EulerMeanPacketProvider.SobolevData.derivativeAmplitude {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) : ℝ

Derivative amplitude, given by 3*(sobolevCoefficientAmplitude ι q E.Rc E.CF₁*coordinateTraceCost D.T + sobolevCoefficientAmplitude ι q E.Rc E.CF).

Equations

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

noncomputable def EulerMeanPacketProvider.SobolevData.pressureAmplitude {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) : ℝ

Pressure amplitude, given by E.Cf+3*sobolevCoefficientAmplitude ι q E.Rc E.CF + 6*sobolevCoefficientAmplitude ι q E.Rc E.CF₁*coordinateTraceCost D.T.

Equations

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

theorem EulerMeanPacketProvider.SobolevData.normalized_bounds {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (d : ℕ) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation D.T b) G.lp) n a ≤ E.Cf * EulerGevrey.majorant R d n) (hfCb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.path) n a ≤ E.Cf * EulerGevrey.majorant R d n) : (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.velocityPath) n a ≤ E.velocityAmplitude * EulerGevrey.majorant R (d + 2) n) ∧ (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.derivativePath) n a ≤ E.derivativeAmplitude * EulerGevrey.majorant R (d + 3) n) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.pressureForcePath) n a ≤ E.pressureAmplitude * EulerGevrey.majorant R (d + 3) n

The concrete source estimates at the fixed budgets above.

Mean inverse estimates with an external forcing envelope

The scalar amplitude is normalized before the actual solve and restored by proved homogeneity. Every radius condition depends only on the fixed source data and the fixed normalized forcing scale, never on the recursive grade or its forcing envelope. Zero envelope is treated by actual zero forcing.

Homogeneity of the genuine mean packet solution

The selected strong representatives inherit the linearity of the actual coercive inverse. Consequently scalar forcing envelopes remain outside the velocity, time-derivative, and physical-pressure estimates.

theorem EulerMeanPacketProvider.Forcing.path_ae_raw {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (θ : ℝ) : ↑↑(G.path t) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => raw (↑t, x, θ)

theorem EulerMeanPacketProvider.Forcing.path_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.path = a • G.path

theorem EulerMeanPacketProvider.Forcing.lp_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.lp = a • G.lp

theorem EulerMeanPacketProvider.Forcing.velocityLp_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.solution.velocityLp = a • G.solution.velocityLp

theorem EulerMeanPacketProvider.Forcing.coordinate_velocity_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) (t : ↑(Set.Icc 0 D.T)) : H.solution.velocity ↑t = a • G.solution.velocity ↑t

Linearity of the L² solve fixes the continuous coordinate representative at every time.

theorem EulerMeanPacketProvider.Forcing.coordinateVelocityPath_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.solution.coordinateVelocityPath = a • G.solution.coordinateVelocityPath

theorem EulerMeanPacketProvider.Forcing.velocityPath_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.velocityPath = a • G.velocityPath

theorem EulerMeanPacketProvider.Forcing.derivativePath_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.derivativePath = a • G.derivativePath

The true within-time derivatives scale by uniqueness of the derivative.

theorem EulerMeanPacketProvider.Forcing.pressureForcePath_smul {D : Data} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (H : Forcing D raw') (a : ℝ) (hraw : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = a • raw (↑t, x, θ)) : H.pressureForcePath = a • G.pressureForcePath

The actual physical pressure residual scales, including at the time endpoints.

Zero forcing produces the actual zero velocity, derivative, and pressure force.

theorem EulerMeanPacketProvider.Forcing.raw_zero_of_path_zero {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hp : G.path = 0) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, x, θ) = 0

theorem EulerMeanPacketProvider.Forcing.paths_zero_of_raw_zero {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hz : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = 0) : G.velocityPath = 0 ∧ G.derivativePath = 0 ∧ G.pressureForcePath = 0

theorem EulerMeanPacketProvider.Forcing.paths_zero_of_path_zero {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hp : G.path = 0) : G.velocityPath = 0 ∧ G.derivativePath = 0 ∧ G.pressureForcePath = 0

theorem EulerMeanPacketProvider.SobolevData.envelope_bounds {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (d : ℕ) (A : ℝ) (hA : 0 ≤ A) (hfb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation D.T b) G.lp) n a ≤ A * (E.Cf * EulerGevrey.majorant R d n)) (hfCb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.path) n a ≤ A * (E.Cf * EulerGevrey.majorant R d n)) : (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.velocityPath) n a ≤ A * (E.velocityAmplitude * EulerGevrey.majorant R (d + 2) n)) ∧ (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.derivativePath) n a ≤ A * (E.derivativeAmplitude * EulerGevrey.majorant R (d + 3) n)) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.pressureForcePath) n a ≤ A * (E.pressureAmplitude * EulerGevrey.majorant R (d + 3) n)

The fixed-Hq mean inverse preserves one external radius for arbitrary nonnegative scalar forcing envelopes.

Exact parameter restriction transfers the ordinary mean estimates to the four-letter cylinder word alphabet. The zero angular direction is retained, so neither the external radius nor the fixed Sobolev order changes.

Exact parameter restriction and injective subalphabet bounds for genuine derivative words.

theorem EulerParameterWordGevrey.wordSum_subalphabet_le {P : Type u_1} {E : Type u_3} {ι : Type u_4} {κ : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [Fintype κ] (directions : κ → P) (e : ι → κ) (he : Function.Injective e) (f : P → E) (n : ℕ) (x : P) : wordSum (directions ∘ e) f n x ≤ wordSum directions f n x

Restricting an alphabet only discards nonnegative summands.

theorem EulerParameterWordGevrey.block_subalphabet_le {P : Type u_1} {E : Type u_3} {ι : Type u_4} {κ : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] [Fintype κ] (directions : κ → P) (e : ι → κ) (he : Function.Injective e) (q : ℕ) (f : P → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : block (directions ∘ e) q f n x ≤ block directions q f n x

The same literal subalphabet restriction is contractive on every fixed Sobolev block.

theorem EulerParameterWordGevrey.wordDerivative_comp_right {P : Type u_1} {Q : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] (directions : ι → P) (A : P →L[ℝ] Q) (f : Q → E) (hf : ContDiff ℝ (↑⊤) f) {n : ℕ} (w : Fin n → ι) (x : P) : wordDerivative directions (f ∘ ⇑A) w x = wordDerivative (⇑A ∘ directions) f w (A x)

A linear parameter map transports the actual directions exactly.

theorem EulerParameterWordGevrey.wordSum_comp_right {P : Type u_1} {Q : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (A : P →L[ℝ] Q) (f : Q → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : wordSum directions (f ∘ ⇑A) n x = wordSum (⇑A ∘ directions) f n (A x)

theorem EulerParameterWordGevrey.block_comp_right {P : Type u_1} {Q : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup Q] [NormedSpace ℝ Q] [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype ι] (directions : ι → P) (A : P →L[ℝ] Q) (q : ℕ) (f : Q → E) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : P) : block directions q (f ∘ ⇑A) n x = block (⇑A ∘ directions) q f n (A x)

Restricting parameters does not change a fixed block when the directions are transported.

noncomputable def EulerMeanPacketProvider.spatialDirection (i : Fin 4) : EulerSmoothLimit.Space

Spatial direction, given by (standardDirection i).1.

Equations

• EulerMeanPacketProvider.spatialDirection i = (EulerCylinderSobolev.standardDirection i).1

theorem EulerMeanPacketProvider.spatialDirection_norm (i : Fin 4) : ‖spatialDirection i‖ ≤ 1

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanCylinderWordBounds1 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanCylinderWordBounds1 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanCylinderWordBounds2 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanCylinderWordBounds2 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanCylinderWordBounds3 (P T : ℝ) [Fact (0 < P)] : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanCylinderWordBounds3 P T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanPacketProvider.instMeanCylinderWordBounds4 (P T : ℝ) [Fact (0 < P)] : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerMeanPacketProvider.instMeanCylinderWordBounds4 P T = inferInstance

theorem EulerMeanPacketProvider.spatialEmbeddingPath_norm (P T : ℝ) [Fact (0 < P)] : ‖spatialEmbeddingPath P T‖ ≤ √P

theorem EulerMeanPacketProvider.pathMean_spatialEmbeddingPath (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) : (EulerCylinderSpatialMean.pathMean P) ((spatialEmbeddingPath P T) p) = p

theorem EulerMeanPacketProvider.spatialEmbeddingPath_block_le (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (q n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((spatialEmbeddingPath P T) p)) n a ≤ √P * EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) p) n a.1

theorem EulerMeanPacketProvider.ordinaryPath_block_le (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (q n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) p) n a ≤ P⁻¹ * √P * EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((spatialEmbeddingPath P T) p)) n (a, 0)

theorem EulerMeanPacketProvider.ordinaryPath_majorant (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (q : ℕ) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((spatialEmbeddingPath P T) p)) n 0 ≤ A * EulerGevrey.majorant R d n) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) p) n a ≤ P⁻¹ * √P * A * EulerGevrey.majorant R d n

theorem EulerMeanPacketProvider.spatialEmbeddingPath_majorant (P T : ℝ) [Fact (0 < P)] (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (q : ℕ) (R A : ℝ) (d : ℕ) (hb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) p) n a ≤ A * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((spatialEmbeddingPath P T) p)) n 0 ≤ √P * A * EulerGevrey.majorant R d n

theorem EulerMeanPacketProvider.embedding_mean_norm_product (P : ℝ) [Fact (0 < P)] : √P * (P⁻¹ * √P) = 1

theorem EulerMeanPacketProvider.Forcing.ordinary_word_bound (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) {q : ℕ} {R A : ℝ} {d : ℕ} (hb : (toCylinderField P G).WordBound q R A d) (n : ℕ) (a : EulerSmoothLimit.Space) : EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.path) n a ≤ P⁻¹ * √P * A * EulerGevrey.majorant R d n

theorem EulerMeanPacketProvider.Forcing.toCylinderField_word_bound (P : ℝ) [Fact (0 < P)] {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) {q : ℕ} {R A : ℝ} {d : ℕ} (hb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.path) n a ≤ A * EulerGevrey.majorant R d n) : (toCylinderField P G).WordBound q R (√P * A) d

A single uniform-time forcing bound suffices for the normalized mean estimates.

theorem EulerMeanPacketProvider.SobolevData.radius_nonneg {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) : 0 ≤ R

theorem EulerMeanPacketProvider.SobolevData.path_envelope_bounds {D : Data} {ι : Type u_1} [Fintype ι] {q : ℕ} {R : ℝ} (E : SobolevData D ι q R) (hCf1 : 1 ≤ E.Cf) (hCfT : √D.T ≤ E.Cf) (directions : ι → EulerSmoothLimit.Space) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (d : ℕ) (A : ℝ) (hA : 0 ≤ A) (hb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.path) n a ≤ A * EulerGevrey.majorant R d n) : (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.velocityPath) n a ≤ A * (E.velocityAmplitude * EulerGevrey.majorant R (d + 2) n)) ∧ (∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.derivativePath) n a ≤ A * (E.derivativeAmplitude * EulerGevrey.majorant R (d + 3) n)) ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block directions q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.pressureForcePath) n a ≤ A * (E.pressureAmplitude * EulerGevrey.majorant R (d + 3) n)

The fixed normalized time factor may be chosen as max(1,sqrt(T)); it does not depend on the forcing grade or scalar envelope.

structure EulerMeanPacketProvider.Budget (D : Data) (q : ℕ) (R : ℝ) extends EulerMeanPacketProvider.SobolevData D (Fin 4) q R : Type

All quantitative inputs concern the source coefficients and their inverse. The fixed normalized forcing factor only accounts for time-L² inclusion.

• Rc : ℝ
• M : ℝ
• CF : ℝ
• CF₁ : ℝ
• CH : ℝ
• CM : ℝ
• Cf : ℝ
• radius_lower : 1024 ≤ self.Rc
• inverse_cost_lower : 1 ≤ self.M
• CF_nonneg : 0 ≤ self.CF
• CF₁_nonneg : 0 ≤ self.CF₁
• CH_nonneg : 0 ≤ self.CH
• CM_nonneg : 0 ≤ self.CM
• Cf_nonneg : 0 ≤ self.Cf
• operator_budget : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity D.T D.F D.F₁ D.opInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude (Fin 4) q D.T self.Rc self.CF self.CF₁ self.CH self.CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude D.L) q * EulerMeanFixedSobolevGevrey.operatorBlockAmplitude (Fin 4) q D.T self.Rc self.CF self.CF₁ self.CH self.CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude D.L ≤ self.M
• forcing_budget : EulerParameterWordGevrey.sobolevInverseCost (EulerMeanSourceFixedInverse.sourceFixedCoercivity D.T D.F D.F₁ D.opInv)⁻¹ (EulerMeanFixedSobolevGevrey.operatorBlockAmplitude (Fin 4) q D.T self.Rc self.CF self.CF₁ self.CH self.CM EulerMeanBoundary.scaledBoundaryOperatorAmplitude D.L) q * EulerMeanFixedSobolevGevrey.forcingBlockAmplitude (Fin 4) q D.T self.Rc self.CF self.CF₁ self.Cf ≤ self.M
• radius_budget : 2 * self.M * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) self.Rc + 1) ≤ R
• acceleration_budget : 2 * EulerTimeLpGramSobolev.gramBlockCost (Fin 4) q D.frameLower self.Rc self.CF (EulerParameterWordGevrey.accelerationBlockAmplitude (Fin 4) q self.Rc self.CF self.CF₁ self.Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) self.Rc + 1) ≤ R
• continuous_acceleration_budget : 2 * EulerTimeLpGramSobolev.gramBlockCost (Fin 4) q D.frameLower self.Rc self.CF (EulerParameterWordGevrey.accelerationBlockAmplitude (Fin 4) q self.Rc self.CF self.CF₁ self.Cf (EulerMeanStrongContinuousGevrey.coordinateTraceCost D.T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) self.Rc + 1) ≤ R
• frame_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ self.CF * EulerGevrey.majorant self.Rc 0 n
• frame_derivative_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ self.CF₁ * EulerGevrey.majorant self.Rc 0 n
• curvature_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.H.field t)) x‖ ≤ self.CH * EulerGevrey.majorant self.Rc 0 n
• initial_strain_bound (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑D.M0.field) x‖ ≤ self.CM * EulerGevrey.majorant self.Rc 0 n
• forcing_one : 1 ≤ self.Cf
• forcing_time : √D.T ≤ self.Cf

def EulerMeanPacketProvider.Data.frameCoefficient (D : Data) : EulerPacketCylinderField.MatrixCoefficient D.T fun (z : EulerPacketPointJets.Domain) => (D.F.field (D.clamp z.1)) z.2.1

Frame coefficient, bundling path, orbit, raw_eq.

Equations

• D.frameCoefficient = { path := D.F.field, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerMeanPacketProvider.Forcing.pressureForceCylinderField {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (P : ℝ) [Fact (0 < P)] : EulerPacketCylinderField.Field P D.T G.pressureForce

Pressure force cylinder field, given by G.pressureForceForcing.toCylinderField P.

Equations

• G.pressureForceCylinderField P = EulerMeanPacketProvider.Forcing.toCylinderField P G.pressureForceForcing

noncomputable def EulerMeanPacketProvider.Forcing.pressureGradientCylinderField {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (P : ℝ) [Fact (0 < P)] : EulerPacketCylinderField.Field P D.T (EulerPacketCylinderField.pressureGradient G.scalar)

This witness represents the literal spatial gradient encoded by the packet pressure jet, not merely the projected physical pressure force.

Equations

• G.pressureGradientCylinderField P = (D.frameCoefficient.adjoint.multiply (G.pressureForceCylinderField P)).congr ⋯

theorem EulerMeanPacketProvider.Forcing.restore_cylinder_word_bound {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (P : ℝ) [Fact (0 < P)] {q d : ℕ} {R A C : ℝ} (hb : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), EulerParameterWordGevrey.block spatialDirection q (fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T b) G.path) n a ≤ P⁻¹ * √P * A * (C * EulerGevrey.majorant R d n)) : (toCylinderField P G).WordBound q R (A * C) d

noncomputable def EulerMeanPacketProvider.Budget.velocityCost {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : ℝ

Velocity cost, given by B.toSobolevData.velocityAmplitude.

Equations

• B.velocityCost = B.velocityAmplitude

noncomputable def EulerMeanPacketProvider.Budget.derivativeCost {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : ℝ

Derivative cost, given by B.toSobolevData.derivativeAmplitude.

Equations

• B.derivativeCost = B.derivativeAmplitude

noncomputable def EulerMeanPacketProvider.Budget.pressureForceCost {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : ℝ

Pressure force cost, given by B.toSobolevData.pressureAmplitude.

Equations

• B.pressureForceCost = B.pressureAmplitude

noncomputable def EulerMeanPacketProvider.Budget.pressureGradientCost {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : ℝ

Pressure gradient cost, given by 3*sobolevCoefficientAmplitude (Fin 4) q B.Rc B.CF*B.pressureForceCost.

Equations

• B.pressureGradientCost = 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q B.Rc B.CF * B.pressureForceCost

theorem EulerMeanPacketProvider.Budget.coefficient_radius_nonneg {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : 0 ≤ B.Rc

theorem EulerMeanPacketProvider.Budget.radius_bounds {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : 1 ≤ R ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) B.Rc ≤ R

theorem EulerMeanPacketProvider.Budget.costs_nonneg {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) : 0 ≤ B.velocityCost ∧ 0 ≤ B.derivativeCost ∧ 0 ≤ B.pressureForceCost ∧ 0 ≤ B.pressureGradientCost

theorem EulerMeanPacketProvider.Budget.frameCoefficient_bound {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.frameCoefficient.path) a‖ ≤ B.CF * EulerGevrey.majorant B.Rc 0 n

theorem EulerMeanPacketProvider.Budget.physical_word_bounds {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) (P : ℝ) [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (d : ℕ) (A : ℝ) (hA : 0 ≤ A) (hG : (Forcing.toCylinderField P G).WordBound q R A d) : (Forcing.vectorCylinderField P G).WordBound q R (A * B.velocityCost) (d + 2) ∧ (Forcing.vectorDerivativeCylinderField P G).WordBound q R (A * B.derivativeCost) (d + 3) ∧ (G.pressureForceCylinderField P).WordBound q R (A * B.pressureForceCost) (d + 3)

Same-radius bounds on the three actual physical output paths. The period factors from averaging and constant extension cancel exactly.

theorem EulerMeanPacketProvider.Budget.word_bounds {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) (P : ℝ) [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (d : ℕ) (A : ℝ) (hA : 0 ≤ A) (hG : (Forcing.toCylinderField P G).WordBound q R A d) : (Forcing.vectorCylinderField P G).WordBound q R (A * B.velocityCost) (d + 2) ∧ (Forcing.vectorDerivativeCylinderField P G).WordBound q R (A * B.derivativeCost) (d + 3) ∧ (G.pressureGradientCylinderField P).WordBound q R (A * B.pressureGradientCost) (d + 3)

The mean solver consumes at most three shifts, with a linear forcing amplitude and the identical radius. The third output is d(bar q).

theorem EulerMeanPacketProvider.Budget.word_bounds_of_field {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) (P : ℝ) [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (d : ℕ) (A : ℝ) (hA : 0 ≤ A) (hF : F.WordBound q R A d) : (Forcing.vectorCylinderField P G).WordBound q R (A * B.velocityCost) (d + 2) ∧ (Forcing.vectorDerivativeCylinderField P G).WordBound q R (A * B.derivativeCost) (d + 3) ∧ (G.pressureGradientCylinderField P).WordBound q R (A * B.pressureGradientCost) (d + 3)

Any actual cylinder witness of the input raw forcing can supply the bound; the provider's canonical choice is immaterial.

theorem EulerMeanPacketProvider.Budget.three_shift_bounds {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) (P : ℝ) [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (d : ℕ) (A : ℝ) (hA : 0 ≤ A) (hF : F.WordBound q R A d) : (Forcing.vectorCylinderField P G).WordBound q R (A * B.velocityCost) (d + 3) ∧ (Forcing.vectorDerivativeCylinderField P G).WordBound q R (A * B.derivativeCost) (d + 3) ∧ (G.pressureGradientCylinderField P).WordBound q R (A * B.pressureGradientCost) (d + 3)

A common three-shift budget also covers the velocity, and is therefore within the source allowance of ten shifts.

theorem EulerMeanPacketProvider.Budget.grade_profile_bounds {D : Data} {q : ℕ} {R : ℝ} (B : Budget D q R) (P : ℝ) [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (F : EulerPacketCylinderField.Field P D.T raw) (p d : ℕ) (A H₀ : ℝ) (hA : 0 ≤ A) (hH₀ : 0 ≤ H₀) (hF : F.WordBound q R (A * H₀ ^ (2 * p - 2)) d) : (Forcing.vectorCylinderField P G).WordBound q R (A * B.velocityCost * H₀ ^ (2 * p - 2)) (d + 3) ∧ (Forcing.vectorDerivativeCylinderField P G).WordBound q R (A * B.derivativeCost * H₀ ^ (2 * p - 2)) (d + 3) ∧ (G.pressureGradientCylinderField P).WordBound q R (A * B.pressureGradientCost * H₀ ^ (2 * p - 2)) (d + 3)

The mean profile H₀^(2p−2) is a constant scalar envelope. The same fixed source budget applies at every grade and every derivative shift.