Related estimates used together by the same construction modules.

Quantitative Hessian errors retain one inverse-frequency factor. The coefficient bounds are those of the actual source deformation.

noncomputable def EulerPacketGraphHessian.fastHessianCost {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R₀ : ℝ} (NB : EulerTransversePacketJoin.NormalBudget D q R₀) (R A : ℝ) : ℝ

Fast hessian cost, given by sobolevEmbeddingConstant P 3*A*NB.C^2*(NB.Rc+‖coordinateEquiv.symm.toContinuousLinearMap‖*R).

Equations

• EulerPacketGraphHessian.fastHessianCost NB R A = EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A * NB.C ^ 2 * (NB.Rc + ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * R)

theorem EulerPacketGraphHessian.fastHessianRemainder_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R₀ : ℝ} (NB : EulerTransversePacketJoin.NormalBudget D q R₀) (a : EulerPacketProfileRecursion.ScalarField) (G : EulerPacketCylinderField.Field P D.T fun (z : EulerPacketPointJets.Domain) => a z • D.m₀) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hG : G.WordBound 6 R A 0) (k : ℝ) (hk : 0 < k) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) (ha : DifferentiableAt ℝ (fun (z : EulerSmoothLimit.Space × ℝ) => a (↑t, z)) ((EulerGraphPullback.graphMap k D.m₀) (Y x))) : ‖fastHessianRemainder (fun (z : EulerLiftedGradientSpace.LiftTangent) => a (↑t, z)) k D.m₀ Y (fun (y : EulerSmoothLimit.Space) => (D.FInv.field t) (Y y)) x‖ ≤ fastHessianCost NB R A / k

noncomputable def EulerPacketGraphHessian.physicalCovector {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (_G : EulerPacketCylinderField.Field P D.T raw) (k : ℝ) (Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Physical covector, given by (D.FInv.field t (Y t x)).adjoint (raw (t,(Y t x,k*⟪D.m₀,Y t x⟫_ℝ))).

Equations

• EulerPacketGraphHessian.physicalCovector D _G k Y t x = (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t x))) (raw (↑t, Y t x, k * inner ℝ D.m₀ (Y t x)))

theorem EulerPacketGraphHessian.physicalCovector_error_bound {P : ℝ} [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P D.T raw) (R A : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (k : ℝ) (hk : 1 ≤ k) (hG : G.WordBound 6 R (A / k ^ 2) 0) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (physicalCovector D G k Y t) x‖ ≤ 9 * C * EulerPacketPhysicalGevrey.physicalFixedCost D Rc C R 1 * EulerCylinderSobolevSpace.sobolevEmbeddingConstant P 3 * A / k

The finite pressure covector differs from the leading angular primary by an actual O(k⁻²) cylinder field, uniformly in the truncation length selected by the source frequency guard.

noncomputable def EulerPacketPressure.covectorGradeField {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (m : EulerSmoothLimit.Space) (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T ⋯ support (a i)) {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (K : (i : ℕ) → i ≤ N → EulerPacketCylinderField.PressureBudget P T ⋯ m (a i) S R i) (i : ℕ) : EulerPacketCylinderField.Field P T (covectorGrades N m a i)

Covector grade field, constructed using Field.assembleFamily.

Equations

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

theorem EulerPacketPressure.covectorGrade_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (m : EulerSmoothLimit.Space) (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T ⋯ support (a i)) {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (K : (i : ℕ) → i ≤ N → EulerPacketCylinderField.PressureBudget P T ⋯ m (a i) S R i) (hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i) (hR : 1 ≤ R) (ha : a 0 = 0) (i : ℕ) : (covectorGradeField hT m G K i).WordBound 6 R (3 * S.H0 ^ (2 * i)) (EulerPacketShiftArithmetic.highShift i)

theorem EulerPacketPressure.covectorGrades_zero {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (m : EulerSmoothLimit.Space) (ha : a 0 = 0) : covectorGrades N m a 0 = 0

theorem EulerPacketPressure.covectorGrades_one {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (m : EulerSmoothLimit.Space) (ha : a 0 = 0) (hN : 1 ≤ N) (hm : (a 1).meanPressure = 0) : covectorGrades N m a 1 = angularPressure m (a 1).highPressure

noncomputable def EulerPacketPressure.covectorRemainder {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (m : EulerSmoothLimit.Space) (κ : ℝ) : EulerPacketProfileRecursion.VectorField

Covector remainder, given by fieldSum (N+1) κ (covectorGrades N m a)-κ • angularPressure m (a 1).highPressure.

Equations

• EulerPacketPressure.covectorRemainder m κ = EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketPressure.covectorGrades N m a) - κ • EulerPacketPressure.angularPressure m (a 1).highPressure

noncomputable def EulerPacketPressure.covectorRemainderField {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (m : EulerSmoothLimit.Space) (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T ⋯ support (a i)) {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (K : (i : ℕ) → i ≤ N → EulerPacketCylinderField.PressureBudget P T ⋯ m (a i) S R i) (ha : a 0 = 0) (hN : 1 ≤ N) (hm : (a 1).meanPressure = 0) (κ : ℝ) : EulerPacketCylinderField.Field P T (covectorRemainder m κ)

Covector remainder field as an element of Field P T (covectorRemainder (N := N) (a := a) m κ).

Equations

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

theorem EulerPacketPressure.covectorRemainder_bound {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (m : EulerSmoothLimit.Space) (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T ⋯ support (a i)) {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} (K : (i : ℕ) → i ≤ N → EulerPacketCylinderField.PressureBudget P T ⋯ m (a i) S R i) (hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i) (hR : 1 ≤ R) (ha : a 0 = 0) (hN : 1 ≤ N) (hm : (a 1).meanPressure = 0) {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData P T O} (BC : EulerPacketCylinderField.CoefficientBudget C) (k : ℝ) (hk : 4 ≤ k) (hbase : EulerPacketCoarseMajorant.tailBase R S.H0 BC.termCost N ≤ k ^ (1 / 100)) : (covectorRemainderField hT m G K ha hN hm k⁻¹).WordBound 6 (4 * R) ((EulerPacketCylinderField.fixedVelocityGradeCost R S.H0 2 + 2) / k ^ 2) 0