A genuine local divergence-free viscous correction for the transformed Euler equation.

The actual time-dependent coefficients and nonlinear source of the lifted Euler correction.

Local boundedness, continuity, and differentiation derived from an exact operator resolvent identity.

theorem EulerResolventCalculus.local_norm_bound {R : Type u_1} [NormedRing R] (P Q M N : R) (hres : Q - P = Q * ((M - N) * P)) (hsmall : ‖M - N‖ * ‖P‖ ≤ 1 / 2) : ‖Q‖ ≤ 2 * ‖P‖

An exact resolvent identity gives a local inverse bound without assuming a uniform inverse estimate.

theorem EulerResolventCalculus.local_difference_bound {R : Type u_1} [NormedRing R] (P Q M N : R) (hres : Q - P = Q * ((M - N) * P)) (hsmall : ‖M - N‖ * ‖P‖ ≤ 1 / 2) : ‖Q - P‖ ≤ 2 * ‖P‖ ^ 2 * ‖M - N‖

The exact resolvent identity yields a local Lipschitz estimate using only the reference inverse norm.

theorem EulerResolventCalculus.continuousAt_of_resolvent {R : Type u_1} [NormedRing R] {α : Type u_2} [TopologicalSpace α] (P M : α → R) (hres : ∀ (s t : α), P s - P t = P s * ((M t - M s) * P t)) (t : α) (hM : ContinuousAt M t) : ContinuousAt P t

Continuity of the coefficient operator implies continuity of actual resolvents, with no separate inverse-continuity assumption.

theorem EulerResolventCalculus.hasDerivAt_of_resolvent {R : Type u_1} [NormedRing R] [NormedAlgebra ℝ R] (P M : ℝ → R) (hres : ∀ (s t : ℝ), P s - P t = P s * ((M t - M s) * P t)) (t : ℝ) (M' : R) (hM : HasDerivAt M M' t) : HasDerivAt P (-(P t * (M' * P t))) t

Differentiating the actual resolvent identity gives the inverse derivative, after continuity has been proved from the same identity.

Time regularity of the actual Sobolev pressure inverse, derived from its genuine resolvent.

@[instance_reducible]

noncomputable def EulerSobolevCoefficientPressure.sobolevEndNormedGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup (↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The inherited normed group of Sobolev endomorphisms, named to keep instance inference shallow.

Equations

• EulerSobolevCoefficientPressure.sobolevEndNormedGroup period q = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable def EulerSobolevCoefficientPressure.sobolevEndNormedSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ (↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The inherited real normed-space structure of Sobolev endomorphisms.

Equations

• EulerSobolevCoefficientPressure.sobolevEndNormedSpace period q = ContinuousLinearMap.toNormedSpace

theorem EulerSobolevCoefficientPressure.pressureSobolev_continuousAt (period : ℝ) [Fact (0 < period)] {α : Type u_1} [TopologicalSpace α] {q : ℕ} (A : α → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (s : α) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A s)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (s : α) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((A s).coefficient x) v) v) (t : α) (hM : ContinuousAt (fun (s : α) => coefficientSobolevOperator period (K s)) t) : ContinuousAt (fun (s : α) => pressureSobolevOperator period (K s) κ m c hc ⋯) t

Coefficient-multiplier continuity implies continuity of the actual pressure operator in Hq norm.

theorem EulerSobolevCoefficientPressure.projectedSource_continuousAt (period : ℝ) [Fact (0 < period)] {α : Type u_1} [TopologicalSpace α] {q : ℕ} (A : α → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (s : α) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A s)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (s : α) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((A s).coefficient x) v) v) (t : α) (hM : ContinuousAt (fun (s : α) => coefficientSobolevOperator period (K s)) t) : ContinuousAt (fun (s : α) => projectedSourceOperator period (K s) κ m c hc ⋯) t

The actual pressure-corrected source operator is continuous whenever the coefficient multiplier is continuous.

theorem EulerSobolevCoefficientPressure.pressureSobolev_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (s : ℝ) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A s)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (s : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((A s).coefficient x) v) v) (t : ℝ) (M' : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hM : HasDerivAt (fun (s : ℝ) => coefficientSobolevOperator period (K s)) M' t) : HasDerivAt (fun (s : ℝ) => pressureSobolevOperator period (K s) κ m c hc ⋯) (-pressureSobolevOperator period (K t) κ m c hc ⋯ ∘SL M' ∘SL pressureSobolevOperator period (K t) κ m c hc ⋯) t

Differentiating the genuine resolvent gives the actual Hq pressure derivative −P M′ P.

theorem EulerSobolevCoefficientPressure.projectedSource_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (A : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (s : ℝ) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A s)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (s : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((A s).coefficient x) v) v) (t : ℝ) (M' : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hM : HasDerivAt (fun (s : ℝ) => coefficientSobolevOperator period (K s)) M' t) : HasDerivAt (fun (s : ℝ) => projectedSourceOperator period (K s) κ m c hc ⋯) (-(M' ∘SL pressureSobolevOperator period (K t) κ m c hc ⋯ + coefficientSobolevOperator period (K t) ∘SL (-pressureSobolevOperator period (K t) κ m c hc ⋯ ∘SL M' ∘SL pressureSobolevOperator period (K t) κ m c hc ⋯))) t

The complete Sobolev pressure-corrected source has the actual derivative obtained by the product rule.

theorem EulerCorrectionOperators.postcompose_continuous {X : Type u_1} {Y : Type u_2} {T : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [TopologicalSpace T] (A : T → Y →L[ℝ] Y) (hA : Continuous A) (B : X →L[ℝ] X →L[ℝ] Y) : Continuous fun (t : T) => postcompose (A t) B

Continuous coefficient multipliers act continuously on any fixed genuine bilinear product.

@[instance_reducible]

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

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

Equations

• EulerCorrectionOperators.timeSobolevGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCorrectionOperators.timeSobolevRealSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionOperators.timeSobolevBilinearGroup (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

• EulerCorrectionOperators.timeSobolevBilinearGroup period q = inferInstance

theorem EulerCorrectionOperators.algebraicBilinear_continuous {T : Type u_3} [TopologicalSpace T] (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (C : T → Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hC : ∀ (i : Fin 3), Continuous fun (t : T) => C t i) : Continuous fun (t : T) => algebraicBilinear period hq (C t)

Time continuity of the actual order-zero quadratic terms.

theorem EulerCorrectionOperators.eulerBilinear_continuous {T : Type u_3} [TopologicalSpace T] (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C : T → Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hC : ∀ (i : Fin 3), Continuous fun (t : T) => C t i) : Continuous fun (t : T) => eulerBilinear period hq L hL (C t)

Time continuity of the literal transport-plus-algebraic Euler nonlinearity.

noncomputable def EulerCorrectionOperators.pressureProjectionPath {T : Type u_3} [TopologicalSpace T] (period : ℝ) [Fact (0 < period)] {q : ℕ} (G : T → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (t : T) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (G t)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : T) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G t).coefficient x) v) v) (hG : Continuous fun (t : T) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K t)) : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The actual Sobolev pressure projection as a continuous coefficient path.

Equations

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

noncomputable def EulerCorrectionOperators.correctionCoefficients {T : Type u_3} [TopologicalSpace T] (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (G : T → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (t : T) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (G t)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : T) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G t).coefficient x) v) v) (hG : Continuous fun (t : T) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K t)) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C₀ : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (C : Fin 3 → C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (z : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (r : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : EulerQuadraticSource.Coefficients T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Concrete coefficient data for equation (17): actual pressure, actual transport, and actual order-zero coefficient multipliers.

Equations

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

theorem EulerCorrectionOperators.correction_source_identity {T : Type u_3} [TopologicalSpace T] (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (G : T → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (t : T) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (G t)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : T) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G t).coefficient x) v) v) (hG : Continuous fun (t : T) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K t)) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C₀ : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (C : Fin 3 → C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (z : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (r : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (correctionCoefficients period hq G K κ m c hc hpos hG L hL C₀ C z r).apply t e = -(EulerSobolevCoefficientPressure.projectedSourceOperator period (K t) κ m c hc ⋯) (r t + (C₀ t) ((EulerCylinderSobolevSpace.truncateOperator period q) e) + ((eulerBilinear period hq L hL fun (i : Fin 3) => (C i) t) (z t + e)) (z t + e) - ((eulerBilinear period hq L hL fun (i : Fin 3) => (C i) t) (z t)) (z t))

The correction is exactly pressure applied to the residual and the nonlinear increment about z.

theorem EulerCorrectionOperators.correction_source_gradient_zero {T : Type u_3} [TopologicalSpace T] (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (G : T → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (t : T) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (G t)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : T) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G t).coefficient x) v) v) (hG : Continuous fun (t : T) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K t)) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C₀ : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (C : Fin 3 → C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (z : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (r : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : T) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period ((correctionCoefficients period hq G K κ m c hc hpos hG L hL C₀ C z r).apply t e)) = 0

The actual nonlinear correction source is divergence-free for every input.

The local quadratic heat construction preserves the actual lifted divergence constraint.

@[instance_reducible]

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

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

Equations

• EulerQuadraticSource.constraintSobolevGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerQuadraticSource.constraintSobolevSpace period q = inferInstance

theorem EulerQuadraticSource.exists_local_quadratic_divergenceFree (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (hu₀ : (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period u₀) = 0) (C : Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hC : ∀ (t : ↑(Set.Icc 0 S)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))), (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period (C.apply t u)) = 0) : ∃ (T : ℝ) (hT : 0 < T) (hTS : T ≤ S) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖u‖ ≤ ‖u₀‖ + 1 ∧ u ⟨0, ⋯⟩ = u₀ ∧ (∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) ∧ ∀ (t : ↑(Set.Icc 0 T)), u t = quadraticDuhamel period ν hν ⋯ hTS C u₀ u t

A local solution driven by the actual divergence-free projected source has zero lifted divergence at every time.

@[instance_reducible]

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

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

Equations

• EulerCorrectionOperators.dataSobolevGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCorrectionOperators.dataSobolevSpace period q = inferInstance

structure EulerCorrectionOperators.CoefficientPath (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : Type u_1) [TopologicalSpace T] : Type u_1

An actual smooth spatial coefficient with its genuine finite Sobolev jet and continuous time action.

• coefficient : T → EulerSpatialSobolevInverse.SmoothCoefficient period

  Coefficient of CoefficientPath, of type T → SmoothCoefficient period.

• jet (t : T) : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (self.coefficient t)

  Jet of CoefficientPath, of type ∀ t, CoefficientJet period standardDirection q (coefficient t).

• continuous : Continuous fun (t : T) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (self.jet t)

noncomputable def EulerCorrectionOperators.CoefficientPath.operatorPath (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (A : CoefficientPath period q T) : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The path acts by actual pointwise multiplication at each time.

Equations

• EulerCorrectionOperators.CoefficientPath.operatorPath period A = { toFun := fun (t : T) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (A.jet t), continuous_toFun := ⋯ }

structure EulerCorrectionOperators.CorrectionData (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : Type u_1) [TopologicalSpace T] : Type u_1

The concrete coefficient and approximate-solution data of the viscous Euler error equation.

• κ : ℝ

  Κ of CorrectionData, of type ℝ.

• direction : EulerLiftedGradientSpace.Vector3

  Direction of CorrectionData, of type Vector3.

• scale_bound : |self.κ| ≤ 1
• direction_bound : ‖self.direction‖ ≤ 1
• metric : CoefficientPath period q T

  Metric of CorrectionData, of type CoefficientPath period q T.

• coercivity : ℝ

  Coercivity of CorrectionData, of type ℝ.

• coercivity_pos : 0 < self.coercivity
• metric_pos (t : T) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3) : self.coercivity * ‖v‖ ^ 2 ≤ inner ℝ (((self.metric.coefficient t).coefficient x) v) v
• linear : CoefficientPath period q T

  Linear of CorrectionData, of type CoefficientPath period q T.

• quadratic : Fin 3 → CoefficientPath period q T

  Quadratic of CorrectionData, of type Fin 3 → CoefficientPath period q T.

• approximation : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))

  Approximation of CorrectionData, of type C(T, SobolevSpace period (q+1)).

• residual : C(T, ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

  Residual of CorrectionData, of type C(T, SobolevSpace period q).

noncomputable def EulerCorrectionOperators.CorrectionData.coefficients (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : CorrectionData period q T) (hq : 6 ≤ q) : EulerQuadraticSource.Coefficients T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The actual pressure-projected nonlinear correction source generated by the concrete data.

Equations

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

theorem EulerCorrectionOperators.CorrectionData.source_gradient_zero (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : Type u_1} [TopologicalSpace T] (D : CorrectionData period q T) (hq : 6 ≤ q) (t : T) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerLiftedGradientSpace.gradientProjection period D.κ D.direction) (EulerCylinderSobolevSpace.value period ((coefficients period D hq).apply t u)) = 0

The actual error source is exactly divergence-free; this property is derived from pressure coercivity.

theorem EulerCorrectionOperators.exists_local_euler_correction (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (D : CorrectionData period q ↑(Set.Icc 0 S)) : ∃ (T : ℝ) (hT : 0 < T) (hTS : T ≤ S) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖e‖ ≤ 1 ∧ e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ ∀ (t : ↑(Set.Icc 0 T)), e t = EulerQuadraticSource.quadraticDuhamel period ν hν ⋯ hTS (CorrectionData.coefficients period D hq) 0 e t

The actual Euler correction equation has a positive-time mild solution with zero initial error and the genuine divergence constraint.