LeanPool.NavierStokesAndEuler.Euler.GevreyPressureShifted

Cutoff-independent nonlinear pressure bounds for actual finite-Sobolev transport sources.

The lower Sobolev pressure estimate needed for the base energy commutator.

∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Pressure.blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) 5 n ≤ (2 * M * (5460 * lowerProductConstant period 3) * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * wordSobolevNorm period 6 l b) * ∑ j ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ j * wordSobolevNorm period 6 j e

The genuine pressure of transport has an unshifted H⁵ bound using only H⁶ velocity at the same external cutoff.

source

@[instance_reducible]

noncomputable def EulerGevreyPressureTransport.pressureTransportGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) :

NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

EulerGevreyPressureTransport.pressureTransportGroup period q = inferInstance

Instances For

source

@[instance_reducible]

noncomputable def EulerGevreyPressureTransport.pressureTransportSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) :

NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

EulerGevreyPressureTransport.pressureTransportSpace period q = inferInstance

Instances For

source

theorem EulerGevreyPressureTransport.pressure_block_eq (period : ℝ) [Fact (0 < period)] {s q n : ℕ} {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) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (h : n + q ≤ s) :

EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) u)) q n = EulerH6Pressure.blockNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos (EulerCylinderSobolevSpace.toJet period u)) q n

Actual coefficient pressure blocks agree with the genuine pressure-jet construction.

source

noncomputable def EulerGevreyPressureTransport.transportPressure (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) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) :

↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The actual finite-Sobolev pressure generated by the nonlinear transport source.

Equations

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

Instances For

source

theorem EulerGevreyPressureTransport.transportPressure_continuous (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) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) :

Continuous fun (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) => transportPressure period hs K κ m c hc hpos L hL p.1 p.2

The nonlinear pressure depends continuously on its actual Sobolev velocity inputs.

source

theorem EulerGevreyPressureTransport.velocityMap_weighted_bound (period : ℝ) [Fact (0 < period)] (q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) :

∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period q n (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) ≤ 4 * ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period q n f

The four-component lifted velocity bound in a finite weighted norm.

source

EulerSobolevGevreyOperators.weightedNorm period 5 N ρ (transportPressure period hs K κ m c hc hpos L hL u v) ≤ 8 * M * (5460 * EulerH6Nonlinear.lowerProductConstant period 3) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v

The actual unshifted H⁵ nonlinear pressure estimate on smooth Sobolev representatives.

source

theorem EulerGevreyPressureTransport.transportPressure_lower (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 + 5 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase : (EulerH6Pressure.CoefficientJet.restrict K 5 ⋯).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 5 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))) :

The lower-order nonlinear pressure estimate holds for the actual finite-Sobolev fields used by the solver.

source

@[instance_reducible]

noncomputable def EulerGevreyPressureTransport.shiftedTransportGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) :

NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

EulerGevreyPressureTransport.shiftedTransportGroup period q = inferInstance

Instances For

source

@[instance_reducible]

noncomputable def EulerGevreyPressureTransport.shiftedTransportSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) :

NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

EulerGevreyPressureTransport.shiftedTransportSpace period q = inferInstance

Instances For

source

noncomputable def EulerGevreyPressureTransport.shiftedPressureNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (ρ : ℝ) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) :

ℝ

The shifted actual H⁶ pressure sum stops one derivative below the velocity cutoff.

Equations

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

Instances For

source

theorem EulerGevreyPressureTransport.continuous_shiftedPressureNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) :

Continuous (shiftedPressureNorm period N ρ)

Continuity on the genuine Sobolev domain of the shifted pressure norm.

source

shiftedPressureNorm period N ρ (transportPressure period hs K κ m c hc hpos L hL u v) ≤ 16 * M * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 (N + 1) ρ u * EulerSobolevTransportCommutator.weightedLoss period 6 (N + 1) ρ v

The actual shifted H⁶ nonlinear pressure estimate on smooth Sobolev representatives.

source

theorem EulerGevreyPressureTransport.transportPressure_shifted (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 + 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 → 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))) :

The shifted nonlinear pressure estimate holds for the actual finite-Sobolev fields used by the solver.