Genuine all-finite-order maximal regularity for actual viscous cylinder mild solutions.

Actual maximal regularity at arbitrary finite Sobolev order via finitely many top derivative equations.

A genuine L²-time H² estimate for regularized heat solutions, with only L² forcing.

Genuine gradient energy and maximal-regularity estimates for smooth Sobolev heat solutions.

noncomputable def EulerHeatGradientEnergy.gradientEnergy (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : ℝ

The actual sum of the four first-derivative L² energies.

Equations

• EulerHeatGradientEnergy.gradientEnergy period u = ∑ i : Fin 4, ‖EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) u)‖ ^ 2

theorem EulerHeatGradientEnergy.gradientEnergy_nonneg (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : 0 ≤ gradientEnergy period u

Gradient energy is nonnegative.

theorem EulerHeatGradientEnergy.gradientEnergy_continuous (period : ℝ) [Fact (0 < period)] : Continuous (gradientEnergy period)

Gradient energy is a continuous function of the actual H¹ field.

theorem EulerHeatGradientEnergy.gradient_pairing (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : ∑ i : Fin 4, inner ℝ (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 1 i) u)) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) v)) = -inner ℝ ((EulerSobolevHeatGenerator.laplacianEvaluation period 2 gradient_pairing._proof_1) u) (EulerCylinderSobolevSpace.value period v)

Genuine strong-derivative integration by parts identifies the full gradient pairing with the Laplacian.

theorem EulerHeatGradientEnergy.gradient_energy_hasDerivAt (period : ℝ) [Fact (0 < period)] (u : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (t : ℝ) (hd : ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 1 i) (u s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) v)) t) : HasDerivAt (fun (s : ℝ) => gradientEnergy period ((EulerCylinderSobolevSpace.truncateOperator period 1) (u s))) (-2 * inner ℝ ((EulerSobolevHeatGenerator.laplacianEvaluation period 2 gradient_pairing._proof_1) (u t)) (EulerCylinderSobolevSpace.value period v)) t

Actual L² time derivatives of the first spatial derivatives determine the gradient-energy derivative.

theorem EulerHeatGradientEnergy.viscosity_young (ν x y : ℝ) (hν : 0 < ν) : 2 * x * y ≤ ν * x ^ 2 + ν⁻¹ * y ^ 2

The scalar Young bound with the exact viscosity scaling used by maximal regularity.

theorem EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt (period : ℝ) [Fact (0 < period)] (u : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (ν t : ℝ) (hd : ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (u s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (u t) + f))) t) : HasDerivAt (fun (s : ℝ) => gradientEnergy period ((EulerCylinderSobolevSpace.restrictOperator period heat_gradient_energy_hasDerivAt._proof_1) (u s))) (-2 * inner ℝ ((EulerSobolevHeatGenerator.laplacianEvaluation period 3 heat_gradient_energy_hasDerivAt._proof_2) (u t)) (ν • (EulerSobolevHeatGenerator.laplacianEvaluation period 3 heat_gradient_energy_hasDerivAt._proof_2) (u t) + EulerCylinderSobolevSpace.value period f)) t

The true heat gradient energy absorbs the source without differentiating the source in its bound.

theorem EulerHeatGradientEnergy.heat_gradient_energy_bound (period : ℝ) [Fact (0 < period)] (u : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (ν t : ℝ) (hν : 0 < ν) (hd : ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (u s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (u t) + f))) t) : deriv (fun (s : ℝ) => gradientEnergy period ((EulerCylinderSobolevSpace.restrictOperator period heat_gradient_energy_hasDerivAt._proof_1) (u s))) t ≤ -ν * ‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 heat_gradient_energy_hasDerivAt._proof_2) (u t)‖ ^ 2 + ν⁻¹ * ‖EulerCylinderSobolevSpace.value period f‖ ^ 2

The actual derivative of gradient energy controls the full L² Laplacian with no source derivative loss.

A genuine H² bound by H¹ and the cylinder Laplacian, used in strong maximal-regularity limits.

Exact L² Hessian coercivity from actual commuting strong derivatives.

noncomputable def EulerHeatGradientEnergy.hessianEnergy (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) : ℝ

The actual sum of all sixteen second-coordinate L² energies.

Equations

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

theorem EulerHeatGradientEnergy.hessian_row_identity (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (j : Fin 4) : ∑ i : Fin 4, ‖EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 1 i) ((EulerCylinderSobolevSpace.derivativeOperator period 2 j) u))‖ ^ 2 = -inner ℝ (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 j) u)) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 j) ((EulerSobolevLaplacian.laplacianOperator period 1) u)))

One row of the genuine Hessian energy is the corresponding gradient-Laplacian pairing.

theorem EulerHeatGradientEnergy.laplacian_gradient_pairing (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : ∑ j : Fin 4, inner ℝ (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 j) u)) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 j) ((EulerSobolevLaplacian.laplacianOperator period 1) u))) = -‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 heat_gradient_energy_hasDerivAt._proof_2) u‖ ^ 2

The sum of the genuine gradient-Laplacian pairings is minus the Laplacian norm squared.

theorem EulerHeatGradientEnergy.hessianEnergy_eq_laplacian (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : hessianEnergy period ((EulerCylinderSobolevSpace.truncateOperator period 2) u) = ‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 heat_gradient_energy_hasDerivAt._proof_2) u‖ ^ 2

All genuine second-coordinate derivatives are controlled exactly by the Laplacian.

theorem EulerSobolevEllipticBound.second_word_sq_le_hessian (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (w : Fin 2 → Fin 4) : ‖EulerCylinderSobolevSpace.word period u ⋯ w‖ ^ 2 ≤ EulerHeatGradientEnergy.hessianEnergy period u

Every actual second derivative word is bounded by the full genuine Hessian energy.

theorem EulerSobolevEllipticBound.H2_norm_sq_le (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) : ‖u‖ ^ 2 ≤ ‖(EulerCylinderSobolevSpace.truncateOperator period 1) u‖ ^ 2 + EulerHeatGradientEnergy.hessianEnergy period u

The complete H² norm is controlled by its H¹ restriction and the actual Hessian energy.

theorem EulerSobolevEllipticBound.H2_norm_sq_le_laplacian (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) : ‖(EulerCylinderSobolevSpace.truncateOperator period 2) u‖ ^ 2 ≤ ‖(EulerCylinderSobolevSpace.restrictOperator period EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_1) u‖ ^ 2 + ‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_2) u‖ ^ 2

The actual finite Sobolev elliptic estimate has no Fourier or inverse-operator assumption.

Integrated genuine heat gradient energy, with the source measured only in L².

theorem EulerHeatGradientEnergy.heat_laplacian_integral_bound (period : ℝ) [Fact (0 < period)] (u : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 3)) (f : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (ν s t : ℝ) (hν : 0 < ν) (hst : s ≤ t) (hu : ContinuousOn u (Set.Icc s t)) (hf : ContinuousOn f (Set.Icc s t)) (hd : ∀ r ∈ Set.Ioo s t, ∀ (i : Fin 4), HasDerivAt (fun (a : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (u a))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (u r) + f r))) r) : ν * ∫ (r : ℝ) in s..t, ‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 heat_gradient_energy_hasDerivAt._proof_2) (u r)‖ ^ 2 ≤ gradientEnergy period ((EulerCylinderSobolevSpace.restrictOperator period heat_gradient_energy_hasDerivAt._proof_1) (u s)) + ν⁻¹ * ∫ (r : ℝ) in s..t, ‖EulerCylinderSobolevSpace.value period (f r)‖ ^ 2

The actual integrated heat energy gains the full Laplacian in L² time without a source derivative in the bound.

theorem EulerHeatMaximalEstimate.gradientEnergy_bound (period : ℝ) [Fact (0 < period)] (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : EulerHeatGradientEnergy.gradientEnergy period u ≤ 4 * ‖u‖ ^ 2

The actual gradient energy is bounded by four times the complete H¹ norm squared.

theorem EulerHeatMaximalEstimate.integral_le_constant_add (f g : ℝ → ℝ) (c T : ℝ) (hT : 0 ≤ T) (hf : Continuous f) (hg : Continuous g) (hfg : ∀ t ∈ Set.Icc 0 T, f t ≤ c + g t) : ∫ (t : ℝ) in 0..T, f t ≤ T * c + ∫ (t : ℝ) in 0..T, g t

Integrating a continuous scalar upper bound by a constant plus another continuous function.

theorem EulerHeatMaximalEstimate.path_H2_point_bound (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) (t : ℝ) : ‖(EulerCylinderSobolevSpace.truncateOperator period 2) (EulerVolterraConvolution.extendPath T hT u t)‖ ^ 2 ≤ ‖(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_1)) u‖ ^ 2 + ‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_2) (EulerVolterraConvolution.extendPath T hT u t)‖ ^ 2

The actual pointwise elliptic estimate with the lower Sobolev path norm as a uniform bound.

theorem EulerHeatMaximalEstimate.time_H2_elliptic_bound (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) : ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 2)) u)‖ ^ 2 ≤ T * ‖(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_1)) u‖ ^ 2 + ∫ (t : ℝ) in 0..T, ‖(EulerSobolevHeatGenerator.laplacianEvaluation period 3 EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_2) (EulerVolterraConvolution.extendPath T hT u t)‖ ^ 2

The actual H² time norm is bounded by the H¹ path norm and the genuine Laplacian time integral.

theorem EulerHeatMaximalEstimate.heat_time_H2_bound (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hd : ∀ t ∈ Set.Ioo 0 T, ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT u s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT u t) + EulerVolterraConvolution.extendPath T hT f t))) t) : ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 2)) u)‖ ^ 2 ≤ (T + 4 * ν⁻¹) * ‖(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_1)) u‖ ^ 2 + ν⁻¹ ^ 2 * ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 1)) f)‖ ^ 2

The true heat PDE bounds the full L²-time H² norm by H¹ data and undifferentiated L² forcing.

Strong Cauchy convergence from a quadratic norm estimate in complete-space arguments.

theorem EulerQuadraticCauchy.transport_quadratic_bound {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] (a b : ℝ) (x x' : X) (y y' : Y) (z z' : Z) (hx : x = x') (hy : y = y') (hz : z = z') (h : ‖x‖ ^ 2 ≤ a * ‖y‖ ^ 2 + b * ‖z‖ ^ 2) : ‖x'‖ ^ 2 ≤ a * ‖y'‖ ^ 2 + b * ‖z'‖ ^ 2

Replacing three vectors by equal vectors preserves a quadratic norm estimate.

theorem EulerQuadraticCauchy.limit_quadratic_bound {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] (U : ℕ → X) (F : ℕ → Y) (V : ℕ → Z) (u : X) (f : Y) (v : Z) (a b : ℝ) (hu : Filter.Tendsto U Filter.atTop (nhds u)) (hf : Filter.Tendsto F Filter.atTop (nhds f)) (hv : Filter.Tendsto V Filter.atTop (nhds v)) (hb : ∀ (n : ℕ), ‖V n‖ ^ 2 ≤ a * ‖U n‖ ^ 2 + b * ‖F n‖ ^ 2) : ‖v‖ ^ 2 ≤ a * ‖u‖ ^ 2 + b * ‖f‖ ^ 2

A quadratic norm estimate passes to actual strong limits in three normed spaces.

theorem EulerQuadraticCauchy.cauchy_of_quadratic_bound {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] (U : ℕ → X) (F : ℕ → Y) (V : ℕ → Z) (a b : ℝ) (hu : CauchySeq U) (hf : CauchySeq F) (hb : ∀ (n m : ℕ), ‖V n - V m‖ ^ 2 ≤ a * ‖U n - U m‖ ^ 2 + b * ‖F n - F m‖ ^ 2) : CauchySeq V

A sequence whose squared differences are bounded by two Cauchy-sequence differences is Cauchy.

Strong L²-time H² Cauchy convergence from genuine heat energy, avoiding weak compactness.

@[instance_reducible]

noncomputable def EulerHeatMaximalCauchy.instSobolevPathSub (period : ℝ) [Fact (0 < period)] (T : ℝ) (k : ℕ) : Sub C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period k))

Cache pointwise subtraction for the Sobolev paths used in difference estimates.

Equations

• EulerHeatMaximalCauchy.instSobolevPathSub period T k = inferInstance

@[instance_reducible]

noncomputable def EulerHeatMaximalCauchy.instSobolevScalarAction (period : ℝ) [Fact (0 < period)] (k : ℕ) : SMul ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period k)

Cache the scalar action used by the Sobolev heat equations.

Equations

• EulerHeatMaximalCauchy.instSobolevScalarAction period k = inferInstance

theorem EulerHeatMaximalCauchy.linear_heat_rhs_sub {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (L : Y →L[ℝ] Z) (A : X →L[ℝ] Y) (ν : ℝ) (u v : X) (f g : Y) : L (ν • A (u - v) + (f - g)) = L (ν • A u + f) - L (ν • A v + g)

A bounded linear observation preserves the difference form of the forced heat right hand side.

theorem EulerHeatMaximalCauchy.first_derivative_difference (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) (f g : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (t : ℝ) (i : Fin 4) (hu : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT u s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT u t) + EulerVolterraConvolution.extendPath T hT f t))) t) (hv : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT v s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT v t) + EulerVolterraConvolution.extendPath T hT g t))) t) : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT (u - v) s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT (u - v) t) + EulerVolterraConvolution.extendPath T hT (f - g) t))) t

The difference of two actual differentiated heat equations is the same linear equation with difference source.

noncomputable def EulerHeatMaximalCauchy.lowerPath (period : ℝ) [Fact (0 < period)] (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))

Restrict a regularized path to its actual H¹ topology.

Equations

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

noncomputable def EulerHeatMaximalCauchy.higherTime (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))

Embed the actual H² restriction of a regularized path into L² time.

Equations

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

noncomputable def EulerHeatMaximalCauchy.sourceTime (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) : ↥(EulerTimeLp.TimeLp T ↥(EulerLiftedGradientSpace.LiftL2 period))

Embed the actual undifferentiated forcing into L² time.

Equations

• EulerHeatMaximalCauchy.sourceTime period T hT f = EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 1)) f)

theorem EulerHeatMaximalCauchy.lowerPath_sub (period : ℝ) [Fact (0 < period)] (T : ℝ) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) : lowerPath period T (u - v) = lowerPath period T u - lowerPath period T v

The lower path restriction preserves differences.

theorem EulerHeatMaximalCauchy.higherTime_sub (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) : higherTime period T hT (u - v) = higherTime period T hT u - higherTime period T hT v

The actual higher time embedding preserves differences.

theorem EulerHeatMaximalCauchy.sourceTime_sub (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (f g : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) : sourceTime period T hT (f - g) = sourceTime period T hT f - sourceTime period T hT g

The actual source time embedding preserves differences.

theorem EulerHeatMaximalCauchy.heat_H2_difference_bound (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u v : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) (f g : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hd : ∀ t ∈ Set.Ioo 0 T, ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT (u - v) s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT (u - v) t) + EulerVolterraConvolution.extendPath T hT (f - g) t))) t) : ‖higherTime period T hT u - higherTime period T hT v‖ ^ 2 ≤ (T + 4 * ν⁻¹) * ‖lowerPath period T u - lowerPath period T v‖ ^ 2 + ν⁻¹ ^ 2 * ‖sourceTime period T hT f - sourceTime period T hT g‖ ^ 2

The true linear heat equation controls actual H² time differences by lower path and source differences.

theorem EulerHeatMaximalCauchy.heat_H2_cauchy (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) (f : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hd : ∀ (n : ℕ), ∀ t ∈ Set.Ioo 0 T, ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT (u n) s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT (u n) t) + EulerVolterraConvolution.extendPath T hT (f n) t))) t) (hu : CauchySeq fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_1)) (u n)) (hf : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 1)) (f n))) : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 2)) (u n))

Actual regularized heat solutions which converge in H¹ and have Cauchy L² sources converge strongly in L² time with two full derivatives.

theorem EulerHeatMaximalCauchy.exists_heat_H2_limit (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 3))) (f : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hd : ∀ (n : ℕ), ∀ t ∈ Set.Ioo 0 T, ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT (u n) s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT (u n) t) + EulerVolterraConvolution.extendPath T hT (f n) t))) t) (hu : CauchySeq fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period EulerHeatGradientEnergy.heat_gradient_energy_hasDerivAt._proof_1)) (u n)) (hf : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 1)) (f n))) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))), Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 2)) (u n))) Filter.atTop (nhds U)

Completeness constructs a genuine Bochner L²-time H² limit of the regularized heat solutions.

Actual higher Sobolev norms controlled by lower norms and finitely many top derivative blocks.

theorem EulerSobolevTopBlocks.top_word_block (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))) (w : Fin (2 + q) → Fin 4) : EulerCylinderSobolevSpace.word period u ⋯ w = EulerCylinderSobolevSpace.word period ((EulerSobolevWordBlocks.wordBlock period 2 q fun (i : Fin q) => w (Fin.natAdd 2 i)) u) ⋯ fun (i : Fin 2) => w (Fin.castAdd q i)

A full top derivative is literally a second derivative of one of the genuine top word blocks.

theorem EulerSobolevTopBlocks.top_blocks_norm_sq (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))) : ‖u‖ ^ 2 ≤ ‖(EulerCylinderSobolevSpace.restrictOperator period ⋯) u‖ ^ 2 + ∑ w : Fin q → Fin 4, ‖(EulerSobolevWordBlocks.wordBlock period 2 q w) u‖ ^ 2

The genuine complete H^(q+2) norm is controlled by H^(q+1) and all order-q H² derivative blocks.

Strong time-space completion controlled by genuine finite spatial derivative blocks.

theorem EulerTopBlockTimeNorm.pathLp_quadratic_bound {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {I : Type u_4} [Fintype I] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (A : X →L[ℝ] Y) (B : I → X →L[ℝ] Z) (hb : ∀ (x : X), ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2 + ∑ i : I, ‖(B i) x‖ ^ 2) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), X)) : ‖EulerTimeLp.pathLp T hT u‖ ^ 2 ≤ ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) u)‖ ^ 2 + ∑ i : I, ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (B i)) u)‖ ^ 2

Integration preserves a finite quadratic norm comparison between bounded spatial observations.

theorem EulerTopBlockTimeNorm.top_blocks_time_norm (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) : ‖EulerTimeLp.pathLp T hT u‖ ^ 2 ≤ ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period ⋯)) u)‖ ^ 2 + ∑ w : Fin q → Fin 4, ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerSobolevWordBlocks.wordBlock period 2 q w)) u)‖ ^ 2

All actual order-q H² blocks and the lower H^(q+1) norm control the full H^(q+2) time norm.

Actual strong L²-time completion from finitely many closed derivative blocks.

Strong Cauchy convergence controlled by finitely many genuine norm observations.

theorem EulerQuadraticCauchy.cauchy_of_finite_quadratic_bound {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {I : Type u_4} [Fintype I] [NormedAddCommGroup X] [NormedAddCommGroup Y] [NormedAddCommGroup Z] (U : ℕ → X) (F : I → ℕ → Y) (V : ℕ → Z) (hu : CauchySeq U) (hf : ∀ (i : I), CauchySeq (F i)) (hb : ∀ (n m : ℕ), ‖V n - V m‖ ^ 2 ≤ ‖U n - U m‖ ^ 2 + ∑ i : I, ‖F i n - F i m‖ ^ 2) : CauchySeq V

A finite family of Cauchy observations controlling squared differences forces a sequence to be Cauchy.

theorem EulerTopBlockTimeNorm.mapped_pathLp_sub {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : ℝ) (hT : 0 ≤ T) (A : X →L[ℝ] Y) (u v : C(↑(Set.Icc 0 T), X)) : EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) (u - v)) = EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) u) - EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) v)

Bounded spatial observation and actual time embedding preserve subtraction together.

theorem EulerTopBlockTimeNorm.pathLp_quadratic_difference {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {I : Type u_4} [Fintype I] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (A : X →L[ℝ] Y) (B : I → X →L[ℝ] Z) (hb : ∀ (x : X), ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2 + ∑ i : I, ‖(B i) x‖ ^ 2) (T : ℝ) (hT : 0 ≤ T) (u v : C(↑(Set.Icc 0 T), X)) : ‖EulerTimeLp.pathLp T hT u - EulerTimeLp.pathLp T hT v‖ ^ 2 ≤ ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) u) - EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) v)‖ ^ 2 + ∑ i : I, ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (B i)) u) - EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (B i)) v)‖ ^ 2

The integrated genuine spatial block bound also controls time-space differences.

theorem EulerTopBlockTimeNorm.cauchy_pathLp_of_blocks {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {I : Type u_4} [Fintype I] [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [NormedAddCommGroup Z] [NormedSpace ℝ Z] (A : X →L[ℝ] Y) (B : I → X →L[ℝ] Z) (hb : ∀ (x : X), ‖x‖ ^ 2 ≤ ‖A x‖ ^ 2 + ∑ i : I, ‖(B i) x‖ ^ 2) (T : ℝ) (hT : 0 ≤ T) (u : ℕ → C(↑(Set.Icc 0 T), X)) (hu : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) (u n))) (hf : ∀ (i : I), CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (B i)) (u n))) : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT (u n)

Genuine finite block convergence and lower-order convergence construct strong convergence in the full Bochner Sobolev space.

Genuine maximal spatial regularity of the actual viscous mild solution, proved by strong Cauchy limits.

theorem EulerHeatMaximalRegularity.regularized_mild_cauchy (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) : CauchySeq fun (n : ℕ) => EulerHeatMaximalCauchy.higherTime period T hT (EulerRegularizedMildEquation.regularizedState period T n u)

The actual regularized mild solutions are strongly Cauchy in Bochner L² time with two derivatives.

theorem EulerHeatMaximalRegularity.regularized_limit_restriction (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerHeatMaximalCauchy.higherTime period T hT (EulerRegularizedMildEquation.regularizedState period T n u)) Filter.atTop (nhds U)) : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period 1) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT u

The strong higher-order limit has exactly the original lower-order field almost everywhere in time.

theorem EulerHeatMaximalRegularity.regularized_limit_bound (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hd : ∀ (n : ℕ), ∀ t ∈ Set.Ioo 0 T, ∀ (i : Fin 4), HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 2 i) (EulerVolterraConvolution.extendPath T hT (EulerRegularizedMildEquation.regularizedState period T n u) s))) (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) (ν • (EulerSobolevLaplacian.laplacianOperator period 1) (EulerVolterraConvolution.extendPath T hT (EulerRegularizedMildEquation.regularizedState period T n u) t) + EulerVolterraConvolution.extendPath T hT (EulerRegularizedMildEquation.regularizedForcing period T n f) t))) t) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerHeatMaximalCauchy.higherTime period T hT (EulerRegularizedMildEquation.regularizedState period T n u)) Filter.atTop (nhds U)) : ‖U‖ ^ 2 ≤ (T + 4 * ν⁻¹) * ‖u‖ ^ 2 + ν⁻¹ ^ 2 * ‖EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.valueOperator period 0)) f)‖ ^ 2

The genuine heat estimate passes to the strong higher-order time limit without weak compactness.

theorem EulerHeatMaximalRegularity.exists_H2_time_limit (period : ℝ) [Fact (0 < period)] (T : ℝ) (u : ℕ → ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))) (hu : CauchySeq u) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))), Filter.Tendsto u Filter.atTop (nhds U)

Completeness of actual H² Bochner space constructs its strong Cauchy limit.

theorem EulerHeatMaximalRegularity.exists_regularized_mild_limit (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))), Filter.Tendsto (fun (n : ℕ) => EulerHeatMaximalCauchy.higherTime period T hT (EulerRegularizedMildEquation.regularizedState period T n u)) Filter.atTop (nhds U)

Strong completion constructs the higher-order limit of the concrete mild-solution approximations.

theorem EulerHeatMaximalRegularity.viscous_mild_maximal_regularity (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period 2))), (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period 1) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT u ∧ Filter.Tendsto (fun (n : ℕ) => EulerHeatMaximalCauchy.higherTime period T hT (EulerRegularizedMildEquation.regularizedState period T n u)) Filter.atTop (nhds U)

The actual viscous mild solution with H¹ values and continuous L² source has two full spatial derivatives in L² time. The higher-regularity element is constructed in the complete Bochner space and identified with the original field almost everywhere.

theorem EulerHeatMaximalRegularity.viscous_mild_ae_H2 (period : ℝ) [Fact (0 < period)] (T : ℝ) (hT : 0 ≤ T) (ν : ℝ) (hν : 0 < ν) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))) (hsol : ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ∃ (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)), EulerCylinderSobolevSpace.value period v = EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u t)

Actual H² spatial representatives exist for almost every time of the genuine H¹ viscous mild solution.

theorem EulerMaximalTopCauchy.top_blocks_norm_sq_original (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))) : ‖u‖ ^ 2 ≤ ‖(EulerCylinderSobolevSpace.restrictOperator period ⋯) u‖ ^ 2 + ∑ w : Fin q → Fin 4, ‖(EulerSobolevWordBlocks.wordBlock period 2 q w) u‖ ^ 2

The top block norm estimate in the original q+1 indexing used by actual mild solutions.

theorem EulerMaximalTopCauchy.maximalApproximation_word_cauchy (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (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))) (w : Fin q → Fin 4) : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerSobolevWordBlocks.wordBlock period 2 q w)) (EulerRegularizedTopBlocks.maximalApproximation period q T n u))

Every actual top-word regularization is strongly Cauchy in time with its two full extra spatial derivatives.

theorem EulerMaximalTopCauchy.maximalApproximation_cauchy (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (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))) : CauchySeq fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)

The genuine full H^(q+2) heat regularizations form a strong Bochner Cauchy sequence, with no assumed derivative bound.

theorem EulerSobolevMaximalRegularity.exists_sobolev_time_limit (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (u : ℕ → ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (hu : CauchySeq u) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))), Filter.Tendsto u Filter.atTop (nhds U)

The complete actual Bochner Sobolev space realizes every strong Cauchy sequence.

theorem EulerSobolevMaximalRegularity.exists_maximal_mild_limit (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (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))) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))), Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)

Completion supplies the genuine higher-order limit of the actual viscous approximations.

theorem EulerSobolevMaximalRegularity.maximal_limit_restriction (period : ℝ) [Fact (0 < period)] {q : ℕ} (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)) : (fun (t : ℝ) => (EulerCylinderSobolevSpace.restrictOperator period ⋯) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT u

The actual higher-order limit restricts to the original viscous solution almost everywhere.

theorem EulerSobolevMaximalRegularity.viscous_mild_maximal_regularity (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (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))) : ∃ (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))), (fun (t : ℝ) => (EulerCylinderSobolevSpace.restrictOperator period ⋯) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT u ∧ Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)

Actual viscous mild solutions with continuous Hq forcing and H^(q+1) values possess full H^(q+2) regularity in Bochner L² time. The stronger field is constructed from genuine heat approximations and identified with the original field almost everywhere.

theorem EulerSobolevMaximalRegularity.viscous_mild_ae_higher (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (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 : ℝ) ∂EulerTimeLp.timeMeasure T, ∃ (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))), (EulerCylinderSobolevSpace.restrictOperator period ⋯) v = EulerVolterraConvolution.extendPath T hT u t

The genuine full higher-order spatial derivatives exist at almost every time of the actual viscous solution.