The literal transport and order-zero quadratic operators in the Euler correction equation.

noncomputable def EulerCorrectionOperators.postcompose {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (A : Y →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) : X →L[ℝ] X →L[ℝ] Y

Postcompose an actual continuous bilinear map by an actual bounded operator.

Equations

• EulerCorrectionOperators.postcompose A B = (ContinuousLinearMap.compL ℝ X Y Y) A ∘SL B

@[simp]

theorem EulerCorrectionOperators.postcompose_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (A : Y →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (u v : X) : ((postcompose A B) u) v = A ((B u) v)

noncomputable def EulerCorrectionOperators.linearize {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (B : X →L[ℝ] X →L[ℝ] Y) (C : X →L[ℝ] Y) (z : X) : X →L[ℝ] Y

Linearization of a quadratic term about the actual approximate solution.

Equations

• EulerCorrectionOperators.linearize B C z = B z + B.flip z + C

@[simp]

theorem EulerCorrectionOperators.linearize_apply {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (B : X →L[ℝ] X →L[ℝ] Y) (C : X →L[ℝ] Y) (z e : X) : (linearize B C z) e = (B z) e + (B e) z + C e

theorem EulerCorrectionOperators.quadratic_correction_identity {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (B : X →L[ℝ] X →L[ℝ] Y) (C : X →L[ℝ] Y) (z e : X) : C (z + e) + (B (z + e)) (z + e) - (C z + (B z) z) = (linearize B C z) e + (B e) e

The correction source is exactly the difference of the full quadratic equations.

theorem EulerCorrectionOperators.linearize_continuous {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {T : Type u_3} [TopologicalSpace T] (B : T → X →L[ℝ] X →L[ℝ] Y) (C : T → X →L[ℝ] Y) (z : T → X) (hB : Continuous B) (hC : Continuous C) (hz : Continuous z) : Continuous fun (t : T) => linearize (B t) (C t) (z t)

Continuous data give continuous linearized operators.

@[instance_reducible]

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

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

Equations

• EulerCorrectionOperators.sobolevGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCorrectionOperators.sobolevRealSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionOperators.sobolevBilinearGroup (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.sobolevBilinearGroup period q = inferInstance

noncomputable def EulerCorrectionOperators.coordinateProduct (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (i : Fin 3) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The actual derivative-free coordinate product on the input Sobolev level.

Equations

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

@[simp]

theorem EulerCorrectionOperators.coordinateProduct_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (i : Fin 3) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((coordinateProduct period hq i) u) v = EulerSobolevL2Product.productHq period hq (EulerVectorCylinder.coordinate 3 i) ⋯ ((EulerCylinderSobolevSpace.truncateOperator period q) u) ((EulerCylinderSobolevSpace.truncateOperator period q) v)

noncomputable def EulerCorrectionOperators.algebraicBilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The actual order-zero quadratic coefficient terms, Σ Cᵢ(uᵢ v).

Equations

• EulerCorrectionOperators.algebraicBilinear period hq C = ∑ i : Fin 3, EulerCorrectionOperators.postcompose (C i) (EulerCorrectionOperators.coordinateProduct period hq i)

theorem EulerCorrectionOperators.algebraicBilinear_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((algebraicBilinear period hq C) u) v = ∑ i : Fin 3, (C i) (((coordinateProduct period hq i) u) v)

noncomputable def EulerCorrectionOperators.eulerBilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C : Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The full bilinear nonlinearity of the transformed Euler equation.

Equations

• EulerCorrectionOperators.eulerBilinear period hq L hL C = EulerSobolevTransport.transportBilinear period hq L hL + EulerCorrectionOperators.algebraicBilinear period hq C

theorem EulerCorrectionOperators.algebraicBilinear_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (C i)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) : ↑↑(EulerCylinderSobolevSpace.value period (((algebraicBilinear period hq fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) u) v)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => ∑ i : Fin 3, (f x).ofLp i • ((C i).coefficient x) (g x)

Actual coefficient multiplication gives precisely the classical order-zero quadratic field.