Exact transport/order-zero splitting of the constructed correction source and its actual pressure.

@[instance_reducible]

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

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

Equations

• EulerGevreyOrderZero.splitGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerGevreyOrderZero.splitSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerGevreyOrderZero.splitBilinearGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : SeminormedAddCommGroup (↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

Cache the standard SeminormedAddCommGroup (SobolevSpace period (q+1) →L[ℝ] SobolevSpace period (q+1) →L[ℝ] SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerGevreyOrderZero.splitBilinearGroup period q = inferInstance

theorem EulerGevreyOrderZero.algebraicAt_eq (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 + 1))) : algebraicAt period hs C ((EulerCylinderSobolevSpace.truncateOperator period s) u) ((EulerCylinderSobolevSpace.truncateOperator period s) v) = ((EulerCorrectionOperators.algebraicBilinear period hs C) u) v

The fixed-level algebraic expression is exactly the algebraic term used in the mild solver.

theorem EulerGevreyOrderZero.backgroundDrift_eq (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u background : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : backgroundDrift period hs L hL background ((EulerCylinderSobolevSpace.truncateOperator period s) u) = ((EulerSobolevTransport.transportBilinear period hs L hL) u) background

The order-zero background transport is exactly e·D z_a in the mild solver.

theorem EulerGevreyOrderZero.correction_split_identity (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 e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : r + (EulerCorrectionOperators.linearize (EulerCorrectionOperators.eulerBilinear period hs L hL C) (C0 ∘SL EulerCylinderSobolevSpace.truncateOperator period s) background) e + ((EulerCorrectionOperators.eulerBilinear period hs L hL C) e) e = ((EulerSobolevTransport.transportBilinear period hs L hL) (background + e)) e + orderZeroSource period hs L hL C0 C background r ((EulerCylinderSobolevSpace.truncateOperator period s) e)

Exact splitting of the actual nonlinear increment into top transport plus the order-zero source.

theorem EulerGevreyOrderZero.weightedNorm_neg (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerSobolevGevreyOperators.weightedNorm period q N ρ (-u) = EulerSobolevGevreyOperators.weightedNorm period q N ρ u

Actual finite weighted Sobolev norms are invariant under sign.

theorem EulerGevreyOrderZero.orderZeroPressure_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (G : EulerSpatialSobolevInverse.SmoothCoefficient period) (KG : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s G) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((G.coefficient x) v) v) (hbase : (EulerH6Pressure.CoefficientJet.restrict KG 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period KG 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (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 ρ (-(EulerSobolevCoefficientPressure.pressureSobolevOperator period KG κ m c hc hpos) (orderZeroSource period hs L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) background r e)) ≤ 2 * M * (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 actual order-zero pressure bound follows from the genuine projected inverse and the derived nonlinear estimate.

theorem EulerGevreyOrderZero.correctionData_rawSource_split (period : ℝ) [Fact (0 < period)] {s : ℕ} {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period s T) (hs : 6 ≤ s) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerCorrectionOperators.CorrectionData.rawSource period D hs t e = ((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents D.κ D.direction) ⋯) (D.approximation t + e)) e + orderZeroSource period hs (EulerSobolevTransport.velocityComponents D.κ D.direction) ⋯ (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.linear.jet t)) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period ((D.quadratic i).jet t)) (D.approximation t) (D.residual t) ((EulerCylinderSobolevSpace.truncateOperator period s) e)

The solver's actual raw source has exactly the transport/order-zero decomposition used by the energy estimate.

theorem EulerGevreyOrderZero.correctionData_pressure_split (period : ℝ) [Fact (0 < period)] {s : ℕ} {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period s T) (hs : 6 ≤ s) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerCorrectionOperators.CorrectionData.pressure period D hs t e = -(EulerSobolevCoefficientPressure.pressureSobolevOperator period (D.metric.jet t) D.κ D.direction D.coercivity ⋯ ⋯) (((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents D.κ D.direction) ⋯) (D.approximation t + e)) e) + -(EulerSobolevCoefficientPressure.pressureSobolevOperator period (D.metric.jet t) D.κ D.direction D.coercivity ⋯ ⋯) (orderZeroSource period hs (EulerSobolevTransport.velocityComponents D.κ D.direction) ⋯ (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.linear.jet t)) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period ((D.quadratic i).jet t)) (D.approximation t) (D.residual t) ((EulerCylinderSobolevSpace.truncateOperator period s) e))

The actual signed correction pressure is the sum of its order-zero and transport pressure solves.