A suitable weak solution that is smooth on the unit cylinder is a classical solution #

Testing the weak momentum equation with ψ eₖ isolates its k-th component; integrating by parts back (in time, in space, and twice for the viscous term through the weak-gradient pairing identity) shows that the classical momentum residual integrates to zero against every test function supported in the cylinder, so it vanishes there. Together with the pointwise divergence equation this gives IsClassicalSolutionOn u p f unitCylinder, the passage from the weak to the classical equations used in the proof of lem:aniso:annulus.

source

theorem CIV.momentum_integrand_basisVec {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (k : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) :

-∑ i : Fin 3, u z i * CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => (fun (z' : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z' • CKN.basisVec k) w i) z - ∑ i : Fin 3, ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => (fun (z' : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z' • CKN.basisVec k) w i) j z + ∑ i : Fin 3, ∑ j : Fin 3, Du z i j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => (fun (z' : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z' • CKN.basisVec k) w i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => (fun (z' : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z' • CKN.basisVec k) w i) i z - ∑ i : Fin 3, f z i * (fun (z' : CKN.Foundation.Parabolic.Vec3 × ℝ) => ψ z' • CKN.basisVec k) z i = -(u z k * CKN.timePartial ψ z) - ∑ j : Fin 3, u z k * u z j * CKN.spatialPartial ψ j z + ∑ j : Fin 3, Du z k j * CKN.spatialPartial ψ j z - p z * CKN.spatialPartial ψ k z - f z k * ψ z

Testing with ψ eₖ collapses the weak momentum integrand to its k-th component.

source

theorem CIV.integrable_mul_spatialPartial_of_test {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) (j : Fin 3) :

MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z * CKN.spatialPartial ψ j z) MeasureTheory.volume

A function continuous on the unit cylinder times a spatial partial of a test function supported in the cylinder is integrable.

source

theorem CIV.integrable_mul_timePartial_of_test {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) :

MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z * CKN.timePartial ψ z) MeasureTheory.volume

A function continuous on the unit cylinder times the time partial of a test function supported in the cylinder is integrable.

source

theorem CIV.integrable_mul_of_test {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) :

MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z * ψ z) MeasureTheory.volume

A function continuous on the unit cylinder times a test function supported in the cylinder is integrable.

source

theorem CIV.spatialPartial_mul_of_mem_unitCylinder {a b : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (ha : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => a z) unitCylinder) (hb : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => b z) unitCylinder) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∈ unitCylinder) (j : Fin 3) :

CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => a w * b w) j z = CKN.spatialPartial a j z * b z + a z * CKN.spatialPartial b j z

The product rule for a spatial partial at a point of the unit cylinder.

source

theorem CIV.integral_convective_pairing {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hsupp : tsupport ψ ⊆ unitCylinder) (k j : Fin 3) :

∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), u z k * u z j * CKN.spatialPartial ψ j z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), (CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w k) j z * u z j + u z k * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z) * ψ z

The convective term: ∫ u_k u_j ∂ⱼψ = -∫ (∂ⱼu_k u_j + u_k ∂ⱼu_j) ψ.

source

∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), Du z k j * CKN.spatialPartial ψ j z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w k) j j z * ψ z

The viscous term: ∫ Du_{kj} ∂ⱼψ = -∫ ∂ⱼ∂ⱼu_k ψ.

source

theorem CIV.timePartial_test_eq_zero_of_notMem_tsupport {ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {z : CKN.Foundation.Parabolic.Vec3 × ℝ} (hz : z ∉ tsupport ψ) :

CKN.timePartial ψ z = 0

The time partial of a smooth function vanishes off its topological support.

source

∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), -(u z k * CKN.timePartial ψ z) - ∑ j : Fin 3, u z k * u z j * CKN.spatialPartial ψ j z + ∑ j : Fin 3, Du z k j * CKN.spatialPartial ψ j z - p z * CKN.spatialPartial ψ k z - f z k * ψ z = 0

The weak momentum equation tested with ψ eₖ, as a whole-space integral of the collapsed integrand.

source

∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), (CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w k) z + ∑ j : Fin 3, u z j * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w k) j z - ∑ j : Fin 3, CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w k) j j z + CKN.spatialPartial p k z - f z k) * ψ z = 0

The classical momentum residual of a suitable weak solution smooth on the unit cylinder integrates to zero against every test function supported in the cylinder.

source

IsClassicalSolutionOn u p f unitCylinder

A suitable weak solution on the unit cylinder whose velocity, pressure and force are smooth there is a classical solution there.

Documentation

LeanPool.CIVAxisymmetric.Prerequisites.Serrin.ClassicalBridge

A suitable weak solution that is smooth on the unit cylinder is a classical solution #