Actual energy-order Bochner representatives of the nonlinear correction source and pressure.

Exact restriction and time continuity of the actual order-zero correction source.

@[instance_reducible]

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

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

Equations

• EulerSobolevCorrectionCompatibility.correctionCompatGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSobolevCorrectionCompatibility.correctionCompatSpace period q = inferInstance

theorem EulerSobolevCorrectionCompatibility.restrict_algebraicAt (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 6 ≤ p) (hq : 6 ≤ q) (hqp : q ≤ p) (A : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (KP : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection p (A i)) (KQ : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A i)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) (EulerGevreyOrderZero.algebraicAt period hp (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KP i)) u v) = EulerGevreyOrderZero.algebraicAt period hq (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i)) ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) ((EulerCylinderSobolevSpace.restrictOperator period hqp) v)

The actual derivative-free Euler term restricts to the same lower-order field.

theorem EulerSobolevCorrectionCompatibility.restrict_backgroundDrift (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 6 ≤ p) (hq : 6 ≤ q) (hqp : q ≤ p) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period (p + 1))) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) (EulerGevreyOrderZero.backgroundDrift period hp L hL z e) = EulerGevreyOrderZero.backgroundDrift period hq L hL ((EulerCylinderSobolevSpace.restrictOperator period ⋯) z) ((EulerCylinderSobolevSpace.restrictOperator period hqp) e)

Background transport has precisely the same value on every compatible Sobolev level.

theorem EulerSobolevCorrectionCompatibility.restrict_orderZeroSource (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 6 ≤ p) (hq : 6 ≤ q) (hqp : q ≤ p) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (A0 : EulerSpatialSobolevInverse.SmoothCoefficient period) (KP0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection p A0) (KQ0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A0) (A : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (KP : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection p (A i)) (KQ : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A i)) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period (p + 1))) (r e : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) : (EulerCylinderSobolevSpace.restrictOperator period hqp) (EulerGevreyOrderZero.orderZeroSource period hp L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period KP0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KP i)) z r e) = EulerGevreyOrderZero.orderZeroSource period hq L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period KQ0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i)) ((EulerCylinderSobolevSpace.restrictOperator period ⋯) z) ((EulerCylinderSobolevSpace.restrictOperator period hqp) r) ((EulerCylinderSobolevSpace.restrictOperator period hqp) e)

The full actual order-zero source agrees exactly with its lower-order construction.

theorem EulerSobolevCorrectionCompatibility.algebraicAt_continuous (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {T : Type u_1} [TopologicalSpace T] (C : T → Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (hC : ∀ (i : Fin 3), Continuous fun (t : T) => C t i) (u v : T → ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (hu : Continuous u) (hv : Continuous v) : Continuous fun (t : T) => EulerGevreyOrderZero.algebraicAt period hs (C t) (u t) (v t)

A continuous coefficient and two continuous energy-order paths give a continuous actual algebraic term.

theorem EulerSobolevCorrectionCompatibility.orderZeroSource_continuous (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {T : Type u_1} [TopologicalSpace T] (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : T → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (hC0 : Continuous C0) (C : T → Fin 3 → ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (hC : ∀ (i : Fin 3), Continuous fun (t : T) => C t i) (z : T → ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r e : T → ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (hz : Continuous z) (hr : Continuous r) (he : Continuous e) : Continuous fun (t : T) => EulerGevreyOrderZero.orderZeroSource period hs L hL (C0 t) (C t) (z t) (r t) (e t)

The actual order-zero source is continuous at the energy Sobolev level, without an additional error derivative.

Strong actual heat approximation and time-dependent operator commutators in Bochner Sobolev spaces.

theorem EulerSobolevTimeRegularization.heat_timeLp_tendsto (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period q (EulerHeatRegularizedPaths.regularizerVariance n))) u) Filter.atTop (nhds u)

The genuine Sobolev heat regularizations converge strongly on every Bochner L² time field.

theorem EulerSobolevTimeRegularization.heat_time_commutator_tendsto (period : ℝ) [Fact (0 < period)] (p q : ℕ) (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period p))) (u : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : Filter.Tendsto (fun (n : ℕ) => (EulerTimeLp.timeMultiplier T hT A) ((ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period q (EulerHeatRegularizedPaths.regularizerVariance n))) u) - (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period p (EulerHeatRegularizedPaths.regularizerVariance n))) ((EulerTimeLp.timeMultiplier T hT A) u)) Filter.atTop (nhds 0)

Actual heat approximation commutes asymptotically with every continuous bounded time-dependent Sobolev operator.

theorem EulerSobolevTimeRegularization.heat_time_commutator_norm_tendsto (period : ℝ) [Fact (0 < period)] (p q : ℕ) (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period p))) (u : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : Filter.Tendsto (fun (n : ℕ) => ‖(EulerTimeLp.timeMultiplier T hT A) ((ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period q (EulerHeatRegularizedPaths.regularizerVariance n))) u) - (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period p (EulerHeatRegularizedPaths.regularizerVariance n))) ((EulerTimeLp.timeMultiplier T hT A) u)‖) Filter.atTop (nhds 0)

The actual heat commutator vanishes in the full L² time norm.

Actual derivative-losing transport on continuous coefficients and square-integrable higher Sobolev states.

@[instance_reducible]

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

A named local normed-group instance for the actual Sobolev scale.

Equations

• EulerTimeSobolevTransport.transportTimeGroup period q = inferInstance

@[instance_reducible]

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

A named local real normed-space instance for the actual Sobolev scale.

Equations

• EulerTimeSobolevTransport.transportTimeSpace period q = inferInstance

noncomputable def EulerTimeSobolevTransport.transportPath (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s))

A continuous actual velocity path gives a continuous path of asymmetric transport operators.

Equations

• EulerTimeSobolevTransport.transportPath period hs L hL T u = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerAsymmetricTransport.asymmetricTransport period hs L hL)) u

noncomputable def EulerTimeSobolevTransport.transportTime (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (v : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))

Actual nonlinear transport of a higher Sobolev time field belongs to the full energy-order Bochner space.

Equations

• EulerTimeSobolevTransport.transportTime period hs L hL T hT u v = (EulerTimeLp.timeMultiplier T hT (EulerTimeSobolevTransport.transportPath period hs L hL T u)) v

theorem EulerTimeSobolevTransport.transportTime_ae (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (v : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) : ↑↑(transportTime period hs L hL T hT u v) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => ((EulerAsymmetricTransport.asymmetricTransport period hs L hL) (EulerVolterraConvolution.extendPath T hT u t)) (↑↑v t)

The actual Bochner transport is literal asymmetric Sobolev transport almost everywhere in time.

theorem EulerTimeSobolevTransport.transport_regularization_commutator (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (v : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) : Filter.Tendsto (fun (n : ℕ) => transportTime period hs L hL T hT u ((ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period (s + 1) (EulerHeatRegularizedPaths.regularizerVariance n))) v) - (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerSobolevHeat.heatOperator period s (EulerHeatRegularizedPaths.regularizerVariance n))) (transportTime period hs L hL T hT u v)) Filter.atTop (nhds 0)

Genuine heat smoothing and actual transport commute asymptotically in the energy-order L² time space.

@[instance_reducible]

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

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

Equations

• EulerTimeCorrectionSource.timeCorrectionGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerTimeCorrectionSource.timeCorrectionSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerTimeCorrectionSource.timeCorrectionPathAdd (period : ℝ) [Fact (0 < period)] (T : ℝ) (q : ℕ) : Add C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

Cache pointwise addition for the Sobolev paths used in correction sources.

Equations

• EulerTimeCorrectionSource.timeCorrectionPathAdd period T q = inferInstance

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

The actual order-zero source is a continuous path on the energy Sobolev level.

Equations

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

noncomputable def EulerTimeCorrectionSource.rawSourceTime (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (T : ℝ) (hT : 0 ≤ T) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (C : Fin 3 → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) (r e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))

The genuine energy-order raw correction source uses the constructed higher derivative only in its top transport.

Equations

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

theorem EulerTimeCorrectionSource.rawSourceTime_ae (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (T : ℝ) (hT : 0 ≤ T) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (C : Fin 3 → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) (r e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) : ↑↑(rawSourceTime period hs T hT L hL C0 C z r e U) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => ((EulerAsymmetricTransport.asymmetricTransport period hs L hL) ((EulerCylinderSobolevSpace.truncateOperator period s) (EulerVolterraConvolution.extendPath T hT z t) + EulerVolterraConvolution.extendPath T hT e t)) (↑↑U t) + EulerVolterraConvolution.extendPath T hT (orderZeroPath period hs T L hL C0 C z r e) t

The Bochner raw source has exactly the actual transport-plus-order-zero representative.

theorem EulerTimeCorrectionSource.restrict_transport_state (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (b e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (U : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (hU : (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) U = e) : (EulerCylinderSobolevSpace.truncateOperator period q) (((EulerAsymmetricTransport.asymmetricTransport period ⋯ L hL) b) U) = ((EulerSobolevTransport.transportBilinear period hq L hL) b) e

Restricting genuine asymmetric transport and its constructed state recovers the original lower-level nonlinearity.

theorem EulerTimeCorrectionSource.restrict_raw_source (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (A0 : EulerSpatialSobolevInverse.SmoothCoefficient period) (KP0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection (q + 1) A0) (KQ0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A0) (A : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (KP : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection (q + 1) (A i)) (KQ : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A i)) (z : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (r e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (U : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (hU : (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) U = e) : (EulerCylinderSobolevSpace.truncateOperator period q) (((EulerAsymmetricTransport.asymmetricTransport period ⋯ L hL) ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) z + e)) U + EulerGevreyOrderZero.orderZeroSource period ⋯ L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period KP0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KP i)) z r e) = ((EulerSobolevTransport.transportBilinear period hq L hL) ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) z + e)) e + EulerGevreyOrderZero.orderZeroSource period hq L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period KQ0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i)) ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) z) ((EulerCylinderSobolevSpace.truncateOperator period q) r) ((EulerCylinderSobolevSpace.truncateOperator period q) e)

The upgraded raw source restricts to the literal lower-order correction equation.

noncomputable def EulerTimeCorrectionSource.positivePressurePath (period : ℝ) [Fact (0 < period)] {s : ℕ} (T : ℝ) (G : EulerCorrectionOperators.CoefficientPath period s ↑(Set.Icc 0 T)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s))

The actual positive coercive pressure operator is a continuous energy-order time path.

Equations

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

noncomputable def EulerTimeCorrectionSource.pressureTime (period : ℝ) [Fact (0 < period)] {s : ℕ} (T : ℝ) (hT : 0 ≤ T) (G : EulerCorrectionOperators.CoefficientPath period s ↑(Set.Icc 0 T)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v) (F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))

The actual signed PDE pressure belongs to the full energy-order Bochner space.

Equations

• EulerTimeCorrectionSource.pressureTime period T hT G κ m c hc hpos F = -(EulerTimeLp.timeMultiplier T hT (EulerTimeCorrectionSource.positivePressurePath period T G κ m c hc hpos)) F

noncomputable def EulerTimeCorrectionSource.projectedTime (period : ℝ) [Fact (0 < period)] {s : ℕ} (T : ℝ) (hT : 0 ≤ T) (G : EulerCorrectionOperators.CoefficientPath period s ↑(Set.Icc 0 T)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v) (F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))

The actual projected mild forcing belongs to the full energy-order Bochner space.

Equations

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

theorem EulerTimeCorrectionSource.pressureTime_ae (period : ℝ) [Fact (0 < period)] {s : ℕ} (T : ℝ) (hT : 0 ≤ T) (G : EulerCorrectionOperators.CoefficientPath period s ↑(Set.Icc 0 T)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v) (F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : ↑↑(pressureTime period T hT G κ m c hc hpos F) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => -(EulerSobolevCoefficientPressure.pressureSobolevOperator period (G.jet (Set.projIcc 0 T hT t)) κ m c hc ⋯) (↑↑F t)

The signed pressure time field is the literal unique coercive pressure solve almost everywhere.

theorem EulerTimeCorrectionSource.projectedTime_ae (period : ℝ) [Fact (0 < period)] {s : ℕ} (T : ℝ) (hT : 0 ≤ T) (G : EulerCorrectionOperators.CoefficientPath period s ↑(Set.Icc 0 T)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v) (F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period s))) : ↑↑(projectedTime period T hT G κ m c hc hpos F) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => -(EulerSobolevCoefficientPressure.projectedSourceOperator period (G.jet (Set.projIcc 0 T hT t)) κ m c hc ⋯) (↑↑F t)

The projected time field is exactly the pressure-projected nonlinear mild forcing almost everywhere.