The classical Euler equation supplies strong evolution in every Sobolev norm once the actual velocity and pressure-gradient L² jets are continuous. The advection field and its regularity are constructed here.

noncomputable def EulerSmoothEulerEvolution.advection {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (U : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : K) => (U t).jetLp n) (t : K) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Advection, given by product (coefficientPath (fun s => (U s).derivative) (continuous_jetLp_derivative U hU)) t (U t).

Equations

• EulerSmoothEulerEvolution.advection U hU t = EulerLpSmoothCoefficientProduct.product (EulerMeanSobolevBoundedField.coefficientPath (fun (s : K) => (U s).derivative) ⋯) t (U t)

theorem EulerSmoothEulerEvolution.advection_field {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (U : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : K) => (U t).jetLp n) (t : K) (x : EulerSmoothLimit.Space) : (advection U hU t).field x = (fderiv ℝ (U t).field x) ((U t).field x)

theorem EulerSmoothEulerEvolution.advection_jet_continuous {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (U : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : K) => (U t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (advection U hU t).jetLp n

noncomputable def EulerSmoothEulerEvolution.rhs {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (U : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : K) => (U t).jetLp n) (G : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (t : K) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Rhs, given by mapField (-(ContinuousLinearMap.id ℝ Space)) (addField (advection U hU t) (G t)).

Equations

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

theorem EulerSmoothEulerEvolution.rhs_field {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (U : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : K) => (U t).jetLp n) (G : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (t : K) (x : EulerSmoothLimit.Space) : (rhs U hU G t).field x = -(fderiv ℝ (U t).field x) ((U t).field x) - (G t).field x

theorem EulerSmoothEulerEvolution.rhs_jet_continuous {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (U : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : K) => (U t).jetLp n) (G : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hG : ∀ (n : ℕ), Continuous fun (t : K) => (G t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (rhs U hU G t).jetLp n

theorem EulerSmoothEulerEvolution.sobolev_evolution (T : ℝ) (hT : 0 ≤ T) (U G : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (U t).jetLp n) (hG : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (G t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), HasDerivAt (fun (r : ℝ) => (U (Set.projIcc 0 T hT r)).field x) (-(fderiv ℝ (U ⟨t, ⋯⟩).field x) ((U ⟨t, ⋯⟩).field x) - (G ⟨t, ⋯⟩).field x) t) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath U hU q)) ((EulerSmoothFieldSobolevTime.sobolevPath (rhs U hU G) ⋯ q) t) (Set.Icc 0 T) ↑t

theorem EulerSmoothEulerEvolution.pointwise_time_derivative_of_classical (T : ℝ) (hT : 0 ≤ T) (U G : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hmatch : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), u (↑t, x) = (U t).field x) (hgradient : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = (G t).field x) (hdiff : ∀ t ∈ Set.Ioo 0 T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (heuler : ∀ t ∈ Set.Ioo 0 T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (r : ℝ) => (U (Set.projIcc 0 T hT r)).field x) (-(fderiv ℝ (U ⟨t, ⋯⟩).field x) ((U ⟨t, ⋯⟩).field x) - (G ⟨t, ⋯⟩).field x) t

theorem EulerSmoothEulerEvolution.sobolev_evolution_of_classical (T : ℝ) (hT : 0 ≤ T) (U G : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (U t).jetLp n) (hG : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (G t).jetLp n) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hmatch : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), u (↑t, x) = (U t).field x) (hgradient : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = (G t).field x) (hdiff : ∀ t ∈ Set.Ioo 0 T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (heuler : ∀ t ∈ Set.Ioo 0 T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath U hU q)) ((EulerSmoothFieldSobolevTime.sobolevPath (rhs U hU G) ⋯ q) t) (Set.Icc 0 T) ↑t