The actual pressure commutators occurring in the Gevrey energy estimate.
noncomputable def
EulerGevreyPressureEnergy.externalPressureNorm
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A)
(N : ℕ)
(ρ : ℝ)
(p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
The actual weighted H⁶ external pressure commutator norm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerGevreyPressureEnergy.basePressureNorm
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A)
(N : ℕ)
(hN : N + 6 ≤ s)
(ρ : ℝ)
(p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
The actual weighted L² base pressure commutator norm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerGevreyPressureEnergy.externalPressureNorm_unshifted
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A)
(N : ℕ)
(hN : N + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
externalPressureNorm period K N ρ p ≤ EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ p
Ordinary coefficient-product control for the actual external pressure commutator.
theorem
EulerGevreyPressureEnergy.externalPressureNorm_shifted
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A)
(N : ℕ)
(hN : N + 1 + 6 ≤ s)
(ρ Rc : ℝ)
(hρ : 0 < ρ)
(hRc : 0 ≤ Rc)
(hsmall : ρ * Rc ≤ 1 / 2)
(hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N + 1 → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2)
(p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
externalPressureNorm period K (N + 1) ρ p ≤ 2 * Rc * EulerGevreyPressureTransport.shiftedPressureNorm period N ρ p
External pressure commutators use only shifted pressure orders strictly below the chosen cutoff.
theorem
EulerGevreyPressureEnergy.basePressureNorm_lower
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A)
(N : ℕ)
(hN : N + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
basePressureNorm period K N hN ρ p ≤ 448 * EulerBasePressureCommutator.baseCoefficientSum period K * EulerSobolevGevreyOperators.weightedNorm period 5 N ρ p
Actual base pressure commutators are controlled by the unshifted one-order-lower pressure norm.
theorem
EulerGevreyPressureEnergy.basePressureNorm_unshifted
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A)
(N : ℕ)
(hN : N + 6 ≤ s)
(ρ : ℝ)
(hρ : 0 < ρ)
(p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
basePressureNorm period K N hN ρ p ≤ 448 * EulerBasePressureCommutator.baseCoefficientSum period K * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ p
The same actual base commutators can be controlled by an available H⁶ pressure bound.
theorem
EulerGevreyPressureEnergy.nonlinear_externalPressure_bound
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
(hs : 6 ≤ s)
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v)
(N : ℕ)
(hN : N + 1 + 6 ≤ s)
(ρ Rc M : ℝ)
(hρ : 0 < ρ)
(hRc : 0 ≤ Rc)
(hM : 1 ≤ M)
(hbase : (EulerH6Pressure.CoefficientJet.restrict K 6 hs).pressureConstant c ≤ M)
(hsmall : 4 * M * (ρ * Rc) ≤ 1)
(hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N + 1 → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2)
(L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ)
(hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1)
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))
:
externalPressureNorm period K (N + 1) ρ
(EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v) ≤ 32 * Rc * M * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 (N + 1) ρ u * EulerSobolevTransportCommutator.weightedLoss period 6 (N + 1) ρ v
The actual nonlinear transport pressure has the required external commutator bound with no extra velocity order.