Actual finite energy families of all required derivative words and their strong weighted limits.

The actual lifted gradient and divergence constraints persist under every available strong derivative word.

noncomputable def EulerSobolevWordConstraints.sobolevGradientProjection (period : ℝ) [Fact (0 < period)] (q : ℕ) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The genuine orthogonal lifted gradient projection acting on the complete Sobolev scale.

Equations

• EulerSobolevWordConstraints.sobolevGradientProjection period q κ m = EulerCylinderSobolevSpace.liftOperator period q (EulerLiftedGradientSpace.gradientProjection period κ m) ⋯

theorem EulerSobolevWordConstraints.sobolevGradientProjection_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((sobolevGradientProjection period q κ m) u) = (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.value period u)

Its zeroth coordinate is exactly the original L² orthogonal projection.

theorem EulerSobolevWordConstraints.sobolevGradientProjection_word (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hn : n ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (w : Fin n → Fin 4) : EulerCylinderSobolevSpace.word period ((sobolevGradientProjection period q κ m) u) hn w = (EulerLiftedGradientSpace.gradientProjection period κ m) (EulerCylinderSobolevSpace.word period u hn w)

The actual Sobolev gradient projection acts on each genuine derivative coordinate.

theorem EulerSobolevWordConstraints.sobolevGradientProjection_zero (period : ℝ) [Fact (0 < period)] {q : ℕ} (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) : (sobolevGradientProjection period q κ m) u = 0

A divergence-free Sobolev field has zero Sobolev gradient projection, including all derivatives.

theorem EulerSobolevWordConstraints.word_divergenceFree (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hn : n ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (w : Fin n → Fin 4) : EulerCylinderSobolevSpace.word period u hn w ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

Every actual derivative word of a divergence-free field remains divergence-free.

theorem EulerSobolevWordConstraints.sobolevGradientProjection_self (period : ℝ) [Fact (0 < period)] {q : ℕ} (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.gradientSpace period κ m) : (sobolevGradientProjection period q κ m) u = u

A genuine gradient field is fixed by the Sobolev gradient projection.

theorem EulerSobolevWordConstraints.word_gradient (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hn : n ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (w : Fin n → Fin 4) : EulerCylinderSobolevSpace.word period u hn w ∈ EulerLiftedGradientSpace.gradientSpace period κ m

Every actual derivative word of a lifted pressure gradient remains in the lifted gradient space.

Every energy-order word of the actual heat-regularized mild solution obeys its genuine L² differential equation.

noncomputable def EulerRegularizedWordEquation.regularizedWordBlock (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)

A genuinely regularized derivative word as a bounded map from the source Sobolev space into H².

Equations

• EulerRegularizedWordEquation.regularizedWordBlock period hm n w = EulerMildTopWord.boundedWordBlock period 2 m ⋯ w ∘SL EulerHeatRegularizedPaths.heatRegularizer period q n

theorem EulerRegularizedWordEquation.regularizedWordBlock_heat (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (regularizedWordBlock period hm n w) ((EulerSobolevHeat.heatOperator period q v) u) = (EulerSobolevHeat.heatOperator period 2 v) ((regularizedWordBlock period hm n w) u)

Every concrete regularized word block commutes with the actual heat semigroup.

theorem EulerRegularizedWordEquation.regularizedWordBlock_value (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : EulerCylinderSobolevSpace.value period ((regularizedWordBlock period hm n w) ((EulerCylinderSobolevSpace.truncateOperator period q) u)) = (EulerGaussianCylinderHeat.cylinderHeat period (EulerHeatRegularizedPaths.regularizerVariance n)) (EulerCylinderSobolevSpace.word period u hm w)

Its underlying field is exactly heat applied to the actual energy-order derivative of the unregularized state.

noncomputable def EulerRegularizedWordEquation.regularizedWordPath (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))

The actual regularized energy-order word path.

Equations

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

theorem EulerRegularizedWordEquation.laplacianEvaluation_two (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) : (EulerSobolevHeatGenerator.laplacianEvaluation period 2 ⋯) u = EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period u)

At depth two the actual Laplacian evaluation is exactly the original genuine jet Laplacian.

theorem EulerRegularizedWordEquation.regularized_word_hasDerivAt (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT (regularizedWordPath period hm n w T u) r)) (ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period ((regularizedWordPath period hm n w T u) ⟨t, ⋯⟩)) + EulerCylinderSobolevSpace.value period ((regularizedWordBlock period hm n w) (f ⟨t, ⋯⟩))) t

Every regularized word at the full solution energy order satisfies the actual time PDE, with no top-order differentiability premise.

theorem EulerRegularizedWordEquation.regularized_word_divergenceFree (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (κ : ℝ) (m₀ : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (hu : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m₀) : EulerCylinderSobolevSpace.value period ((regularizedWordBlock period hm n w) ((EulerCylinderSobolevSpace.truncateOperator period q) u)) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m₀

Actual energy-order word regularization preserves lifted divergence-freeness.

Concrete forcing for the regularized word PDE and its strong energy-order time limit.

Strong L²-time convergence of actual energy-order regularized state, source, and pressure words.

Exact bounded observations of genuine higher-order Bochner representatives.

theorem EulerTimeLp.compLpL_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (T : ℝ) (A : E →L[ℝ] F) (B : F →L[ℝ] G) (u : ↥(TimeLp T E)) : (ContinuousLinearMap.compLpL 2 (timeMeasure T) B) ((ContinuousLinearMap.compLpL 2 (timeMeasure T) A) u) = (ContinuousLinearMap.compLpL 2 (timeMeasure T) (B ∘SL A)) u

Composition of actual bounded spatial maps is composition of their genuine Bochner actions.

theorem EulerTimeLp.observation_time_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (D : F →L[ℝ] G) (W : E →L[ℝ] G) (hDA : ∀ (x : E), D (A x) = W x) (u : ↥(TimeLp T E)) (f : C(↑(Set.Icc 0 T), F)) (hf : (fun (t : ℝ) => A (↑↑u t)) =ᵐ[timeMeasure T] EulerVolterraConvolution.extendPath T hT f) : pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) D) f) = (ContinuousLinearMap.compLpL 2 (timeMeasure T) W) u

A continuous lower-order representative and an actual higher-order time field have identical bounded observations when the operators agree on restriction.

theorem EulerRegularizedWordTime.field_heat_timeLp_tendsto (period : ℝ) [Fact (0 < period)] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥(EulerLiftedGradientSpace.LiftL2 period))) : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerGaussianCylinderHeat.cylinderHeat period (EulerHeatRegularizedPaths.regularizerVariance n))) u) Filter.atTop (nhds u)

The actual L² cylinder heat approximation converges on every Bochner L² time field.

noncomputable def EulerRegularizedWordTime.sourceWordPath (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

An actual regularized energy-order derivative of a continuous low-order source, as an L² time path.

Equations

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

theorem EulerRegularizedWordTime.sourceWordPath_time_eq (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT f) : EulerTimeLp.pathLp T hT (sourceWordPath period hm n w T f) = (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerGaussianCylinderHeat.cylinderHeat period (EulerHeatRegularizedPaths.regularizerVariance n))) ((ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerCylinderSobolevSpace.wordOperator period ⟨⟨m, ⋯⟩, w⟩)) F)

Source smoothing agrees exactly with heat on a genuinely higher-order Bochner representative, whenever their lower fields agree almost everywhere.

theorem EulerRegularizedWordTime.sourceWordPath_time_tendsto (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (w : Fin m → Fin 4) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT f) : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (sourceWordPath period hm n w T f)) Filter.atTop (nhds ((ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerCylinderSobolevSpace.wordOperator period ⟨⟨m, ⋯⟩, w⟩)) F))

The actual regularized source words converge strongly at the full energy order using the proved higher time regularity.

theorem EulerRegularizedWordTime.regularizedWordPath_first_eq (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 1)) (EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerMildTopWord.boundedWordBlock period 1 m ⋯ w)) (EulerRegularizedTopBlocks.maximalApproximation period q T n u)

The H¹ restriction of a regularized energy word is literally the corresponding block of the full maximal-regularity approximation.

theorem EulerRegularizedWordTime.regularizedWordPath_first_tendsto (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (w : Fin m → Fin 4) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)) : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 1)) (EulerRegularizedWordEquation.regularizedWordPath period hm n w T u))) Filter.atTop (nhds ((ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerMildTopWord.boundedWordBlock period 1 m ⋯ w)) U))

Genuine maximal regularity gives strong H¹ time convergence for every full energy-order derivative word.

Continuous time-path application and its exact Bochner compatibility.

noncomputable def EulerTimeLp.timePathApply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : C(↑(Set.Icc 0 T), E)) : C(↑(Set.Icc 0 T), F)

The actual pointwise action of a continuous operator path on a continuous field path.

Equations

• EulerTimeLp.timePathApply T A u = { toFun := fun (t : ↑(Set.Icc 0 T)) => (A t) (u t), continuous_toFun := ⋯ }

theorem EulerTimeLp.pathLp_timePathApply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : C(↑(Set.Icc 0 T), E)) : pathLp T hT (timePathApply T A u) = (timeMultiplier T hT A) (pathLp T hT u)

The actual continuous-path action has exactly its Bochner multiplier value.

theorem EulerTimeLp.timePathApply_tendsto {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), E →L[ℝ] F)) (u : ℕ → C(↑(Set.Icc 0 T), E)) (U : ↥(TimeLp T E)) (hu : Filter.Tendsto (fun (n : ℕ) => pathLp T hT (u n)) Filter.atTop (nhds U)) : Filter.Tendsto (fun (n : ℕ) => pathLp T hT (timePathApply T A (u n))) Filter.atTop (nhds ((timeMultiplier T hT A) U))

Strong L² convergence of actual continuous field paths survives a fixed continuous time-dependent operator.

noncomputable def EulerRegularizedForcingWord.forcingWordPath (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The actual transport-pressure forcing in the regularized energy-word PDE.

Equations

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

theorem EulerRegularizedForcingWord.forcingWordPath_apply (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ↑(Set.Icc 0 T)) : (forcingWordPath period hm n w T A G u f p) t = EulerCylinderSobolevSpace.value period ((EulerRegularizedWordEquation.regularizedWordBlock period hm n w) (f t)) + (A t) ((EulerCylinderSobolevSpace.truncateOperator period 1) ((EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) t)) + (G t) (EulerCylinderSobolevSpace.value period ((EulerRegularizedWordEquation.regularizedWordBlock period hm n w) (p t)))

The regularized forcing has its literal source-plus-transport-plus-pressure value.

theorem EulerRegularizedForcingWord.forcingWordPath_equation (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T ν : ℝ) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ↑(Set.Icc 0 T)) : ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period ((EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) t)) + EulerCylinderSobolevSpace.value period ((EulerRegularizedWordEquation.regularizedWordBlock period hm n w) (f t)) + (A t) ((EulerCylinderSobolevSpace.truncateOperator period 1) ((EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) t)) + (G t) (EulerCylinderSobolevSpace.value period ((EulerRegularizedWordEquation.regularizedWordBlock period hm n w) (p t))) = (forcingWordPath period hm n w T A G u f p) t + ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period ((EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) t))

The source-plus-transport-plus-pressure definition gives the exact regularized word equation.

theorem EulerRegularizedForcingWord.regularized_word_hasDerivAt_clamped (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT (EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) r)) (ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period (EulerVolterraConvolution.extendPath T hT (EulerRegularizedWordEquation.regularizedWordPath period hm n w T u) t)) + EulerVolterraConvolution.extendPath T hT (EulerRegularizedWordTime.sourceWordPath period hm n w T f) t) t

The full energy-order regularized word has the actual clamped-path heat derivative at each interior time.

noncomputable def EulerRegularizedForcingWord.forcingWordTime (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (w : Fin m → Fin 4) (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : ↥(EulerTimeLp.TimeLp T ↥(EulerLiftedGradientSpace.LiftL2 period))

The literal forcing obtained from full energy-order source, state, and pressure time fields.

Equations

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

theorem EulerRegularizedForcingWord.forcingWordPath_time_tendsto (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (w : Fin m → Fin 4) (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)) (hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT f) (hP : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑P t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT p) : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (forcingWordPath period hm n w T A G u f p)) Filter.atTop (nhds (forcingWordTime period hm w T hT A G U F P))

The concrete regularized PDE forcing converges strongly at the full energy order by maximal regularity and the actual higher-order source/pressure representatives.

The actual energy-order regularized words converge uniformly in time and preserve pressure closedness.

noncomputable def EulerRegularizedWordEquation.energyWordPath (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (w : Fin m → Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))

The unregularized energy-order word retained as an actual H⁰ time path.

Equations

• EulerRegularizedWordEquation.energyWordPath period hm w T u = EulerMildWordEquation.mapPath period T (EulerMildTopWord.boundedWordBlock period 0 m ⋯ w) u

theorem EulerRegularizedWordEquation.regularizedWordPath_heat_value (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 2)) (regularizedWordPath period hm n w T u) = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 0)) (EulerHeatRegularizedPaths.pathHeat period 0 T (EulerHeatRegularizedPaths.regularizerVariance n) (energyWordPath period hm w T u))

The actual regularized energy word is exactly the L² value of its genuine H⁰ heat path.

theorem EulerRegularizedWordEquation.regularizedWordPath_value_tendsto (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (w : Fin m → Fin 4) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 2)) (regularizedWordPath period hm n w T u)) Filter.atTop (nhds ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 0)) (energyWordPath period hm w T u)))

Every actual energy-order word of the regularized mild solution converges uniformly in L² time paths, including the top order.

theorem EulerRegularizedWordEquation.cylinderHeat_gradient (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (v : NNReal) (p : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) : (EulerGaussianCylinderHeat.cylinderHeat period v) p ∈ EulerLiftedGradientSpace.gradientSpace period κ m

Genuine heat smoothing preserves the lifted gradient subspace.

theorem EulerRegularizedWordEquation.regularizedWordBlock_gradient (period : ℝ) [Fact (0 < period)] {q m : ℕ} (hm : m ≤ q + 1) (n : ℕ) (w : Fin m → Fin 4) (κ : ℝ) (m₀ : EulerLiftedGradientSpace.Vector3) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hp : EulerCylinderSobolevSpace.value period p ∈ EulerLiftedGradientSpace.gradientSpace period κ m₀) : EulerCylinderSobolevSpace.value period ((regularizedWordBlock period hm n w) p) ∈ EulerLiftedGradientSpace.gradientSpace period κ m₀

Every regularized pressure word stays in the actual lifted gradient space, without assuming an unregularized derivative of that order.

Actual finite families of continuous and Bochner time fields, with exact norm-topology compatibility.

def EulerTimeFamily.familyPath {I : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (T : ℝ) (u : I → C(↑(Set.Icc 0 T), E)) : C(↑(Set.Icc 0 T), I → E)

A finite family of continuous time paths as the actual continuous family-valued path.

Equations

• EulerTimeFamily.familyPath T u = { toFun := fun (t : ↑(Set.Icc 0 T)) (i : I) => (u i) t, continuous_toFun := ⋯ }

theorem EulerTimeFamily.familyPath_continuous {I : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (T : ℝ) : Continuous (familyPath T)

Bundling actual finite continuous paths is continuous in their uniform topologies.

theorem EulerTimeFamily.familyPath_tendsto {I : Type u_1} {E : Type u_2} [NormedAddCommGroup E] (T : ℝ) (u : ℕ → I → C(↑(Set.Icc 0 T), E)) (v : I → C(↑(Set.Icc 0 T), E)) (hu : ∀ (i : I), Filter.Tendsto (fun (n : ℕ) => u n i) Filter.atTop (nhds (v i))) : Filter.Tendsto (fun (n : ℕ) => familyPath T (u n)) Filter.atTop (nhds (familyPath T v))

Componentwise uniform path convergence gives uniform convergence of the actual finite family.

noncomputable def EulerTimeFamily.familyTime {I : Type u_1} {E : Type u_2} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : I → ↥(EulerTimeLp.TimeLp T E)) : ↥(EulerTimeLp.TimeLp T (I → E))

A finite family of actual Bochner fields, constructed by the genuine bounded coordinate injections.

Equations

• EulerTimeFamily.familyTime T u = ∑ i : I, (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (ContinuousLinearMap.single ℝ (fun (x : I) => E) i)) (u i)

theorem EulerTimeFamily.familyTime_ae {I : Type u_1} {E : Type u_2} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : I → ↥(EulerTimeLp.TimeLp T E)) : ↑↑(familyTime T u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) (i : I) => ↑↑(u i) t

The Bochner finite-family construction has exactly the componentwise representative almost everywhere.

theorem EulerTimeFamily.familyTime_tendsto {I : Type u_1} {E : Type u_2} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ℕ → I → ↥(EulerTimeLp.TimeLp T E)) (v : I → ↥(EulerTimeLp.TimeLp T E)) (hu : ∀ (i : I), Filter.Tendsto (fun (n : ℕ) => u n i) Filter.atTop (nhds (v i))) : Filter.Tendsto (fun (n : ℕ) => familyTime T (u n)) Filter.atTop (nhds (familyTime T v))

Strong convergence of each actual component gives strong convergence of the full finite Bochner family.

theorem EulerTimeFamily.familyTime_pathLp {I : Type u_1} {E : Type u_2} [Fintype I] [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : I → C(↑(Set.Icc 0 T), E)) : (familyTime T fun (i : I) => EulerTimeLp.pathLp T hT (u i)) = EulerTimeLp.pathLp T hT (familyPath T u)

Bundling continuous paths and passing to genuine Bochner classes commute exactly.

noncomputable def EulerRegularizedEnergyFamily.regularizedFamily (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (n : ℕ) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (i : α) : C(↑(Set.Icc 0 T), β → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))

A finite actual family of energy-order heat-regularized Sobolev word paths.

Equations

• EulerRegularizedEnergyFamily.regularizedFamily period d w hd n T u i = EulerTimeFamily.familyPath T fun (j : β) => EulerRegularizedWordEquation.regularizedWordPath period ⋯ n (w i j) T u

noncomputable def EulerRegularizedEnergyFamily.regularizedValueFamily (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (n : ℕ) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (i : α) : C(↑(Set.Icc 0 T), β → ↥(EulerLiftedGradientSpace.LiftL2 period))

The genuine L² values of the regularized energy-word family.

Equations

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

noncomputable def EulerRegularizedEnergyFamily.energyValueFamily (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (i : α) : C(↑(Set.Icc 0 T), β → ↥(EulerLiftedGradientSpace.LiftL2 period))

The actual original energy-order derivative family as a continuous L² path.

Equations

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

theorem EulerRegularizedEnergyFamily.regularizedValueFamily_tendsto (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (i : α) : Filter.Tendsto (fun (n : ℕ) => regularizedValueFamily period d w hd n T u i) Filter.atTop (nhds (energyValueFamily period d w hd T u i))

Every actual finite family of regularized derivative values converges uniformly, including its top order.

noncomputable def EulerRegularizedEnergyFamily.regularizedForcingFamily (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (n : ℕ) (T : ℝ) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (i : α) : C(↑(Set.Icc 0 T), β → ↥(EulerLiftedGradientSpace.LiftL2 period))

The actual finite family of regularized forcing words in the differentiated PDE.

Equations

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

noncomputable def EulerRegularizedEnergyFamily.forcingFamilyTime (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype β] {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (i : α) : ↥(EulerTimeLp.TimeLp T (β → ↥(EulerLiftedGradientSpace.LiftL2 period)))

The limiting actual finite forcing family represented in Bochner L² time.

Equations

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

theorem EulerRegularizedEnergyFamily.regularizedForcingFamily_tendsto (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype β] {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)) (hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT f) (hP : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑P t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT p) (i : α) : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (regularizedForcingFamily period d w hd n T A G u f p i)) Filter.atTop (nhds (forcingFamilyTime period d w hd T hT A G U F P i))

Every actual finite forcing family converges strongly by the genuine word-level maximal regularity argument.

theorem EulerRegularizedEnergyFamily.regularizedWeightedForcing_tendsto (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (d : α → β → ℕ) (w : (i : α) → (j : β) → Fin (d i j) → Fin 4) (hd : ∀ (i : α) (j : β), d i j ≤ q + 1) (T : ℝ) (hT : 0 ≤ T) (weights : α → C(↑(Set.Icc 0 T), ℝ)) (A : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (f p : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)) (hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT f) (hP : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑P t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT p) : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerWeightedForcingTime.weightedForcingPath T weights (regularizedForcingFamily period d w hd n T A G u f p))) Filter.atTop (nhds (EulerWeightedForcingTime.weightedForcingTime T hT weights (forcingFamilyTime period d w hd T hT A G U F P)))

Computed weighted forcing paths converge to the actual weighted norm of the limiting PDE forcing family.