LeanPool.NavierStokesAndEuler.Euler.PacketPhysicalPressureGevrey

The physical pressure force κF⁻ᵀp has the same fixed polynomial frequency losses as the velocity correction. The inverse-transpose coefficient bounds follow from the actual determinant-one deformation.

source

noncomputable def EulerPacketPhysicalGevrey.graphPressureForce {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

EulerSmoothLimit.Space

Graph pressure force, given by κ • (D.FInv.field t x).adjoint (physicalField P k D.m₀ (e t) x).

Equations

EulerPacketPhysicalGevrey.graphPressureForce D P κ k e t x = κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) x)) (EulerCylinderPhysicalTensor.physicalField P k D.m₀ (e t) x)

Instances For

source

theorem EulerPacketPhysicalGevrey.graphPressureForce_contDiff {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (e t) x)) (t : ↑(Set.Icc 0 D.T)) :

ContDiff ℝ (↑⊤) (graphPressureForce D P κ k e t)

source

theorem EulerPacketPhysicalGevrey.inverseTranspose_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C : ℝ) (hR : 0 ≤ R) (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 R 0 n) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => ContinuousLinearMap.adjoint ((D.FInv.field t) y)) x‖ ≤ 9 * C ^ 2 * EulerGevrey.majorant R 0 n

source

theorem EulerPacketPhysicalGevrey.graphPressureForce_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (e t) x)) (R C A S : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hA : 0 ≤ A) (hS : 0 ≤ S) (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 R 0 n) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (e t) x‖ ≤ A * S ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

‖iteratedFDeriv ℝ n (graphPressureForce D P κ k e t) x‖ ≤ |κ| * 27 * C ^ 2 * A * EulerGevrey.majorant (R + EulerCylinderPhysicalTensor.frequencyFactor k D.m₀ * S) 0 n

source

noncomputable def EulerPacketPhysicalGevrey.physicalPressureForce {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

EulerSmoothLimit.Space

Physical pressure force, given by graphPressureForce D P κ k e t (Y t x).

Equations

EulerPacketPhysicalGevrey.physicalPressureForce D P κ k e Y t x = EulerPacketPhysicalGevrey.graphPressureForce D P κ k e t (Y t x)

Instances For

source

‖iteratedFDeriv ℝ n (physicalPressureForce D P κ k e Y t) x‖ ≤ |κ| * 27 * C ^ 2 * A * physicalRadius D k R C S ^ n * ↑n.factorial ^ 2

source

theorem EulerPacketPhysicalGevrey.physicalPressureForce_power_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P κ k : ℝ) (e : ↑(Set.Icc 0 D.T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (he : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (e t) x)) (R C A S : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hA : 0 ≤ A) (hS : 0 ≤ S) (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 R 0 n) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P), ∑ w : Fin n → Fin 4, ‖EulerCylinderSobolev.iteratedFieldDerivative P w (e t) x‖ ≤ A * S ^ n * ↑n.factorial ^ 2) (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) (hk : 1 ≤ k) (hκ : |κ| ≤ 1) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) :

‖iteratedFDeriv ℝ n (physicalPressureForce D P κ k e Y t) x‖ ≤ 9 * C * physicalFixedCost D R C S n * A * k ^ n