Cartesian Navier--Stokes residual in regular axisymmetric coordinates

Every derivative below is an ordinary Fréchet derivative. The coordinate is s=(x₀²+x₁²)/2, so none of the formulas divide by the cylindrical radius.

noncomputable def NavierStokes.AxisymmetricResidual.pack (a b c : ℝ) : ProblemStatement.Space

Pack, given by a • coordinateVector 0 + b • coordinateVector 1 + c • coordinateVector 2.

Equations

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

@[simp]

theorem NavierStokes.AxisymmetricResidual.pack_zero (a b c : ℝ) : (pack a b c).ofLp 0 = a

@[simp]

theorem NavierStokes.AxisymmetricResidual.pack_one (a b c : ℝ) : (pack a b c).ofLp 1 = b

@[simp]

theorem NavierStokes.AxisymmetricResidual.pack_two (a b c : ℝ) : (pack a b c).ofLp 2 = c

noncomputable def NavierStokes.AxisymmetricResidual.packDerivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b c : E →L[ℝ] ℝ) : E →L[ℝ] ProblemStatement.Space

Pack derivative, given by `a.smulRight (coordinateVector 0) + b.smulRight (coordinateVector

1. • c.smulRight (coordinateVector 2)`.

Equations

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

@[simp]

theorem NavierStokes.AxisymmetricResidual.packDerivative_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b c : E →L[ℝ] ℝ) (v : E) : (packDerivative a b c) v = pack (a v) (b v) (c v)

theorem NavierStokes.AxisymmetricResidual.hasFDerivAt_pack {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b c : E → ℝ} {da db dc : E →L[ℝ] ℝ} {x : E} (ha : HasFDerivAt a da x) (hb : HasFDerivAt b db x) (hc : HasFDerivAt c dc x) : HasFDerivAt (fun (y : E) => pack (a y) (b y) (c y)) (packDerivative da db dc) x

theorem NavierStokes.AxisymmetricResidual.fderiv_pack_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b c : E → ℝ} {x : E} (ha : DifferentiableAt ℝ a x) (hb : DifferentiableAt ℝ b x) (hc : DifferentiableAt ℝ c x) (v : E) : (fderiv ℝ (fun (y : E) => pack (a y) (b y) (c y)) x) v = pack ((fderiv ℝ a x) v) ((fderiv ℝ b x) v) ((fderiv ℝ c x) v)

noncomputable def NavierStokes.AxisymmetricResidual.direction (g : ProblemStatement.Space → ℝ) (i : Fin 3) (x : ProblemStatement.Space) : ℝ

Direction, given by fderiv ℝ g x (coordinateVector i).

Equations

• NavierStokes.AxisymmetricResidual.direction g i x = (fderiv ℝ g x) (NavierStokes.ProblemStatement.coordinateVector i)

noncomputable def NavierStokes.AxisymmetricResidual.scalarLaplacian (g : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : ℝ

Scalar laplacian, given by ∑ i : Fin 3, direction (fun y => direction g i y) i x.

Equations

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

noncomputable def NavierStokes.AxisymmetricResidual.vectorLaplacian (g : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ProblemStatement.Space

Vector laplacian, given by ∑ i : Fin 3, fderiv ℝ (fun y => fderiv ℝ g y (coordinateVector i)) x (coordinateVector i).

Equations

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

theorem NavierStokes.AxisymmetricResidual.contDiff_direction {g : ProblemStatement.Space → ℝ} {m n : WithTop ℕ∞} (hg : ContDiff ℝ n g) (hmn : m + 1 ≤ n) (i : Fin 3) : ContDiff ℝ m fun (x : ProblemStatement.Space) => direction g i x

theorem NavierStokes.AxisymmetricResidual.direction_add {a b : ProblemStatement.Space → ℝ} (ha : Differentiable ℝ a) (hb : Differentiable ℝ b) (i : Fin 3) (x : ProblemStatement.Space) : direction (fun (y : ProblemStatement.Space) => a y + b y) i x = direction a i x + direction b i x

theorem NavierStokes.AxisymmetricResidual.direction_sub {a b : ProblemStatement.Space → ℝ} (ha : Differentiable ℝ a) (hb : Differentiable ℝ b) (i : Fin 3) (x : ProblemStatement.Space) : direction (fun (y : ProblemStatement.Space) => a y - b y) i x = direction a i x - direction b i x

theorem NavierStokes.AxisymmetricResidual.direction_neg (a : ProblemStatement.Space → ℝ) (i : Fin 3) (x : ProblemStatement.Space) : direction (fun (y : ProblemStatement.Space) => -a y) i x = -direction a i x

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_add {a b : ProblemStatement.Space → ℝ} (ha : ContDiff ℝ 2 a) (hb : ContDiff ℝ 2 b) (x : ProblemStatement.Space) : scalarLaplacian (fun (y : ProblemStatement.Space) => a y + b y) x = scalarLaplacian a x + scalarLaplacian b x

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_sub {a b : ProblemStatement.Space → ℝ} (ha : ContDiff ℝ 2 a) (hb : ContDiff ℝ 2 b) (x : ProblemStatement.Space) : scalarLaplacian (fun (y : ProblemStatement.Space) => a y - b y) x = scalarLaplacian a x - scalarLaplacian b x

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_neg (a : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : scalarLaplacian (fun (y : ProblemStatement.Space) => -a y) x = -scalarLaplacian a x

theorem NavierStokes.AxisymmetricResidual.direction_coord_mul {g : ProblemStatement.Space → ℝ} (hg : Differentiable ℝ g) (i j : Fin 3) (x : ProblemStatement.Space) : direction (fun (y : ProblemStatement.Space) => y.ofLp i * g y) j x = (ProblemStatement.coordinateVector j).ofLp i * g x + x.ofLp i * direction g j x

theorem NavierStokes.AxisymmetricResidual.second_direction_coord_mul {g : ProblemStatement.Space → ℝ} (hg : ContDiff ℝ 2 g) (i j : Fin 3) (x : ProblemStatement.Space) : direction (fun (y : ProblemStatement.Space) => direction (fun (z : ProblemStatement.Space) => z.ofLp i * g z) j y) j x = 2 * (ProblemStatement.coordinateVector j).ofLp i * direction g j x + x.ofLp i * direction (fun (y : ProblemStatement.Space) => direction g j y) j x

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_coord_mul {g : ProblemStatement.Space → ℝ} (hg : ContDiff ℝ 2 g) (i : Fin 3) (x : ProblemStatement.Space) : scalarLaplacian (fun (y : ProblemStatement.Space) => y.ofLp i * g y) x = x.ofLp i * scalarLaplacian g x + 2 * direction g i x

theorem NavierStokes.AxisymmetricResidual.vectorLaplacian_pack {a b c : ProblemStatement.Space → ℝ} (ha : ContDiff ℝ 2 a) (hb : ContDiff ℝ 2 b) (hc : ContDiff ℝ 2 c) (x : ProblemStatement.Space) : vectorLaplacian (fun (y : ProblemStatement.Space) => pack (a y) (b y) (c y)) x = pack (scalarLaplacian a x) (scalarLaplacian b x) (scalarLaplacian c x)

noncomputable def NavierStokes.AxisymmetricResidual.lift (G : AxisymmetricFields.Profile) (t : ℝ) (x : ProblemStatement.Space) : ℝ

Lift, given by G (profilePoint t x).

Equations

• NavierStokes.AxisymmetricResidual.lift G t x = G (NavierStokes.AxisymmetricFields.profilePoint t x)

def NavierStokes.AxisymmetricResidual.SliceDifferentiable (G : AxisymmetricFields.Profile) (t : ℝ) : Prop

Joint differentiability is needed only along the spatial slice being evaluated.

Equations

• NavierStokes.AxisymmetricResidual.SliceDifferentiable G t = ∀ (x : NavierStokes.ProblemStatement.Space), DifferentiableAt ℝ G (NavierStokes.AxisymmetricFields.profilePoint t x)

def NavierStokes.AxisymmetricResidual.SliceC2 (G : AxisymmetricFields.Profile) (t : ℝ) : Prop

No smooth extension across the singular time is required by this hypothesis.

Equations

• NavierStokes.AxisymmetricResidual.SliceC2 G t = ∀ (x : NavierStokes.ProblemStatement.Space), ContDiffAt ℝ 2 G (NavierStokes.AxisymmetricFields.profilePoint t x)

theorem NavierStokes.AxisymmetricResidual.SliceC2.differentiable {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceC2 G t) : SliceDifferentiable G t

theorem NavierStokes.AxisymmetricResidual.sliceC2_of_contDiffOn {G : AxisymmetricFields.Profile} {times : Set ℝ} {t : ℝ} (hG : ContDiffOn ℝ 2 G (times ×ˢ Set.univ)) (ht : times ∈ nhds t) : SliceC2 G t

theorem NavierStokes.AxisymmetricResidual.contDiff_lift_slice {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceC2 G t) : ContDiff ℝ 2 (lift G t)

noncomputable def NavierStokes.AxisymmetricResidual.partialT (G : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Partial T, given by fderiv ℝ G p (1, (0, 0)).

Equations

• NavierStokes.AxisymmetricResidual.partialT G p = (fderiv ℝ G p) (1, 0, 0)

noncomputable def NavierStokes.AxisymmetricResidual.laplaceScalar (G : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Laplace scalar, given by 2 * p.2.1 * partialS (partialS G) p + 2 * partialS G p + partialZ (partialZ G) p.

Equations

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

noncomputable def NavierStokes.AxisymmetricResidual.laplaceWeighted (G : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Laplace weighted, given by 2 * p.2.1 * partialS (partialS G) p + 4 * partialS G p + partialZ (partialZ G) p.

Equations

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

theorem NavierStokes.AxisymmetricResidual.contDiff_lift {G : AxisymmetricFields.Profile} {n : WithTop ℕ∞} (hG : ContDiff ℝ n G) (t : ℝ) : ContDiff ℝ n (lift G t)

theorem NavierStokes.AxisymmetricResidual.contDiff_partialS {G : AxisymmetricFields.Profile} {m n : WithTop ℕ∞} (hG : ContDiff ℝ n G) (hmn : m + 1 ≤ n) : ContDiff ℝ m (AxisymmetricFields.partialS G)

theorem NavierStokes.AxisymmetricResidual.contDiff_partialZ {G : AxisymmetricFields.Profile} {m n : WithTop ℕ∞} (hG : ContDiff ℝ n G) (hmn : m + 1 ≤ n) : ContDiff ℝ m (AxisymmetricFields.partialZ G)

theorem NavierStokes.AxisymmetricResidual.fderiv_lift_apply {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceDifferentiable G t) (x v : ProblemStatement.Space) : (fderiv ℝ (lift G t) x) v = (x.ofLp 0 * v.ofLp 0 + x.ofLp 1 * v.ofLp 1) * AxisymmetricFields.partialS G (AxisymmetricFields.profilePoint t x) + v.ofLp 2 * AxisymmetricFields.partialZ G (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.AxisymmetricResidual.direction_lift_zero {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceDifferentiable G t) (x : ProblemStatement.Space) : direction (lift G t) 0 x = x.ofLp 0 * lift (AxisymmetricFields.partialS G) t x

theorem NavierStokes.AxisymmetricResidual.direction_lift_one {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceDifferentiable G t) (x : ProblemStatement.Space) : direction (lift G t) 1 x = x.ofLp 1 * lift (AxisymmetricFields.partialS G) t x

theorem NavierStokes.AxisymmetricResidual.direction_lift_two {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceDifferentiable G t) (x : ProblemStatement.Space) : direction (lift G t) 2 x = lift (AxisymmetricFields.partialZ G) t x

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_lift {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceC2 G t) (x : ProblemStatement.Space) : scalarLaplacian (lift G t) x = laplaceScalar G (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_weighted_zero {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceC2 G t) (x : ProblemStatement.Space) : scalarLaplacian (fun (y : ProblemStatement.Space) => y.ofLp 0 * lift G t y) x = x.ofLp 0 * laplaceWeighted G (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.AxisymmetricResidual.scalarLaplacian_weighted_one {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceC2 G t) (x : ProblemStatement.Space) : scalarLaplacian (fun (y : ProblemStatement.Space) => y.ofLp 1 * lift G t y) x = x.ofLp 1 * laplaceWeighted G (AxisymmetricFields.profilePoint t x)

noncomputable def NavierStokes.AxisymmetricResidual.componentX (B F : AxisymmetricFields.Profile) (t : ℝ) (x : ProblemStatement.Space) : ℝ

Component X, given by -(x 0 * lift B t x + x 1 * lift F t x).

Equations

• NavierStokes.AxisymmetricResidual.componentX B F t x = -(x.ofLp 0 * NavierStokes.AxisymmetricResidual.lift B t x + x.ofLp 1 * NavierStokes.AxisymmetricResidual.lift F t x)

noncomputable def NavierStokes.AxisymmetricResidual.componentY (B F : AxisymmetricFields.Profile) (t : ℝ) (x : ProblemStatement.Space) : ℝ

Component Y, given by x 0 * lift F t x - x 1 * lift B t x.

Equations

• NavierStokes.AxisymmetricResidual.componentY B F t x = x.ofLp 0 * NavierStokes.AxisymmetricResidual.lift F t x - x.ofLp 1 * NavierStokes.AxisymmetricResidual.lift B t x

noncomputable def NavierStokes.AxisymmetricResidual.velocity (B F U : AxisymmetricFields.Profile) : ProblemStatement.VelocityField

Convention: radial velocity -r B, angular velocity r F, axial velocity U.

Equations

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

noncomputable def NavierStokes.AxisymmetricResidual.pressure (P : AxisymmetricFields.Profile) : ProblemStatement.PressureField

Pressure, defined pointwise by lift P w.1 w.2.

Equations

• NavierStokes.AxisymmetricResidual.pressure P w = NavierStokes.AxisymmetricResidual.lift P w.1 w.2

noncomputable def NavierStokes.AxisymmetricResidual.velocityJacobian (B F U : AxisymmetricFields.Profile) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Velocity jacobian, constructed using packDerivative.

Equations

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

theorem NavierStokes.AxisymmetricResidual.hasFDerivAt_velocity {B F U : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceDifferentiable B t) (hF : SliceDifferentiable F t) (hU : SliceDifferentiable U t) (x : ProblemStatement.Space) : HasFDerivAt (fun (y : ProblemStatement.Space) => velocity B F U (t, y)) (velocityJacobian B F U t x) x

noncomputable def NavierStokes.AxisymmetricResidual.advectionRadial (B F U : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Advection radial, given by (B p) ^ 2 - (F p) ^ 2 + 2 * p.2.1 * B p * partialS B p - U p * partialZ B p.

Equations

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

noncomputable def NavierStokes.AxisymmetricResidual.advectionAngular (B F U : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Advection angular, given by 2 * B p * F p + 2 * p.2.1 * B p * partialS F p - U p * partialZ F p.

Equations

• NavierStokes.AxisymmetricResidual.advectionAngular B F U p = 2 * B p * F p + 2 * p.2.1 * B p * NavierStokes.AxisymmetricFields.partialS F p - U p * NavierStokes.AxisymmetricFields.partialZ F p

noncomputable def NavierStokes.AxisymmetricResidual.advectionAxial (B U : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Advection axial, given by -2 * p.2.1 * B p * partialS U p + U p * partialZ U p.

Equations

• NavierStokes.AxisymmetricResidual.advectionAxial B U p = -2 * p.2.1 * B p * NavierStokes.AxisymmetricFields.partialS U p + U p * NavierStokes.AxisymmetricFields.partialZ U p

theorem NavierStokes.AxisymmetricResidual.advection_velocity {B F U : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceDifferentiable B t) (hF : SliceDifferentiable F t) (hU : SliceDifferentiable U t) (x : ProblemStatement.Space) : ProblemStatement.advection (velocity B F U) t x = pack (x.ofLp 0 * advectionRadial B F U (AxisymmetricFields.profilePoint t x) + x.ofLp 1 * advectionAngular B F U (AxisymmetricFields.profilePoint t x)) (x.ofLp 1 * advectionRadial B F U (AxisymmetricFields.profilePoint t x) - x.ofLp 0 * advectionAngular B F U (AxisymmetricFields.profilePoint t x)) (advectionAxial B U (AxisymmetricFields.profilePoint t x))

theorem NavierStokes.AxisymmetricResidual.divergence_velocity {B F U : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceDifferentiable B t) (hF : SliceDifferentiable F t) (hU : SliceDifferentiable U t) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (velocity B F U) t x = AxisymmetricFields.partialZ U (AxisymmetricFields.profilePoint t x) - 2 * B (AxisymmetricFields.profilePoint t x) - 2 * AxisymmetricFields.radialEnergy x * AxisymmetricFields.partialS B (AxisymmetricFields.profilePoint t x)

theorem NavierStokes.AxisymmetricResidual.spatialLaplacian_velocity {B F U : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceC2 B t) (hF : SliceC2 F t) (hU : SliceC2 U t) (x : ProblemStatement.Space) : ProblemStatement.spatialLaplacian (velocity B F U) t x = pack (-x.ofLp 0 * laplaceWeighted B (AxisymmetricFields.profilePoint t x) - x.ofLp 1 * laplaceWeighted F (AxisymmetricFields.profilePoint t x)) (-x.ofLp 1 * laplaceWeighted B (AxisymmetricFields.profilePoint t x) + x.ofLp 0 * laplaceWeighted F (AxisymmetricFields.profilePoint t x)) (laplaceScalar U (AxisymmetricFields.profilePoint t x))

theorem NavierStokes.AxisymmetricResidual.pressureGradient_pressure {P : AxisymmetricFields.Profile} {t : ℝ} (hP : SliceDifferentiable P t) (x : ProblemStatement.Space) : ProblemStatement.pressureGradient (pressure P) t x = pack (x.ofLp 0 * AxisymmetricFields.partialS P (AxisymmetricFields.profilePoint t x)) (x.ofLp 1 * AxisymmetricFields.partialS P (AxisymmetricFields.profilePoint t x)) (AxisymmetricFields.partialZ P (AxisymmetricFields.profilePoint t x))

def NavierStokes.AxisymmetricResidual.timeProfileJacobian : ℝ →L[ℝ] AxisymmetricFields.ProfilePoint

Time profile jacobian, given by (ContinuousLinearMap.id ℝ ℝ).prod (0 : ℝ →L[ℝ] ℝ × ℝ).

Equations

• NavierStokes.AxisymmetricResidual.timeProfileJacobian = (ContinuousLinearMap.id ℝ ℝ).prod 0

noncomputable def NavierStokes.AxisymmetricResidual.timeProfileDerivative (G : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ →L[ℝ] ℝ

Time profile derivative, given by (fderiv ℝ G p).comp timeProfileJacobian.

Equations

• NavierStokes.AxisymmetricResidual.timeProfileDerivative G p = fderiv ℝ G p ∘SL NavierStokes.AxisymmetricResidual.timeProfileJacobian

@[simp]

theorem NavierStokes.AxisymmetricResidual.timeProfileDerivative_one (G : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : (timeProfileDerivative G p) 1 = partialT G p

theorem NavierStokes.AxisymmetricResidual.hasFDerivAt_time_lift {G : AxisymmetricFields.Profile} {t : ℝ} (hG : SliceDifferentiable G t) (x : ProblemStatement.Space) : HasFDerivAt (fun (s : ℝ) => lift G s x) (timeProfileDerivative G (AxisymmetricFields.profilePoint t x)) t

theorem NavierStokes.AxisymmetricResidual.temporalDerivative_velocity {B F U : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceDifferentiable B t) (hF : SliceDifferentiable F t) (hU : SliceDifferentiable U t) (x : ProblemStatement.Space) : ProblemStatement.temporalDerivative (velocity B F U) t x = pack (-x.ofLp 0 * partialT B (AxisymmetricFields.profilePoint t x) - x.ofLp 1 * partialT F (AxisymmetricFields.profilePoint t x)) (-x.ofLp 1 * partialT B (AxisymmetricFields.profilePoint t x) + x.ofLp 0 * partialT F (AxisymmetricFields.profilePoint t x)) (partialT U (AxisymmetricFields.profilePoint t x))

noncomputable def NavierStokes.AxisymmetricResidual.residualRadial (B F U P : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Residual radial, given by -partialT B p + advectionRadial B F U p + laplaceWeighted B p + partialS P p.

Equations

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

noncomputable def NavierStokes.AxisymmetricResidual.residualAngular (B F U : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Residual angular, given by -partialT F p + advectionAngular B F U p + laplaceWeighted F p.

Equations

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

noncomputable def NavierStokes.AxisymmetricResidual.residualAxial (B U P : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

Residual axial, given by partialT U p + advectionAxial B U p - laplaceScalar U p + partialZ P p.

Equations

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

theorem NavierStokes.AxisymmetricResidual.navierStokesResidual_velocity {B F U P : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceC2 B t) (hF : SliceC2 F t) (hU : SliceC2 U t) (hP : SliceDifferentiable P t) (x : ProblemStatement.Space) : ProblemStatement.navierStokesResidual (velocity B F U) (pressure P) t x = pack (x.ofLp 0 * residualRadial B F U P (AxisymmetricFields.profilePoint t x) + x.ofLp 1 * residualAngular B F U (AxisymmetricFields.profilePoint t x)) (x.ofLp 1 * residualRadial B F U P (AxisymmetricFields.profilePoint t x) - x.ofLp 0 * residualAngular B F U (AxisymmetricFields.profilePoint t x)) (residualAxial B U P (AxisymmetricFields.profilePoint t x))

Exact physical Navier--Stokes residual, at viscosity one, including radial, angular, and axial viscosity. Its hypotheses need no continuation past time t.

theorem NavierStokes.AxisymmetricResidual.navierStokesResidual_on_axis {B F U P : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceC2 B t) (hF : SliceC2 F t) (hU : SliceC2 U t) (hP : SliceDifferentiable P t) (x : ProblemStatement.Space) (hx0 : x.ofLp 0 = 0) (hx1 : x.ofLp 1 = 0) : ProblemStatement.navierStokesResidual (velocity B F U) (pressure P) t x = residualAxial B U P (t, 0, x.ofLp 2) • ProblemStatement.coordinateVector 2

theorem NavierStokes.AxisymmetricResidual.navierStokesResidual_eq_zero {B F U P : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceC2 B t) (hF : SliceC2 F t) (hU : SliceC2 U t) (hP : SliceDifferentiable P t) (x : ProblemStatement.Space) (hr : residualRadial B F U P (AxisymmetricFields.profilePoint t x) = 0) (ha : residualAngular B F U (AxisymmetricFields.profilePoint t x) = 0) (hz : residualAxial B U P (AxisymmetricFields.profilePoint t x) = 0) : ProblemStatement.navierStokesResidual (velocity B F U) (pressure P) t x = 0

The three explicit coefficient equations imply the actual Cartesian PDE.

noncomputable def NavierStokes.AxisymmetricResidual.fromPotentialB (H : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

From potential B, given by partialZ H p / 2.

Equations

• NavierStokes.AxisymmetricResidual.fromPotentialB H p = NavierStokes.AxisymmetricFields.partialZ H p / 2

noncomputable def NavierStokes.AxisymmetricResidual.fromPotentialF (K : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

From potential F, given by -partialS K p.

Equations

• NavierStokes.AxisymmetricResidual.fromPotentialF K p = -NavierStokes.AxisymmetricFields.partialS K p

noncomputable def NavierStokes.AxisymmetricResidual.fromPotentialU (H : AxisymmetricFields.Profile) (p : AxisymmetricFields.ProfilePoint) : ℝ

From potential U, given by H p + p.2.1 * partialS H p.

Equations

• NavierStokes.AxisymmetricResidual.fromPotentialU H p = H p + p.2.1 * NavierStokes.AxisymmetricFields.partialS H p

theorem NavierStokes.AxisymmetricResidual.velocity_from_potential_at (H K : AxisymmetricFields.Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : DifferentiableAt ℝ H (AxisymmetricFields.profilePoint t x)) (hK : DifferentiableAt ℝ K (AxisymmetricFields.profilePoint t x)) : AxisymmetricFields.velocity H K (t, x) = velocity (fromPotentialB H) (fromPotentialF K) (fromPotentialU H) (t, x)

Connect the residual convention to the already constructed curl field.

theorem NavierStokes.AxisymmetricResidual.velocity_from_potential {H K : AxisymmetricFields.Profile} (hH : Differentiable ℝ H) (hK : Differentiable ℝ K) : AxisymmetricFields.velocity H K = velocity (fromPotentialB H) (fromPotentialF K) (fromPotentialU H)

theorem NavierStokes.AxisymmetricResidual.divergence_velocity_eq_zero {B F U : AxisymmetricFields.Profile} {t : ℝ} (hB : SliceDifferentiable B t) (hF : SliceDifferentiable F t) (hU : SliceDifferentiable U t) (x : ProblemStatement.Space) (h : AxisymmetricFields.partialZ U (AxisymmetricFields.profilePoint t x) = 2 * B (AxisymmetricFields.profilePoint t x) + 2 * AxisymmetricFields.radialEnergy x * AxisymmetricFields.partialS B (AxisymmetricFields.profilePoint t x)) : ProblemStatement.spatialDivergence (velocity B F U) t x = 0