Local Cartesian residual formulas for axisymmetric profiles #
Only regularity at the evaluated profile point is required. The second derivative formulas use equality of germs of first derivatives, so they do not impose any condition on an unrelated profile point such as the axis.
theorem
NavierStokes.LocalAxisymmetricResidual.contDiffAt_direction
{g : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
{m n : WithTop ℕ∞}
(hg : ContDiffAt ℝ n g x)
(hmn : m + 1 ≤ n)
(i : Fin 3)
:
ContDiffAt ℝ m (fun (y : ProblemStatement.Space) => AxisymmetricResidual.direction g i y) x
theorem
NavierStokes.LocalAxisymmetricResidual.direction_congr
{a b : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(h : a =ᶠ[nhds x] b)
(i : Fin 3)
:
theorem
NavierStokes.LocalAxisymmetricResidual.direction_add
{a b : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(ha : DifferentiableAt ℝ a x)
(hb : DifferentiableAt ℝ b x)
(i : Fin 3)
:
AxisymmetricResidual.direction (fun (y : ProblemStatement.Space) => a y + b y) i x = AxisymmetricResidual.direction a i x + AxisymmetricResidual.direction b i x
theorem
NavierStokes.LocalAxisymmetricResidual.direction_sub
{a b : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(ha : DifferentiableAt ℝ a x)
(hb : DifferentiableAt ℝ b x)
(i : Fin 3)
:
AxisymmetricResidual.direction (fun (y : ProblemStatement.Space) => a y - b y) i x = AxisymmetricResidual.direction a i x - AxisymmetricResidual.direction b i x
theorem
NavierStokes.LocalAxisymmetricResidual.scalarLaplacian_add
{a b : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(ha : ContDiffAt ℝ 2 a x)
(hb : ContDiffAt ℝ 2 b x)
:
AxisymmetricResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => a y + b y) x = AxisymmetricResidual.scalarLaplacian a x + AxisymmetricResidual.scalarLaplacian b x
theorem
NavierStokes.LocalAxisymmetricResidual.scalarLaplacian_sub
{a b : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(ha : ContDiffAt ℝ 2 a x)
(hb : ContDiffAt ℝ 2 b x)
:
AxisymmetricResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => a y - b y) x = AxisymmetricResidual.scalarLaplacian a x - AxisymmetricResidual.scalarLaplacian b x
theorem
NavierStokes.LocalAxisymmetricResidual.direction_coord_mul
{g : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(hg : DifferentiableAt ℝ g x)
(i j : Fin 3)
:
AxisymmetricResidual.direction (fun (y : ProblemStatement.Space) => y.ofLp i * g y) j x = (ProblemStatement.coordinateVector j).ofLp i * g x + x.ofLp i * AxisymmetricResidual.direction g j x
theorem
NavierStokes.LocalAxisymmetricResidual.second_direction_coord_mul
{g : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(hg : ContDiffAt ℝ 2 g x)
(i j : Fin 3)
:
AxisymmetricResidual.direction
(fun (y : ProblemStatement.Space) =>
AxisymmetricResidual.direction (fun (z : ProblemStatement.Space) => z.ofLp i * g z) j y)
j x = 2 * (ProblemStatement.coordinateVector j).ofLp i * AxisymmetricResidual.direction g j x + x.ofLp i * AxisymmetricResidual.direction (fun (y : ProblemStatement.Space) => AxisymmetricResidual.direction g j y) j x
theorem
NavierStokes.LocalAxisymmetricResidual.scalarLaplacian_coord_mul
{g : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(hg : ContDiffAt ℝ 2 g x)
(i : Fin 3)
:
AxisymmetricResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => y.ofLp i * g y) x = x.ofLp i * AxisymmetricResidual.scalarLaplacian g x + 2 * AxisymmetricResidual.direction g i x
theorem
NavierStokes.LocalAxisymmetricResidual.vectorLaplacian_pack
{a b c : ProblemStatement.Space → ℝ}
{x : ProblemStatement.Space}
(ha : ContDiffAt ℝ 2 a x)
(hb : ContDiffAt ℝ 2 b x)
(hc : ContDiffAt ℝ 2 c x)
:
AxisymmetricResidual.vectorLaplacian (fun (y : ProblemStatement.Space) => AxisymmetricResidual.pack (a y) (b y) (c y))
x = AxisymmetricResidual.pack (AxisymmetricResidual.scalarLaplacian a x) (AxisymmetricResidual.scalarLaplacian b x)
(AxisymmetricResidual.scalarLaplacian c x)
theorem
NavierStokes.LocalAxisymmetricResidual.contDiffAt_lift
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
{n : WithTop ℕ∞}
(hG : ContDiffAt ℝ n G (AxisymmetricFields.profilePoint t x))
:
ContDiffAt ℝ n (AxisymmetricResidual.lift G t) x
theorem
NavierStokes.LocalAxisymmetricResidual.fderiv_lift_apply
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : DifferentiableAt ℝ G (AxisymmetricFields.profilePoint t x))
(v : ProblemStatement.Space)
:
(fderiv ℝ (AxisymmetricResidual.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.LocalAxisymmetricResidual.direction_lift_zero
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : DifferentiableAt ℝ G (AxisymmetricFields.profilePoint t x))
:
theorem
NavierStokes.LocalAxisymmetricResidual.direction_lift_one
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : DifferentiableAt ℝ G (AxisymmetricFields.profilePoint t x))
:
theorem
NavierStokes.LocalAxisymmetricResidual.direction_lift_two
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : DifferentiableAt ℝ G (AxisymmetricFields.profilePoint t x))
:
theorem
NavierStokes.LocalAxisymmetricResidual.scalarLaplacian_lift
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : ContDiffAt ℝ 2 G (AxisymmetricFields.profilePoint t x))
:
theorem
NavierStokes.LocalAxisymmetricResidual.scalarLaplacian_weighted_zero
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : ContDiffAt ℝ 2 G (AxisymmetricFields.profilePoint t x))
:
AxisymmetricResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => y.ofLp 0 * AxisymmetricResidual.lift G t y)
x = x.ofLp 0 * AxisymmetricResidual.laplaceWeighted G (AxisymmetricFields.profilePoint t x)
theorem
NavierStokes.LocalAxisymmetricResidual.scalarLaplacian_weighted_one
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : ContDiffAt ℝ 2 G (AxisymmetricFields.profilePoint t x))
:
AxisymmetricResidual.scalarLaplacian (fun (y : ProblemStatement.Space) => y.ofLp 1 * AxisymmetricResidual.lift G t y)
x = x.ofLp 1 * AxisymmetricResidual.laplaceWeighted G (AxisymmetricFields.profilePoint t x)
theorem
NavierStokes.LocalAxisymmetricResidual.hasFDerivAt_velocity
{B F U : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : DifferentiableAt ℝ B (AxisymmetricFields.profilePoint t x))
(hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint t x))
(hU : DifferentiableAt ℝ U (AxisymmetricFields.profilePoint t x))
:
HasFDerivAt (fun (y : ProblemStatement.Space) => AxisymmetricResidual.velocity B F U (t, y))
(AxisymmetricResidual.velocityJacobian B F U t x) x
The spatial Jacobian uses derivatives only at the evaluated profile point.
theorem
NavierStokes.LocalAxisymmetricResidual.advection_velocity
{B F U : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : DifferentiableAt ℝ B (AxisymmetricFields.profilePoint t x))
(hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint t x))
(hU : DifferentiableAt ℝ U (AxisymmetricFields.profilePoint t x))
:
ProblemStatement.advection (AxisymmetricResidual.velocity B F U) t x = AxisymmetricResidual.pack
(x.ofLp 0 * AxisymmetricResidual.advectionRadial B F U (AxisymmetricFields.profilePoint t x) + x.ofLp 1 * AxisymmetricResidual.advectionAngular B F U (AxisymmetricFields.profilePoint t x))
(x.ofLp 1 * AxisymmetricResidual.advectionRadial B F U (AxisymmetricFields.profilePoint t x) - x.ofLp 0 * AxisymmetricResidual.advectionAngular B F U (AxisymmetricFields.profilePoint t x))
(AxisymmetricResidual.advectionAxial B U (AxisymmetricFields.profilePoint t x))
theorem
NavierStokes.LocalAxisymmetricResidual.divergence_velocity
{B F U : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : DifferentiableAt ℝ B (AxisymmetricFields.profilePoint t x))
(hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint t x))
(hU : DifferentiableAt ℝ U (AxisymmetricFields.profilePoint t x))
:
ProblemStatement.spatialDivergence (AxisymmetricResidual.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.LocalAxisymmetricResidual.spatialLaplacian_velocity
{B F U : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : ContDiffAt ℝ 2 B (AxisymmetricFields.profilePoint t x))
(hF : ContDiffAt ℝ 2 F (AxisymmetricFields.profilePoint t x))
(hU : ContDiffAt ℝ 2 U (AxisymmetricFields.profilePoint t x))
:
ProblemStatement.spatialLaplacian (AxisymmetricResidual.velocity B F U) t x = AxisymmetricResidual.pack
(-x.ofLp 0 * AxisymmetricResidual.laplaceWeighted B (AxisymmetricFields.profilePoint t x) - x.ofLp 1 * AxisymmetricResidual.laplaceWeighted F (AxisymmetricFields.profilePoint t x))
(-x.ofLp 1 * AxisymmetricResidual.laplaceWeighted B (AxisymmetricFields.profilePoint t x) + x.ofLp 0 * AxisymmetricResidual.laplaceWeighted F (AxisymmetricFields.profilePoint t x))
(AxisymmetricResidual.laplaceScalar U (AxisymmetricFields.profilePoint t x))
The physical vector Laplacian is local in all three profiles. In particular this applies to a radial quotient at any point where it is C².
theorem
NavierStokes.LocalAxisymmetricResidual.pressureGradient_pressure
{P : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hP : DifferentiableAt ℝ P (AxisymmetricFields.profilePoint t x))
:
ProblemStatement.pressureGradient (AxisymmetricResidual.pressure P) t x = AxisymmetricResidual.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))
theorem
NavierStokes.LocalAxisymmetricResidual.hasFDerivAt_time_lift
{G : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hG : DifferentiableAt ℝ G (AxisymmetricFields.profilePoint t x))
:
HasFDerivAt (fun (s : ℝ) => AxisymmetricResidual.lift G s x)
(AxisymmetricResidual.timeProfileDerivative G (AxisymmetricFields.profilePoint t x)) t
Joint profile differentiability provides the time derivative at the point, with no hypothesis about any other point of the spatial slice.
theorem
NavierStokes.LocalAxisymmetricResidual.temporalDerivative_velocity
{B F U : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : DifferentiableAt ℝ B (AxisymmetricFields.profilePoint t x))
(hF : DifferentiableAt ℝ F (AxisymmetricFields.profilePoint t x))
(hU : DifferentiableAt ℝ U (AxisymmetricFields.profilePoint t x))
:
ProblemStatement.temporalDerivative (AxisymmetricResidual.velocity B F U) t x = AxisymmetricResidual.pack
(-x.ofLp 0 * AxisymmetricResidual.partialT B (AxisymmetricFields.profilePoint t x) - x.ofLp 1 * AxisymmetricResidual.partialT F (AxisymmetricFields.profilePoint t x))
(-x.ofLp 1 * AxisymmetricResidual.partialT B (AxisymmetricFields.profilePoint t x) + x.ofLp 0 * AxisymmetricResidual.partialT F (AxisymmetricFields.profilePoint t x))
(AxisymmetricResidual.partialT U (AxisymmetricFields.profilePoint t x))
theorem
NavierStokes.LocalAxisymmetricResidual.navierStokesResidual_velocity
{B F U P : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : ContDiffAt ℝ 2 B (AxisymmetricFields.profilePoint t x))
(hF : ContDiffAt ℝ 2 F (AxisymmetricFields.profilePoint t x))
(hU : ContDiffAt ℝ 2 U (AxisymmetricFields.profilePoint t x))
(hP : DifferentiableAt ℝ P (AxisymmetricFields.profilePoint t x))
:
ProblemStatement.navierStokesResidual (AxisymmetricResidual.velocity B F U) (AxisymmetricResidual.pressure P) t x = AxisymmetricResidual.pack
(x.ofLp 0 * AxisymmetricResidual.residualRadial B F U P (AxisymmetricFields.profilePoint t x) + x.ofLp 1 * AxisymmetricResidual.residualAngular B F U (AxisymmetricFields.profilePoint t x))
(x.ofLp 1 * AxisymmetricResidual.residualRadial B F U P (AxisymmetricFields.profilePoint t x) - x.ofLp 0 * AxisymmetricResidual.residualAngular B F U (AxisymmetricFields.profilePoint t x))
(AxisymmetricResidual.residualAxial B U P (AxisymmetricFields.profilePoint t x))
The exact physical residual at viscosity one, from regularity only at
the evaluated joint profile point. No SliceC2 or SliceDifferentiable
hypothesis occurs. This does not assert that a radial quotient is smooth
at a point where its denominator vanishes.
theorem
NavierStokes.LocalAxisymmetricResidual.navierStokesResidual_eq_zero
{B F U P : AxisymmetricFields.Profile}
{t : ℝ}
{x : ProblemStatement.Space}
(hB : ContDiffAt ℝ 2 B (AxisymmetricFields.profilePoint t x))
(hF : ContDiffAt ℝ 2 F (AxisymmetricFields.profilePoint t x))
(hU : ContDiffAt ℝ 2 U (AxisymmetricFields.profilePoint t x))
(hP : DifferentiableAt ℝ P (AxisymmetricFields.profilePoint t x))
(hr : AxisymmetricResidual.residualRadial B F U P (AxisymmetricFields.profilePoint t x) = 0)
(ha : AxisymmetricResidual.residualAngular B F U (AxisymmetricFields.profilePoint t x) = 0)
(hz : AxisymmetricResidual.residualAxial B U P (AxisymmetricFields.profilePoint t x) = 0)
:
The three local coefficient equations imply the actual Cartesian PDE.