Cutoff-independent bounds for the actual order-zero Euler correction source.

@[instance_reducible]

noncomputable def EulerGevreyOrderZero.orderZeroGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

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

Equations

• EulerGevreyOrderZero.orderZeroGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerGevreyOrderZero.orderZeroSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

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

Equations

• EulerGevreyOrderZero.orderZeroSpace period q = inferInstance

noncomputable def EulerGevreyOrderZero.algebraicAt (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The actual derivative-free algebraic nonlinearity at one complete Sobolev level.

Equations

• EulerGevreyOrderZero.algebraicAt period hs C u v = ∑ i : Fin 3, (C i) (EulerSobolevL2Product.productHq period hs (EulerVectorCylinder.coordinate 3 i) ⋯ u v)

noncomputable def EulerGevreyOrderZero.backgroundDrift (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (background : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The part e·D z_a transports the prescribed background and has no derivative on the error.

Equations

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

theorem EulerGevreyOrderZero.algebraicAt_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s (C i)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ (algebraicAt period hs (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) u v) ≤ (∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period (K i) 6 N ρ) * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v

The actual coefficient-weighted quadratic field has a uniform truncated Gevrey bound.

theorem EulerGevreyOrderZero.backgroundDrift_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (background : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ (backgroundDrift period hs L hL background e) ≤ EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e * ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.derivativeOperator period s i) background)

Background transport is order zero in the error in the actual finite Gevrey norm.

noncomputable def EulerGevreyOrderZero.orderZeroSource (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (background : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r e : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)

The actual order-zero source Z(e)+r_a in the transformed Euler correction equation.

Equations

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

theorem EulerGevreyOrderZero.orderZeroSource_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : EulerSpatialSobolevInverse.SmoothCoefficient period) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s C0) (C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s (C i)) (background : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r e : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ (orderZeroSource period hs L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) background r e) ≤ EulerSobolevGevreyOperators.weightedNorm period 6 N ρ r + (EulerH6Nonlinear.productConstant period 3 * ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.derivativeOperator period s i) background) + EulerSobolevGevreyOperators.weightedCoefficient period K0 6 N ρ + (2 * ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period (K i) 6 N ρ) * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.truncateOperator period s) background)) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e + (∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period (K i) 6 N ρ) * EulerH6Nonlinear.productConstant period 3 * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ e ^ 2

The source's actual order-zero forcing is bounded by residual, linear, and quadratic error energies, with no cutoff-dependent constant.