General smooth local Euler existence in ordinary R³. The datum has all actual spatial L² derivatives; no Gevrey radius is assumed. The solution is the strong Sobolev limit of genuine symmetric regularized Euler evolutions on one common positive interval.

Actual smooth regularizers of ordinary solenoidal L². Their maps into every complete Sobolev space are bounded by the closed graph theorem, rather than by an assumed derivative estimate.

theorem EulerOrdinarySobolev.instOrdinarySmoothingOperator1 : Fact (0 < 1)

structure EulerOrdinarySobolev.SmoothingOperator : Type

Smoothing operator data, collecting op, smooth, translation, symmetric, contraction, solenoidal.

• op : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

  Op of SmoothingOperator, of type L2 →L[ℝ] L2.

• smooth (u : ↥EulerMeanSolenoidal.L2) : EulerMeanSmoothRepresentative.SmoothOrbit (self.op u)
• translation (a : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : (EulerMeanSolenoidal.translation a) (self.op u) = self.op ((EulerMeanSolenoidal.translation a) u)
• symmetric (u v : ↥EulerMeanSolenoidal.L2) : inner ℝ (self.op u) v = inner ℝ u (self.op v)
• contraction (u : ↥EulerMeanSolenoidal.L2) : ‖self.op u‖ ≤ ‖u‖
• solenoidal (u : ↥EulerMeanSolenoidal.L2) : self.op u ∈ EulerMeanSolenoidal.solenoidalSpace

noncomputable def EulerOrdinarySobolev.SmoothingOperator.field (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Field, given by smoothL2Field (S.op u) (S.smooth u).

Equations

• S.field u = EulerMeanSmoothRepresentative.smoothL2Field (S.op u) ⋯

@[simp]

theorem EulerOrdinarySobolev.SmoothingOperator.field_toLp (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) : (S.field u).toLp = S.op u

noncomputable def EulerOrdinarySobolev.SmoothingOperator.liftLinear (S : SmoothingOperator) (q : ℕ) : ↥EulerMeanSolenoidal.L2 →ₗ[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q)

Lift linear, bundling toFun, map_add, map_smul.

Equations

• S.liftLinear q = { toFun := fun (u : ↥EulerMeanSolenoidal.L2) => EulerMeanSmoothRepresentative.ordinarySobolev q (S.op u) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem EulerOrdinarySobolev.SmoothingOperator.liftLinear_value (S : SmoothingOperator) (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) : EulerCylinderSobolevSpace.value 1 ((S.liftLinear q) u) = EulerMeanOrdinaryLift.ordinaryLift (S.op u)

noncomputable def EulerOrdinarySobolev.SmoothingOperator.lift (S : SmoothingOperator) (q : ℕ) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace 1 q)

Lift, constructed using ContinuousLinearMap.ofSeqClosedGraph.

Equations

• S.lift q = ContinuousLinearMap.ofSeqClosedGraph ⋯

@[simp]

theorem EulerOrdinarySobolev.SmoothingOperator.lift_apply (S : SmoothingOperator) (q : ℕ) (u : ↥EulerMeanSolenoidal.L2) : (S.lift q) u = EulerMeanSmoothRepresentative.ordinarySobolev q (S.op u) ⋯

noncomputable def EulerOrdinarySobolev.SmoothingOperator.jetMap (S : SmoothingOperator) (n : ℕ) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space) 2 MeasureTheory.volume)

Jet map, given by (ordinaryTensorOperator n).comp (S.lift n).

Equations

• S.jetMap n = EulerOrdinarySobolev.ordinaryTensorOperator n ∘SL S.lift n

theorem EulerOrdinarySobolev.SmoothingOperator.field_jetLp (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) (n : ℕ) : (S.field u).jetLp n = (S.jetMap n) u

theorem EulerOrdinarySobolev.SmoothingOperator.field_jet_continuous (S : SmoothingOperator) {K : Type u_1} [TopologicalSpace K] (u : K → ↥EulerMeanSolenoidal.L2) (hu : Continuous u) (n : ℕ) : Continuous fun (t : K) => (S.field (u t)).jetLp n

theorem EulerOrdinarySobolev.SmoothingOperator.field_jet_norm (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) (n : ℕ) : ‖(S.field u).jetLp n‖ ≤ ‖S.jetMap n‖ * ‖u‖

theorem EulerOrdinarySobolev.SmoothingOperator.field_add (S : SmoothingOperator) (u v : ↥EulerMeanSolenoidal.L2) : S.field (u + v) = (S.field u).addField (S.field v)

theorem EulerOrdinarySobolev.SmoothingOperator.field_smul (S : SmoothingOperator) (c : ℝ) (u : ↥EulerMeanSolenoidal.L2) : S.field (c • u) = scaleField c (S.field u)

theorem EulerOrdinarySobolev.SmoothingOperator.field_word (S : SmoothingOperator) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : (wordField (S.field A.toLp) w).toLp = S.op (wordField A w).toLp

theorem EulerOrdinarySobolev.SmoothingOperator.field_word_norm (S : SmoothingOperator) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : ‖(wordField (S.field A.toLp) w).toLp‖ ≤ ‖(wordField A w).toLp‖

theorem EulerOrdinarySobolev.SmoothingOperator.field_wordBound (S : SmoothingOperator) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) (N : ℝ) (hN : WordBound q N A) : WordBound q N (S.field A.toLp)

theorem EulerOrdinarySobolev.SmoothingOperator.field_energy_le (S : SmoothingOperator) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : wordEnergy q (S.field A.toLp) ≤ wordEnergy q A

noncomputable def EulerOrdinarySobolev.SmoothingOperator.pointwiseCost (S : SmoothingOperator) : ℝ

Pointwise cost, given by smoothEmbeddingConstant*(∑ n ∈ range 3, ‖S.jetMap n‖).

Equations

• S.pointwiseCost = EulerSmoothSobolev.smoothEmbeddingConstant * ∑ n ∈ Finset.range 3, ‖S.jetMap n‖

theorem EulerOrdinarySobolev.SmoothingOperator.pointwiseCost_nonneg (S : SmoothingOperator) : 0 ≤ S.pointwiseCost

theorem EulerOrdinarySobolev.SmoothingOperator.field_pointwise (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) (x : EulerSmoothLimit.Space) : ‖(S.field u).field x‖ ≤ S.pointwiseCost * ‖u‖

The regularized L² flow has genuine smooth spatial representatives, continuous jets of every order, and its true time derivative.

A bounded quadratic vector field whose radial energy vanishes has a genuine global flow on a real Hilbert space. Radial normalization first gives a globally Lipschitz equation; its conserved norm then removes the normalization by a constant rescaling of time.

noncomputable def EulerHilbertQuadraticFlow.radial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : E

Radial, given by (1+‖x‖)⁻¹ • x.

Equations

• EulerHilbertQuadraticFlow.radial x = (1 + ‖x‖)⁻¹ • x

theorem EulerHilbertQuadraticFlow.radial_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : ‖radial x‖ ≤ 1

theorem EulerHilbertQuadraticFlow.radial_sub_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x y : E) : ‖radial x - radial y‖ ≤ 2 * ‖x - y‖

theorem EulerHilbertQuadraticFlow.radial_lipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : LipschitzWith 2 radial

noncomputable def EulerHilbertQuadraticFlow.normalized {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] E) (x : E) : E

Normalized, given by B (radial x) (radial x).

Equations

• EulerHilbertQuadraticFlow.normalized B x = (B (EulerHilbertQuadraticFlow.radial x)) (EulerHilbertQuadraticFlow.radial x)

theorem EulerHilbertQuadraticFlow.bilinear_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] E) (x y : E) : ‖(B x) y‖ ≤ ‖B‖ * ‖x‖ * ‖y‖

theorem EulerHilbertQuadraticFlow.normalized_lipschitz {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] E) : LipschitzWith (4 * ‖B‖₊) (normalized B)

theorem EulerHilbertQuadraticFlow.normalized_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (B : E →L[ℝ] E →L[ℝ] E) (x : E) : normalized B x = (1 + ‖x‖)⁻¹ ^ 2 • (B x) x

theorem EulerHilbertQuadraticFlow.exists_global_quadratic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (B : E →L[ℝ] E →L[ℝ] E) (hB : ∀ (x : E), inner ℝ x ((B x) x) = 0) (x : E) : ∃ (u : ℝ → E), u 0 = x ∧ (∀ (t : ℝ), HasDerivAt u ((B (u t)) (u t)) t) ∧ ∀ (t : ℝ), ‖u t‖ = ‖x‖

A genuine global L² solution of the symmetric regularized Euler equation. The vector field is a bounded bilinear map and its actual L² energy vanishes by noncompact transport cancellation.

theorem EulerOrdinarySobolev.advection_add_left (A B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : advectionField (A.addField B) C = (advectionField A C).addField (advectionField B C)

theorem EulerOrdinarySobolev.advection_add_right (A B C : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : advectionField A (B.addField C) = (advectionField A B).addField (advectionField A C)

theorem EulerOrdinarySobolev.advection_smul_left (c : ℝ) (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : advectionField (scaleField c A) B = scaleField c (advectionField A B)

theorem EulerOrdinarySobolev.advection_smul_right (c : ℝ) (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : advectionField A (scaleField c B) = scaleField c (advectionField A B)

noncomputable def EulerOrdinarySobolev.SmoothingOperator.advectionLinear (S : SmoothingOperator) : ↥EulerMeanSolenoidal.L2 →ₗ[ℝ] ↥EulerMeanSolenoidal.L2 →ₗ[ℝ] ↥EulerMeanSolenoidal.L2

Advection linear, bundling toFun, map_add, map_smul, map_add and the required compatibility proofs.

Equations

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

noncomputable def EulerOrdinarySobolev.SmoothingOperator.advectionCost (S : SmoothingOperator) : ℝ

Advection cost, given by S.pointwiseCost*‖S.jetMap 1‖.

Equations

• S.advectionCost = S.pointwiseCost * ‖S.jetMap 1‖

theorem EulerOrdinarySobolev.SmoothingOperator.advectionLinear_bound (S : SmoothingOperator) (u v : ↥EulerMeanSolenoidal.L2) : ‖(S.advectionLinear u) v‖ ≤ S.advectionCost * ‖u‖ * ‖v‖

noncomputable def EulerOrdinarySobolev.SmoothingOperator.advection (S : SmoothingOperator) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Advection, given by S.advectionLinear.mkContinuous₂ S.advectionCost S.advectionLinear_bound.

Equations

• S.advection = S.advectionLinear.mkContinuous₂ S.advectionCost ⋯

@[simp]

theorem EulerOrdinarySobolev.SmoothingOperator.advection_apply (S : SmoothingOperator) (u v : ↥EulerMeanSolenoidal.L2) : (S.advection u) v = (advectionField (S.field u) (S.field v)).toLp

noncomputable def EulerOrdinarySobolev.SmoothingOperator.quadratic (S : SmoothingOperator) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Quadratic, given by (ContinuousLinearMap.compL ℝ L2 L2 L2 (-S.op)).comp S.advection.

Equations

• S.quadratic = (ContinuousLinearMap.compL ℝ ↥EulerMeanSolenoidal.L2 ↥EulerMeanSolenoidal.L2 ↥EulerMeanSolenoidal.L2) (-S.op) ∘SL S.advection

@[simp]

theorem EulerOrdinarySobolev.SmoothingOperator.quadratic_apply (S : SmoothingOperator) (u v : ↥EulerMeanSolenoidal.L2) : (S.quadratic u) v = -S.op (advectionField (S.field u) (S.field v)).toLp

theorem EulerOrdinarySobolev.SmoothingOperator.field_divergence (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (S.field u).field x = 0

theorem EulerOrdinarySobolev.SmoothingOperator.quadratic_energy (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) : inner ℝ u ((S.quadratic u) u) = 0

theorem EulerOrdinarySobolev.SmoothingOperator.exists_global (S : SmoothingOperator) (u₀ : ↥EulerMeanSolenoidal.L2) : ∃ (u : ℝ → ↥EulerMeanSolenoidal.L2), u 0 = u₀ ∧ (∀ (t : ℝ), HasDerivAt u ((S.quadratic (u t)) (u t)) t) ∧ ∀ (t : ℝ), ‖u t‖ = ‖u₀‖

noncomputable def EulerOrdinarySobolev.SmoothingOperator.rhs (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Rhs, given by fieldNeg (S.field (advectionField (S.field u) (S.field u)).toLp).

Equations

• S.rhs u = EulerOrdinarySobolev.fieldNeg (S.field (EulerOrdinarySobolev.advectionField (S.field u) (S.field u)).toLp)

theorem EulerOrdinarySobolev.SmoothingOperator.rhs_toLp (S : SmoothingOperator) (u : ↥EulerMeanSolenoidal.L2) : (S.rhs u).toLp = (S.quadratic u) u

theorem EulerOrdinarySobolev.SmoothingOperator.rhs_continuous (S : SmoothingOperator) {K : Type u_1} [TopologicalSpace K] (u : K → ↥EulerMeanSolenoidal.L2) (hu : Continuous u) (n : ℕ) : Continuous fun (t : K) => (S.rhs (u t)).jetLp n

structure EulerOrdinarySobolev.RegularizedEvolution (S : SmoothingOperator) (T : ℝ) (hT : 0 ≤ T) : Type

Regularized evolution data, collecting velocity, velocity_continuous, solenoidal, time_law.

• velocity : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Velocity field of RegularizedEvolution, of type Icc (0 : ℝ) T → SmoothL2Field Space.

• velocity_continuous (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (self.velocity t).jetLp n
• solenoidal (t : ↑(Set.Icc 0 T)) : (self.velocity t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace
• time_law (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => (self.velocity (Set.projIcc 0 T hT r)).toLp) ((S.quadratic (self.velocity ⟨t, ⋯⟩).toLp) (self.velocity ⟨t, ⋯⟩).toLp) t

noncomputable def EulerOrdinarySobolev.RegularizedEvolution.derivative {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Derivative, given by S.rhs (U.velocity t).toLp.

Equations

• U.derivative t = S.rhs (U.velocity t).toLp

theorem EulerOrdinarySobolev.RegularizedEvolution.derivative_continuous {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (U.derivative t).jetLp n

theorem EulerOrdinarySobolev.RegularizedEvolution.pointwise_time {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (U.velocity (Set.projIcc 0 T hT r)).field x) ((U.derivative t).field x) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.RegularizedEvolution.l2_time {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => (U.velocity (Set.projIcc 0 T hT r)).toLp) (U.derivative t).toLp (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.SmoothingOperator.exists_smooth (S : SmoothingOperator) (T : ℝ) (hT : 0 ≤ T) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) : ∃ (U : RegularizedEvolution S T hT), U.velocity ⟨0, ⋯⟩ = A

Actual symmetric, solenoidal smoothing operators. They converge to Helmholtz projection, with an explicit H¹ approximation error.

Symmetric compact smooth approximate identities on ordinary spatial L².

A true orbit derivative gives a global increment bound for a linear isometric action.

theorem EulerIsometricAction.norm_sub_le_of_hasFDerivAt {P : Type u_1} {E : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] (τ : P → E →ₗᵢ[ℝ] E) (hadd : ∀ (a b : P) (u : E), (τ a) ((τ b) u) = (τ (a + b)) u) (hzero : ∀ (u : E), (τ 0) u = u) (u : E) (D : P →L[ℝ] E) (h : HasFDerivAt (fun (a : P) => (τ a) u) D 0) (a : P) : ‖(τ a) u - u‖ ≤ ‖D‖ * ‖a‖

noncomputable def EulerOrdinaryMollifier.bump (n : ℕ) : ContDiffBump 0

Bump, bundling rIn, rOut, rIn_pos, rIn_lt_rOut.

Equations

• EulerOrdinaryMollifier.bump n = { rIn := EulerNoncompactTransport.cutoffScale n, rOut := 2 * EulerNoncompactTransport.cutoffScale n, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def EulerOrdinaryMollifier.kernel (n : ℕ) : EulerSmoothLimit.Space → ℝ

Kernel, given by (bump n).normed volume.

Equations

• EulerOrdinaryMollifier.kernel n = (EulerOrdinaryMollifier.bump n).normed MeasureTheory.volume

theorem EulerOrdinaryMollifier.kernel_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (kernel n)

theorem EulerOrdinaryMollifier.kernel_compact (n : ℕ) : HasCompactSupport (kernel n)

theorem EulerOrdinaryMollifier.kernel_nonneg (n : ℕ) (x : EulerSmoothLimit.Space) : 0 ≤ kernel n x

theorem EulerOrdinaryMollifier.kernel_integral (n : ℕ) : ∫ (x : EulerSmoothLimit.Space), kernel n x = 1

theorem EulerOrdinaryMollifier.kernel_integrable (n : ℕ) : MeasureTheory.Integrable (kernel n) MeasureTheory.volume

theorem EulerOrdinaryMollifier.kernel_neg (n : ℕ) (x : EulerSmoothLimit.Space) : kernel n (-x) = kernel n x

noncomputable def EulerOrdinaryMollifier.smoothOrbit (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : EulerSmoothLimit.Space → ↥EulerMeanSolenoidal.L2

Smooth orbit, given by convolution (kernel n) (fun a => translation a u) (ContinuousLinearMap.lsmul ℝ ℝ) volume.

Equations

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

noncomputable def EulerOrdinaryMollifier.mollify (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : ↥EulerMeanSolenoidal.L2

Mollify, given by smoothOrbit n u 0.

Equations

• EulerOrdinaryMollifier.mollify n u = EulerOrdinaryMollifier.smoothOrbit n u 0

theorem EulerOrdinaryMollifier.smoothOrbit_contDiff (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : ContDiff ℝ (↑⊤) (smoothOrbit n u)

theorem EulerOrdinaryMollifier.mollify_tendsto (u : ↥EulerMeanSolenoidal.L2) : Filter.Tendsto (fun (n : ℕ) => mollify n u) Filter.atTop (nhds u)

theorem EulerOrdinaryMollifier.mollify_eq_integral (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : mollify n u = ∫ (y : EulerSmoothLimit.Space), kernel n y • (EulerMeanSolenoidal.translation (-y)) u

theorem EulerOrdinaryMollifier.kernel_orbit_integrable (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : MeasureTheory.Integrable (fun (y : EulerSmoothLimit.Space) => kernel n y • (EulerMeanSolenoidal.translation (-y)) u) MeasureTheory.volume

theorem EulerOrdinaryMollifier.mollify_norm_le (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : ‖mollify n u‖ ≤ ‖u‖

theorem EulerOrdinaryMollifier.mollify_add (n : ℕ) (u v : ↥EulerMeanSolenoidal.L2) : mollify n (u + v) = mollify n u + mollify n v

theorem EulerOrdinaryMollifier.mollify_smul (n : ℕ) (c : ℝ) (u : ↥EulerMeanSolenoidal.L2) : mollify n (c • u) = c • mollify n u

noncomputable def EulerOrdinaryMollifier.mollifierLinear (n : ℕ) : ↥EulerMeanSolenoidal.L2 →ₗ[ℝ] ↥EulerMeanSolenoidal.L2

Mollifier linear, bundling toFun, map_add, map_smul.

Equations

• EulerOrdinaryMollifier.mollifierLinear n = { toFun := EulerOrdinaryMollifier.mollify n, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerOrdinaryMollifier.mollifier (n : ℕ) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Mollifier, given by (mollifierLinear n).mkContinuous 1 (fun u => by change ‖mollify n u‖ ≤ 1*‖u‖ simpa only [one_mul] using mollify_norm_le n u).

Equations

• EulerOrdinaryMollifier.mollifier n = (EulerOrdinaryMollifier.mollifierLinear n).mkContinuous 1 ⋯

@[simp]

theorem EulerOrdinaryMollifier.mollifier_apply (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : (mollifier n) u = mollify n u

theorem EulerOrdinaryMollifier.mollify_translation (n : ℕ) (a : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : (EulerMeanSolenoidal.translation a) (mollify n u) = mollify n ((EulerMeanSolenoidal.translation a) u)

theorem EulerOrdinaryMollifier.smoothOrbit_eq (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) (x : EulerSmoothLimit.Space) : smoothOrbit n u x = (EulerMeanSolenoidal.translation x) (mollify n u)

theorem EulerOrdinaryMollifier.mollify_smooth (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanSolenoidal.translation a) (mollify n u)

theorem EulerOrdinaryMollifier.translation_inner_shift (a : EulerSmoothLimit.Space) (u v : ↥EulerMeanSolenoidal.L2) : inner ℝ ((EulerMeanSolenoidal.translation a) u) v = inner ℝ u ((EulerMeanSolenoidal.translation (-a)) v)

theorem EulerOrdinaryMollifier.mollify_symmetric (n : ℕ) (u v : ↥EulerMeanSolenoidal.L2) : inner ℝ (mollify n u) v = inner ℝ u (mollify n v)

theorem EulerOrdinaryMollifier.translation_increment (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (a : EulerSmoothLimit.Space) : ‖(EulerMeanSolenoidal.translation a) A.toLp - A.toLp‖ ≤ ‖A.derivative.toLp‖ * ‖a‖

theorem EulerOrdinaryMollifier.mollify_error (n : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ‖mollify n A.toLp - A.toLp‖ ≤ 2 * EulerNoncompactTransport.cutoffScale n * ‖A.derivative.toLp‖

theorem EulerOrdinarySobolev.projection_inner (u v : ↥EulerMeanSolenoidal.L2) : inner ℝ (EulerMeanSolenoidal.solenoidalProjection u) v = inner ℝ u (EulerMeanSolenoidal.solenoidalProjection v)

theorem EulerOrdinarySobolev.projection_idempotent (u : ↥EulerMeanSolenoidal.L2) : EulerMeanSolenoidal.solenoidalProjection (EulerMeanSolenoidal.solenoidalProjection u) = EulerMeanSolenoidal.solenoidalProjection u

noncomputable def EulerOrdinarySobolev.regularizerMap (n : ℕ) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Regularizer map, given by solenoidalProjection.comp ((mollifier n).comp solenoidalProjection).

Equations

• EulerOrdinarySobolev.regularizerMap n = EulerMeanSolenoidal.solenoidalProjection ∘SL EulerOrdinaryMollifier.mollifier n ∘SL EulerMeanSolenoidal.solenoidalProjection

@[simp]

theorem EulerOrdinarySobolev.regularizerMap_apply (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : (regularizerMap n) u = EulerMeanSolenoidal.solenoidalProjection (EulerOrdinaryMollifier.mollify n (EulerMeanSolenoidal.solenoidalProjection u))

theorem EulerOrdinarySobolev.regularizerMap_translation (n : ℕ) (a : EulerSmoothLimit.Space) (u : ↥EulerMeanSolenoidal.L2) : (EulerMeanSolenoidal.translation a) ((regularizerMap n) u) = (regularizerMap n) ((EulerMeanSolenoidal.translation a) u)

theorem EulerOrdinarySobolev.regularizerMap_smooth (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : EulerMeanSmoothRepresentative.SmoothOrbit ((regularizerMap n) u)

theorem EulerOrdinarySobolev.regularizerMap_symmetric (n : ℕ) (u v : ↥EulerMeanSolenoidal.L2) : inner ℝ ((regularizerMap n) u) v = inner ℝ u ((regularizerMap n) v)

theorem EulerOrdinarySobolev.regularizerMap_contract (n : ℕ) (u : ↥EulerMeanSolenoidal.L2) : ‖(regularizerMap n) u‖ ≤ ‖u‖

noncomputable def EulerOrdinarySobolev.regularizer (n : ℕ) : SmoothingOperator

Regularizer, bundling op, smooth, translation, symmetric and the required compatibility proofs.

Equations

• EulerOrdinarySobolev.regularizer n = { op := EulerOrdinarySobolev.regularizerMap n, smooth := ⋯, translation := ⋯, symmetric := ⋯, contraction := ⋯, solenoidal := ⋯ }

theorem EulerOrdinarySobolev.regularizer_tendsto (u : ↥EulerMeanSolenoidal.L2) : Filter.Tendsto (fun (n : ℕ) => (regularizer n).op u) Filter.atTop (nhds (EulerMeanSolenoidal.solenoidalProjection u))

theorem EulerOrdinarySobolev.regularizer_error (n : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ‖(regularizer n).op A.toLp - EulerMeanSolenoidal.solenoidalProjection A.toLp‖ ≤ 2 * EulerNoncompactTransport.cutoffScale n * ‖(solenoidalField A).derivative.toLp‖

theorem EulerOrdinarySobolev.solenoidalField_wordBound (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) (M : ℝ) (hM : WordBound q M A) : WordBound q M (solenoidalField A)

noncomputable def EulerOrdinarySobolev.regularizerError (n : ℕ) : ℝ

Regularizer error, given by 6*EulerNoncompactTransport.cutoffScale n.

Equations

• EulerOrdinarySobolev.regularizerError n = 6 * EulerNoncompactTransport.cutoffScale n

theorem EulerOrdinarySobolev.regularizerError_nonneg (n : ℕ) : 0 ≤ regularizerError n

theorem EulerOrdinarySobolev.regularizerError_tendsto : Filter.Tendsto regularizerError Filter.atTop (nhds 0)

theorem EulerOrdinarySobolev.regularizer_error_wordBound (n : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M : ℝ) (hM : WordBound 1 M A) : ‖(regularizer n).op A.toLp - EulerMeanSolenoidal.solenoidalProjection A.toLp‖ ≤ regularizerError n * M

The true smooth regularized Euler flows are Cauchy in continuous L² on the common energy-controlled interval.

The actual regularized Euler right-hand side converges to the projected Euler right-hand side, uniformly on bounded H⁴ sets.

theorem EulerOrdinarySobolev.regularizer_error_words (n : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (q : ℕ) (M : ℝ) (hM : WordBound (q + 1) M A) : WordBound q (regularizerError n * M) (fieldSub ((regularizer n).field A.toLp) A)

theorem EulerOrdinarySobolev.wordBound_gradient {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {M : ℝ} (hM : WordBound 3 M A) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ A.field x‖ ≤ 360 * EulerSmoothSobolev.smoothEmbeddingConstant * M

theorem EulerOrdinarySobolev.advection_low_words (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M : ℝ) (hM : WordBound 4 M A) : WordBound 1 (6 * h3ProductConstant * M ^ 2) (advectionField A A)

noncomputable def EulerOrdinarySobolev.regularizationCost (M : ℝ) : ℝ

Regularization cost, given by (6*h3ProductConstant+399*smoothEmbeddingConstant)*M^2.

Equations

• EulerOrdinarySobolev.regularizationCost M = (6 * EulerOrdinarySobolev.h3ProductConstant + 399 * EulerSmoothSobolev.smoothEmbeddingConstant) * M ^ 2

theorem EulerOrdinarySobolev.regularizationCost_nonneg (M : ℝ) : 0 ≤ regularizationCost M

theorem EulerOrdinarySobolev.regularized_rhs_error (n : ℕ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (M : ℝ) (hM : WordBound 4 M A) : ‖((regularizer n).rhs A.toLp).toLp - (projectedRhs A).toLp‖ ≤ regularizerError n * regularizationCost M

Actual L² stability of projected Euler with a small additive defect. The reference gradient is the only solution coefficient.

theorem EulerOrdinarySobolev.projected_difference_energy (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hB : B.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) : 2 * inner ℝ (B.toLp - A.toLp) ((projectedRhs B).toLp - (projectedRhs A).toLp) ≤ 2 * K * ‖B.toLp - A.toLp‖ ^ 2

theorem EulerOrdinarySobolev.perturbed_difference_energy (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hB : B.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (RA RB : ↥EulerMeanSolenoidal.L2) (K ea eb : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (ha : ‖RA - (projectedRhs A).toLp‖ ≤ ea) (hb : ‖RB - (projectedRhs B).toLp‖ ≤ eb) : 2 * inner ℝ (B.toLp - A.toLp) (RB - RA) ≤ (2 * K + 1) * ‖B.toLp - A.toLp‖ ^ 2 + (ea + eb) ^ 2

theorem EulerOrdinarySobolev.forced_linear_zero_bound (T C E : ℝ) (hC : 1 ≤ C) (X X' : ℝ → ℝ) (hX : ContinuousOn X (Set.Icc 0 T)) (hX0 : X 0 = 0) (hd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt X (X' t) (Set.Icc 0 T) t) (hb : ∀ t ∈ Set.Icc 0 T, X' t ≤ C * X t + E ^ 2) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : X t ≤ E ^ 2 * Real.exp (C * T)

noncomputable def EulerOrdinarySobolev.regularizedComparisonCost (T M : ℝ) : ℝ

Regularized comparison cost, given by regularizationCost M*Real.sqrt (Real.exp ((2*((360*smoothEmbeddingConstant)*M)+1)*T)).

Equations

• EulerOrdinarySobolev.regularizedComparisonCost T M = EulerOrdinarySobolev.regularizationCost M * √(Real.exp ((2 * (360 * EulerSmoothSobolev.smoothEmbeddingConstant * M) + 1) * T))

theorem EulerOrdinarySobolev.regularizedComparisonCost_nonneg (T M : ℝ) : 0 ≤ regularizedComparisonCost T M

theorem EulerOrdinarySobolev.regularized_l2_comparison {T : ℝ} {hT : 0 ≤ T} {j k : ℕ} (U : RegularizedEvolution (regularizer j) T hT) (V : RegularizedEvolution (regularizer k) T hT) (M : ℝ) (hU : ∀ (t : ↑(Set.Icc 0 T)), WordBound 4 M (U.velocity t)) (hV : ∀ (t : ↑(Set.Icc 0 T)), WordBound 4 M (V.velocity t)) (hinit : (V.velocity ⟨0, ⋯⟩).toLp = (U.velocity ⟨0, ⋯⟩).toLp) : ‖fieldPath V.velocity ⋯ - fieldPath U.velocity ⋯‖ ≤ (regularizerError j + regularizerError k) * regularizedComparisonCost T M

theorem EulerOrdinarySobolev.regularized_cauchy {T : ℝ} {hT : 0 ≤ T} (U : (n : ℕ) → RegularizedEvolution (regularizer n) T hT) (M : ℝ) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), WordBound 4 M ((U n).velocity t)) (hinit : ∀ (j k : ℕ), ((U k).velocity ⟨0, ⋯⟩).toLp = ((U j).velocity ⟨0, ⋯⟩).toLp) : CauchySeq fun (n : ℕ) => fieldPath (U n).velocity ⋯

Uniform energy bounds for the actual regularized flows. Symmetry and translation commutation transfer the exact energy production to the smoothed velocity, where the checked Euler cancellations apply.

A uniform short-time bound for a nonnegative genuine energy with a quadratic differential upper bound.

theorem EulerOrdinarySobolev.quadratic_energy_bound (T C : ℝ) (hT : 0 ≤ T) (X X' : ℝ → ℝ) (hX : ContinuousOn X (Set.Icc 0 T)) (hpos : ∀ t ∈ Set.Icc 0 T, 0 ≤ X t) (hd : ∀ t ∈ Set.Icc 0 T, HasDerivWithinAt X (X' t) (Set.Icc 0 T) t) (hb : ∀ t ∈ Set.Icc 0 T, X' t ≤ C * (1 + X t) ^ 2) (hC : 0 ≤ C) (hsmall : C * T ≤ (1 + X 0)⁻¹ / 2) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : X t ≤ 2 * X 0 + 1

theorem EulerOrdinarySobolev.SmoothingOperator.rhs_pairing (S : SmoothingOperator) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : inner ℝ (wordField A w).toLp (wordField (S.rhs A.toLp) w).toLp = inner ℝ (wordField (S.field A.toLp) w).toLp (wordField (fieldNeg (advectionField (S.field A.toLp) (S.field A.toLp))) w).toLp

theorem EulerOrdinarySobolev.SmoothingOperator.rhs_energy (S : SmoothingOperator) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : WordBound 3 M A) : integerEnergyProduction m A (S.rhs A.toLp) ≤ tameEnergyConstant m * M * wordEnergy m A

noncomputable def EulerOrdinarySobolev.RegularizedEvolution.energy {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (m : ℕ) : C(↑(Set.Icc 0 T), ℝ)

Energy, given by ⟨fun t => wordEnergy m (U.velocity t),wordEnergy_continuous U.velocity U.velocity_continuous m⟩.

Equations

• U.energy m = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.wordEnergy m (U.velocity t), continuous_toFun := ⋯ }

noncomputable def EulerOrdinarySobolev.RegularizedEvolution.energyDerivative {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (m : ℕ) (t : ↑(Set.Icc 0 T)) : ℝ

Energy derivative, given by integerEnergyProduction m (U.velocity t) (U.derivative t).

Equations

• U.energyDerivative m t = EulerOrdinarySobolev.integerEnergyProduction m (U.velocity t) (U.derivative t)

theorem EulerOrdinarySobolev.RegularizedEvolution.energy_time {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (m : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (U.energy m)) (U.energyDerivative m t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.RegularizedEvolution.energy_tame {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (t : ↑(Set.Icc 0 T)) (hM : WordBound 3 M (U.velocity t)) : U.energyDerivative m t ≤ tameEnergyConstant m * M * (U.energy m) t

theorem EulerOrdinarySobolev.RegularizedEvolution.energy_quadratic {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (t : ↑(Set.Icc 0 T)) : U.energyDerivative 3 t ≤ tameEnergyConstant 3 * (1 + (U.energy 3) t) ^ 2

theorem EulerOrdinarySobolev.RegularizedEvolution.short_energy {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (hsmall : tameEnergyConstant 3 * T ≤ (1 + (U.energy 3) ⟨0, ⋯⟩)⁻¹ / 2) (t : ↑(Set.Icc 0 T)) : (U.energy 3) t ≤ 2 * (U.energy 3) ⟨0, ⋯⟩ + 1

theorem EulerOrdinarySobolev.RegularizedEvolution.energy_uniform {S : SmoothingOperator} {T : ℝ} {hT : 0 ≤ T} (U : RegularizedEvolution S T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 3 M (U.velocity t)) (t : ↑(Set.Icc 0 T)) : wordEnergy m (U.velocity t) ≤ wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * M * T)

noncomputable def EulerOrdinarySobolev.regularizedTime (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Regularized time, given by (2*(1+tameEnergyConstant 3)*(1+wordEnergy 3 A))⁻¹.

Equations

• EulerOrdinarySobolev.regularizedTime A = (2 * (1 + EulerOrdinarySobolev.tameEnergyConstant 3) * (1 + EulerOrdinarySobolev.wordEnergy 3 A))⁻¹

theorem EulerOrdinarySobolev.regularizedTime_pos (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : 0 < regularizedTime A

noncomputable def EulerOrdinarySobolev.regularizedH3 (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : ℝ

Regularized H3, given by Real.sqrt (2*wordEnergy 3 A+1).

Equations

• EulerOrdinarySobolev.regularizedH3 A = √(2 * EulerOrdinarySobolev.wordEnergy 3 A + 1)

theorem EulerOrdinarySobolev.regularized_h3 (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {S : SmoothingOperator} (U : RegularizedEvolution S (regularizedTime A) ⋯) (hinit : U.velocity ⟨0, ⋯⟩ = A) (t : ↑(Set.Icc 0 (regularizedTime A))) : WordBound 3 (regularizedH3 A) (U.velocity t)

theorem EulerOrdinarySobolev.regularized_all_order (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : ∃ (C : ℝ), ∀ (S : SmoothingOperator) (U : RegularizedEvolution S (regularizedTime A) ⋯), U.velocity ⟨0, ⋯⟩ = A → ∀ (t : ↑(Set.Icc 0 (regularizedTime A))), tensorNorm q (U.velocity t) ≤ C

noncomputable def EulerOrdinarySobolev.RegularizedEvolution.derivativePath {T : ℝ} {hT : 0 ≤ T} {S : SmoothingOperator} (U : RegularizedEvolution S T hT) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Derivative path, given by fieldPath U.derivative U.derivative_continuous.

Equations

• U.derivativePath = EulerOrdinarySobolev.fieldPath U.derivative ⋯

theorem EulerOrdinarySobolev.RegularizedEvolution.integral_equation {T : ℝ} {hT : 0 ≤ T} {S : SmoothingOperator} (U : RegularizedEvolution S T hT) (t : ↑(Set.Icc 0 T)) : (U.velocity t).toLp = (U.velocity ⟨0, ⋯⟩).toLp + ((EulerContinuousTimeIntegral.integral T hT) U.derivativePath) t

theorem EulerOrdinarySobolev.SmoothLimitData.regularized_solenoidal {T : ℝ} {hT : 0 ≤ T} {U : (n : ℕ) → RegularizedEvolution (regularizer n) T hT} (L : SmoothLimitData (fun (n : ℕ) => (U n).velocity) ⋯) (t : ↑(Set.Icc 0 T)) : (L.field t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerOrdinarySobolev.SmoothLimitData.regularized_derivative_convergence {T : ℝ} {hT : 0 ≤ T} {U : (n : ℕ) → RegularizedEvolution (regularizer n) T hT} (L : SmoothLimitData (fun (n : ℕ) => (U n).velocity) ⋯) (M : ℝ) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), WordBound 4 M ((U n).velocity t)) : Filter.Tendsto (fun (n : ℕ) => (U n).derivativePath) Filter.atTop (nhds (projectedRhsPath L.field ⋯))

theorem EulerOrdinarySobolev.SmoothLimitData.regularized_integral_equation {T : ℝ} {hT : 0 ≤ T} {U : (n : ℕ) → RegularizedEvolution (regularizer n) T hT} (L : SmoothLimitData (fun (n : ℕ) => (U n).velocity) ⋯) (M : ℝ) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), WordBound 4 M ((U n).velocity t)) (t : ↑(Set.Icc 0 T)) : (L.field t).toLp = (L.field ⟨0, ⋯⟩).toLp + ((EulerContinuousTimeIntegral.integral T hT) (projectedRhsPath L.field ⋯)) t

theorem EulerOrdinarySobolev.SmoothLimitData.regularized_time {T : ℝ} {hT : 0 ≤ T} {U : (n : ℕ) → RegularizedEvolution (regularizer n) T hT} (L : SmoothLimitData (fun (n : ℕ) => (U n).velocity) ⋯) (M : ℝ) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), WordBound 4 M ((U n).velocity t)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => (L.field (Set.projIcc 0 T hT r)).toLp) (projectedRhs (L.field t)).toLp (Set.Icc 0 T) ↑t

noncomputable def EulerOrdinarySobolev.SmoothLimitData.regularizedEvolution {T : ℝ} {hT : 0 ≤ T} {U : (n : ℕ) → RegularizedEvolution (regularizer n) T hT} (L : SmoothLimitData (fun (n : ℕ) => (U n).velocity) ⋯) (M : ℝ) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), WordBound 4 M ((U n).velocity t)) : Evolution T hT

Regularized evolution, bundling velocity, pressureForce, velocity_continuous, pressure_continuous and the required compatibility proofs.

Equations

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

noncomputable def EulerOrdinarySobolev.regularizedSolution (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (n : ℕ) : RegularizedEvolution (regularizer n) (regularizedTime A) ⋯

Regularized solution, given by Classical.choose ((regularizer n).exists_smooth (regularizedTime A) (regularizedTime_pos A).le A hA).

Equations

• EulerOrdinarySobolev.regularizedSolution A hA n = Classical.choose ⋯

theorem EulerOrdinarySobolev.regularizedSolution_initial (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (n : ℕ) : (regularizedSolution A hA n).velocity ⟨0, ⋯⟩ = A

theorem EulerOrdinarySobolev.regularizedSolution_bounds (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (q : ℕ) : ∃ (M : ℝ), ∀ (n : ℕ) (t : ↑(Set.Icc 0 (regularizedTime A))), tensorNorm q ((regularizedSolution A hA n).velocity t) ≤ M

theorem EulerOrdinarySobolev.regularizedSolution_cauchy (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) : CauchySeq fun (n : ℕ) => fieldPath (regularizedSolution A hA n).velocity ⋯

noncomputable def EulerOrdinarySobolev.localLimit (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) : SmoothLimitData (fun (n : ℕ) => (regularizedSolution A hA n).velocity) ⋯

Local limit, given by smoothLimitData (regularizedTime_pos A).le _ _ (regularizedSolution_bounds A hA) (regularizedSolution_cauchy A hA).

Equations

• EulerOrdinarySobolev.localLimit A hA = EulerOrdinarySobolev.smoothLimitData ⋯ (fun (n : ℕ) => (EulerOrdinarySobolev.regularizedSolution A hA n).velocity) ⋯ ⋯ ⋯

noncomputable def EulerOrdinarySobolev.localEvolution (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) : Evolution (regularizedTime A) ⋯

Local evolution, choosing the witness provided by regularizedSolution_bounds.

Equations

• EulerOrdinarySobolev.localEvolution A hA = (EulerOrdinarySobolev.localLimit A hA).regularizedEvolution (Classical.choose ⋯) ⋯

theorem EulerOrdinarySobolev.localEvolution_initial (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) : (localEvolution A hA).velocity ⟨0, ⋯⟩ = A

theorem EulerOrdinarySobolev.exists_local_evolution (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) : ∃ (T : ℝ) (hT : 0 < T) (U : Evolution T ⋯), U.velocity ⟨0, ⋯⟩ = A