Actual Cartesian differential operators in cylindrical coordinates

The chart is (r,theta,z) ↦ (r cos theta,r sin theta,z). Coordinate derivatives are actual Fréchet derivatives. Pulling Cartesian fields back through this chart avoids choosing a global inverse angular coordinate.

noncomputable def NavierStokes.CylindricalResidual.chart (q : ProblemStatement.Space) : ProblemStatement.Space

The three arguments are r, theta, and z, respectively.

Equations

• NavierStokes.CylindricalResidual.chart q = NavierStokes.AxisymmetricResidual.pack (q.ofLp 0 * Real.cos (q.ofLp 1)) (q.ofLp 0 * Real.sin (q.ofLp 1)) (q.ofLp 2)

noncomputable def NavierStokes.CylindricalResidual.horizontal : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Horizontal, given by packDerivative (projection 0) (projection 1) 0.

Equations

• NavierStokes.CylindricalResidual.horizontal = NavierStokes.AxisymmetricResidual.packDerivative (NavierStokes.AxisymmetricFields.projection 0) (NavierStokes.AxisymmetricFields.projection 1) 0

noncomputable def NavierStokes.CylindricalResidual.connection : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Infinitesimal rotation: (a,b,c) ↦ (-b,a,0).

Equations

• NavierStokes.CylindricalResidual.connection = NavierStokes.AxisymmetricResidual.packDerivative (-NavierStokes.AxisymmetricFields.projection 1) (NavierStokes.AxisymmetricFields.projection 0) 0

noncomputable def NavierStokes.CylindricalResidual.vertical : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Vertical, given by packDerivative 0 0 (projection 2).

Equations

• NavierStokes.CylindricalResidual.vertical = NavierStokes.AxisymmetricResidual.packDerivative 0 0 (NavierStokes.AxisymmetricFields.projection 2)

noncomputable def NavierStokes.CylindricalResidual.frame (θ : ℝ) : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Frame, given by Real.cos θ • horizontal + Real.sin θ • connection + vertical.

Equations

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

theorem NavierStokes.CylindricalResidual.frame_apply (θ : ℝ) (v : ProblemStatement.Space) : (frame θ) v = AxisymmetricResidual.pack (Real.cos θ * v.ofLp 0 - Real.sin θ * v.ofLp 1) (Real.sin θ * v.ofLp 0 + Real.cos θ * v.ofLp 1) (v.ofLp 2)

theorem NavierStokes.CylindricalResidual.connection_apply (v : ProblemStatement.Space) : connection v = AxisymmetricResidual.pack (-v.ofLp 1) (v.ofLp 0) 0

theorem NavierStokes.CylindricalResidual.frame_connection (θ : ℝ) : frame θ ∘SL connection = -Real.sin θ • horizontal + Real.cos θ • connection

theorem NavierStokes.CylindricalResidual.frame_inverse (θ : ℝ) (v : ProblemStatement.Space) : (frame (-θ)) ((frame θ) v) = v

theorem NavierStokes.CylindricalResidual.frame_inverse' (θ : ℝ) (v : ProblemStatement.Space) : (frame θ) ((frame (-θ)) v) = v

noncomputable def NavierStokes.CylindricalResidual.chartJacobian (q : ProblemStatement.Space) : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Chart jacobian, given by (frame (q 1)).comp (packDerivative (projection 0) (q 0 • projection 1) (projection 2)).

Equations

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

theorem NavierStokes.CylindricalResidual.chartJacobian_apply (q v : ProblemStatement.Space) : (chartJacobian q) v = (frame (q.ofLp 1)) (AxisymmetricResidual.pack (v.ofLp 0) (q.ofLp 0 * v.ofLp 1) (v.ofLp 2))

theorem NavierStokes.CylindricalResidual.hasFDerivAt_chart (q : ProblemStatement.Space) : HasFDerivAt chart (chartJacobian q) q

theorem NavierStokes.CylindricalResidual.contDiff_chart {n : WithTop ℕ∞} : ContDiff ℝ n chart

noncomputable def NavierStokes.CylindricalResidual.dCoord {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : Fin 3) (f : ProblemStatement.Space → E) (q : ProblemStatement.Space) : E

D coord, given by fderiv ℝ f q (coordinateVector i).

Equations

• NavierStokes.CylindricalResidual.dCoord i f q = (fderiv ℝ f q) (NavierStokes.ProblemStatement.coordinateVector i)

noncomputable def NavierStokes.CylindricalResidual.euclideanLaplacian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.Space → E) (x : ProblemStatement.Space) : E

Euclidean laplacian, given by ∑ i : Fin 3, dCoord i (dCoord i f) x.

Equations

• NavierStokes.CylindricalResidual.euclideanLaplacian f x = ∑ i : Fin 3, NavierStokes.CylindricalResidual.dCoord i (NavierStokes.CylindricalResidual.dCoord i f) x

noncomputable def NavierStokes.CylindricalResidual.scalarLaplacian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.Space → E) (q : ProblemStatement.Space) : E

Scalar laplacian, given by dCoord 0 (dCoord 0 f) q + (q 0)⁻¹ • dCoord 0 f q + ((q 0) ^ 2)⁻¹ • dCoord 1 (dCoord 1 f) q + dCoord 2 (dCoord 2 f) q.

Equations

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

theorem NavierStokes.CylindricalResidual.contDiffAt_dCoord {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} {m n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f q) (hmn : m + 1 ≤ n) (i : Fin 3) : ContDiffAt ℝ m (dCoord i f) q

theorem NavierStokes.CylindricalResidual.dCoord_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.Space → E} {q : ProblemStatement.Space} (h : f =ᶠ[nhds q] g) (i : Fin 3) : dCoord i f q = dCoord i g q

theorem NavierStokes.CylindricalResidual.dCoord_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f q) (hg : DifferentiableAt ℝ g q) (i : Fin 3) : dCoord i (fun (y : ProblemStatement.Space) => f y + g y) q = dCoord i f q + dCoord i g q

theorem NavierStokes.CylindricalResidual.dCoord_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f q) (i : Fin 3) : dCoord i (fun (y : ProblemStatement.Space) => L (f y)) q = L (dCoord i f q)

theorem NavierStokes.CylindricalResidual.fderiv_pullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (v : ProblemStatement.Space) : (fderiv ℝ (fun (y : ProblemStatement.Space) => f (chart y)) q) v = (fderiv ℝ f (chart q)) ((chartJacobian q) v)

noncomputable def NavierStokes.CylindricalResidual.chartVector (q v : ProblemStatement.Space) : ProblemStatement.Space

Resolve a Cartesian vector into chart-coordinate components.

Equations

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

theorem NavierStokes.CylindricalResidual.chartJacobian_chartVector (q v : ProblemStatement.Space) (hr : q.ofLp 0 ≠ 0) : (chartJacobian q) (chartVector q v) = v

theorem NavierStokes.CylindricalResidual.cartesian_derivative_from_pullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (hr : q.ofLp 0 ≠ 0) (v : ProblemStatement.Space) : (fderiv ℝ f (chart q)) v = (fderiv ℝ (fun (y : ProblemStatement.Space) => f (chart y)) q) (chartVector q v)

Exact first-order bridge from ordinary Cartesian derivatives.

noncomputable def NavierStokes.CylindricalResidual.hessian {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.Space → E) (x v w : ProblemStatement.Space) : E

The actual second Fréchet derivative, with the two directions displayed.

Equations

• NavierStokes.CylindricalResidual.hessian f x v w = ((fderiv ℝ (fderiv ℝ f) x) v) w

theorem NavierStokes.CylindricalResidual.dCoord_dCoord {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : ContDiffAt ℝ 2 f q) (i : Fin 3) : dCoord i (dCoord i f) q = hessian f q (ProblemStatement.coordinateVector i) (ProblemStatement.coordinateVector i)

theorem NavierStokes.CylindricalResidual.second_chain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {g : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hf : ContDiffAt ℝ 2 f (g q)) (hg : ContDiffAt ℝ 2 g q) (i : Fin 3) : dCoord i (dCoord i (f ∘ g)) q = hessian f (g q) (dCoord i g q) (dCoord i g q) + (fderiv ℝ f (g q)) (dCoord i (dCoord i g) q)

theorem NavierStokes.CylindricalResidual.dCoord_chart_zero (q : ProblemStatement.Space) : dCoord 0 chart q = AxisymmetricResidual.pack (Real.cos (q.ofLp 1)) (Real.sin (q.ofLp 1)) 0

theorem NavierStokes.CylindricalResidual.dCoord_chart_one (q : ProblemStatement.Space) : dCoord 1 chart q = AxisymmetricResidual.pack (-q.ofLp 0 * Real.sin (q.ofLp 1)) (q.ofLp 0 * Real.cos (q.ofLp 1)) 0

theorem NavierStokes.CylindricalResidual.dCoord_chart_two (q : ProblemStatement.Space) : dCoord 2 chart q = ProblemStatement.coordinateVector 2

theorem NavierStokes.CylindricalResidual.dCoord_dCoord_chart_zero (q : ProblemStatement.Space) : dCoord 0 (dCoord 0 chart) q = 0

theorem NavierStokes.CylindricalResidual.dCoord_dCoord_chart_one (q : ProblemStatement.Space) : dCoord 1 (dCoord 1 chart) q = -q.ofLp 0 • dCoord 0 chart q

theorem NavierStokes.CylindricalResidual.dCoord_dCoord_chart_two (q : ProblemStatement.Space) : dCoord 2 (dCoord 2 chart) q = 0

theorem NavierStokes.CylindricalResidual.dCoord_pullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (i : Fin 3) : dCoord i (f ∘ chart) q = (fderiv ℝ f (chart q)) (dCoord i chart q)

theorem NavierStokes.CylindricalResidual.scalarLaplacian_pullback {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : ContDiffAt ℝ 2 f (chart q)) (hr : q.ofLp 0 ≠ 0) : scalarLaplacian (fun (y : ProblemStatement.Space) => f (chart y)) q = euclideanLaplacian f (chart q)

The cylindrical scalar Laplacian is the pullback of the Cartesian trace.

theorem NavierStokes.CylindricalResidual.contDiff_frame {n : WithTop ℕ∞} : ContDiff ℝ n frame

theorem NavierStokes.CylindricalResidual.hasFDerivAt_frameField (q : ProblemStatement.Space) : HasFDerivAt (fun (y : ProblemStatement.Space) => frame (y.ofLp 1)) ((AxisymmetricFields.projection 1).smulRight (frame (q.ofLp 1) ∘SL connection)) q

noncomputable def NavierStokes.CylindricalResidual.encode (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ProblemStatement.Space

Cartesian representation of cylindrical vector components.

Equations

• NavierStokes.CylindricalResidual.encode w q = (NavierStokes.CylindricalResidual.frame (q.ofLp 1)) (w q)

theorem NavierStokes.CylindricalResidual.contDiffAt_encode {w : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} {n : WithTop ℕ∞} (hw : ContDiffAt ℝ n w q) : ContDiffAt ℝ n (encode w) q

theorem NavierStokes.CylindricalResidual.fderiv_encode {w : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hw : DifferentiableAt ℝ w q) (v : ProblemStatement.Space) : (fderiv ℝ (encode w) q) v = (frame (q.ofLp 1)) ((fderiv ℝ w q) v + v.ofLp 1 • connection (w q))

theorem NavierStokes.CylindricalResidual.dCoord_encode {w : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hw : DifferentiableAt ℝ w q) (i : Fin 3) : dCoord i (encode w) q = (frame (q.ofLp 1)) (dCoord i w q + (ProblemStatement.coordinateVector i).ofLp 1 • connection (w q))

theorem NavierStokes.CylindricalResidual.dCoord_const_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f q) (a : ℝ) (i : Fin 3) : dCoord i (fun (y : ProblemStatement.Space) => a • f y) q = a • dCoord i f q

theorem NavierStokes.CylindricalResidual.dCoord_dCoord_encode {w : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hw : ContDiffAt ℝ 2 w q) (i : Fin 3) : dCoord i (dCoord i (encode w)) q = (frame (q.ofLp 1)) (dCoord i (dCoord i w) q + (2 * (ProblemStatement.coordinateVector i).ofLp 1) • connection (dCoord i w q) + (ProblemStatement.coordinateVector i).ofLp 1 ^ 2 • connection (connection (w q)))

noncomputable def NavierStokes.CylindricalResidual.vectorLaplacian (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ProblemStatement.Space

Vector Laplacian of physical components in the moving cylindrical basis.

Equations

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

theorem NavierStokes.CylindricalResidual.scalarLaplacian_encode {w : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hw : ContDiffAt ℝ 2 w q) : scalarLaplacian (encode w) q = (frame (q.ofLp 1)) (vectorLaplacian w q)

noncomputable def NavierStokes.CylindricalResidual.components (f : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ProblemStatement.Space

Cylindrical components of an arbitrary Cartesian vector field.

Equations

• NavierStokes.CylindricalResidual.components f q = (NavierStokes.CylindricalResidual.frame (-q.ofLp 1)) (f (NavierStokes.CylindricalResidual.chart q))

theorem NavierStokes.CylindricalResidual.encode_components (f : ProblemStatement.Space → ProblemStatement.Space) : encode (components f) = fun (q : ProblemStatement.Space) => f (chart q)

theorem NavierStokes.CylindricalResidual.differentiableAt_components {f : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) : DifferentiableAt ℝ (components f) q

theorem NavierStokes.CylindricalResidual.contDiffAt_components {f : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} {n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f (chart q)) : ContDiffAt ℝ n (components f) q

theorem NavierStokes.CylindricalResidual.cartesianLaplacian_components {f : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hf : ContDiffAt ℝ 2 f (chart q)) (hr : q.ofLp 0 ≠ 0) : euclideanLaplacian f (chart q) = (frame (q.ofLp 1)) (vectorLaplacian (components f) q)

theorem NavierStokes.CylindricalResidual.fderiv_pack {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ProblemStatement.Space → E) (q : ProblemStatement.Space) (a b c : ℝ) : (fderiv ℝ f q) (AxisymmetricResidual.pack a b c) = a • dCoord 0 f q + b • dCoord 1 f q + c • dCoord 2 f q

theorem NavierStokes.CylindricalResidual.cartesianDerivative_components {f : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (hr : q.ofLp 0 ≠ 0) (b : ProblemStatement.Space) : (frame (-q.ofLp 1)) ((fderiv ℝ f (chart q)) ((frame (q.ofLp 1)) b)) = b.ofLp 0 • dCoord 0 (components f) q + (b.ofLp 1 / q.ofLp 0) • (dCoord 1 (components f) q + connection (components f q)) + b.ofLp 2 • dCoord 2 (components f) q

Cartesian directional differentiation, resolved in the cylindrical frame.

noncomputable def NavierStokes.CylindricalResidual.vectorAdvection (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ProblemStatement.Space

Vector advection, given by w q 0 • dCoord 0 w q + (w q 1 / q 0) • (dCoord 1 w q + connection (w q)) + w q 2 • dCoord 2 w q.

Equations

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

theorem NavierStokes.CylindricalResidual.cartesianAdvection_components {f : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (hr : q.ofLp 0 ≠ 0) : (fderiv ℝ f (chart q)) (f (chart q)) = (frame (q.ofLp 1)) (vectorAdvection (components f) q)

noncomputable def NavierStokes.CylindricalResidual.euclideanDivergence (f : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ℝ

Euclidean divergence, given by ∑ i : Fin 3, (fderiv ℝ f x (coordinateVector i)) i.

Equations

• NavierStokes.CylindricalResidual.euclideanDivergence f x = ∑ i : Fin 3, ((fderiv ℝ f x) (NavierStokes.ProblemStatement.coordinateVector i)).ofLp i

noncomputable def NavierStokes.CylindricalResidual.vectorDivergence (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : ℝ

Vector divergence, given by (dCoord 0 w q) 0 + w q 0 / q 0 + (dCoord 1 w q) 1 / q 0 + (dCoord 2 w q) 2.

Equations

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

theorem NavierStokes.CylindricalResidual.trace_rotation (A : ProblemStatement.Space →L[ℝ] ProblemStatement.Space) (θ : ℝ) : ∑ i : Fin 3, (A (ProblemStatement.coordinateVector i)).ofLp i = ∑ i : Fin 3, ((frame (-θ)) (A ((frame θ) (ProblemStatement.coordinateVector i)))).ofLp i

theorem NavierStokes.CylindricalResidual.cartesianDivergence_components {f : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (hr : q.ofLp 0 ≠ 0) : euclideanDivergence f (chart q) = vectorDivergence (components f) q

noncomputable def NavierStokes.CylindricalResidual.euclideanGradient (f : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space

Euclidean gradient, given by ∑ i : Fin 3, dCoord i f x • coordinateVector i.

Equations

• NavierStokes.CylindricalResidual.euclideanGradient f x = ∑ i : Fin 3, NavierStokes.CylindricalResidual.dCoord i f x • NavierStokes.ProblemStatement.coordinateVector i

noncomputable def NavierStokes.CylindricalResidual.scalarGradient (f : ProblemStatement.Space → ℝ) (q : ProblemStatement.Space) : ProblemStatement.Space

Scalar gradient, given by pack (dCoord 0 f q) (dCoord 1 f q / q 0) (dCoord 2 f q).

Equations

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

theorem NavierStokes.CylindricalResidual.cartesianGradient_pullback {f : ProblemStatement.Space → ℝ} {q : ProblemStatement.Space} (hf : DifferentiableAt ℝ f (chart q)) (hr : q.ofLp 0 ≠ 0) : euclideanGradient f (chart q) = (frame (q.ofLp 1)) (scalarGradient (f ∘ chart) q)

noncomputable def NavierStokes.CylindricalResidual.velocityComponents (u : ProblemStatement.VelocityField) : ProblemStatement.VelocityField

Pullback of a time-dependent velocity into the moving cylindrical frame.

Equations

• NavierStokes.CylindricalResidual.velocityComponents u tq = NavierStokes.CylindricalResidual.components (fun (x : NavierStokes.ProblemStatement.Space) => u (tq.1, x)) tq.2

noncomputable def NavierStokes.CylindricalResidual.pressurePullback (p : ProblemStatement.PressureField) : ProblemStatement.PressureField

Pressure pullback, defined pointwise by p (tq.1, chart tq.2).

Equations

• NavierStokes.CylindricalResidual.pressurePullback p tq = p (tq.1, NavierStokes.CylindricalResidual.chart tq.2)

noncomputable def NavierStokes.CylindricalResidual.cylindricalResidual (w : ProblemStatement.VelocityField) (p : ProblemStatement.PressureField) (t : ℝ) (q : ProblemStatement.Space) : ProblemStatement.Space

Cylindrical residual, constructed using temporalDerivative.

Equations

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

theorem NavierStokes.CylindricalResidual.temporalDerivative_components {u : ProblemStatement.VelocityField} {t : ℝ} {q : ProblemStatement.Space} (ht : DifferentiableAt ℝ (fun (s : ℝ) => u (s, chart q)) t) : ProblemStatement.temporalDerivative (velocityComponents u) t q = (frame (-q.ofLp 1)) (ProblemStatement.temporalDerivative u t (chart q))

theorem NavierStokes.CylindricalResidual.navierStokesResidual_cylindrical_of_slices {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hu : ContDiffAt ℝ 2 (fun (x : ProblemStatement.Space) => u (t, x)) (chart q)) (ht : DifferentiableAt ℝ (fun (s : ℝ) => u (s, chart q)) t) (hp : DifferentiableAt ℝ (fun (x : ProblemStatement.Space) => p (t, x)) (chart q)) (hr : 0 < q.ofLp 0) : ProblemStatement.navierStokesResidual u p t (chart q) = (frame (q.ofLp 1)) (cylindricalResidual (velocityComponents u) (pressurePullback p) t q)

The full actual Cartesian Navier--Stokes residual, under local regularity.

theorem NavierStokes.CylindricalResidual.navierStokesResidual_cylindrical {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hu : ContDiffAt ℝ 2 u (t, chart q)) (hp : DifferentiableAt ℝ p (t, chart q)) (hr : 0 < q.ofLp 0) : ProblemStatement.navierStokesResidual u p t (chart q) = (frame (q.ofLp 1)) (cylindricalResidual (velocityComponents u) (pressurePullback p) t q)

Joint local C² regularity supplies all velocity slice hypotheses.

theorem NavierStokes.CylindricalResidual.divergence_cylindrical {u : ProblemStatement.VelocityField} {t : ℝ} {q : ProblemStatement.Space} (hu : DifferentiableAt ℝ (fun (x : ProblemStatement.Space) => u (t, x)) (chart q)) (hr : 0 < q.ofLp 0) : ProblemStatement.spatialDivergence u t (chart q) = vectorDivergence (fun (y : ProblemStatement.Space) => velocityComponents u (t, y)) q

theorem NavierStokes.CylindricalResidual.vectorAdvection_radial (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : (vectorAdvection w q).ofLp 0 = (w q).ofLp 0 * (dCoord 0 w q).ofLp 0 + (w q).ofLp 1 / q.ofLp 0 * (dCoord 1 w q).ofLp 0 + (w q).ofLp 2 * (dCoord 2 w q).ofLp 0 - (w q).ofLp 1 ^ 2 / q.ofLp 0

theorem NavierStokes.CylindricalResidual.vectorAdvection_angular (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : (vectorAdvection w q).ofLp 1 = (w q).ofLp 0 * (dCoord 0 w q).ofLp 1 + (w q).ofLp 1 / q.ofLp 0 * (dCoord 1 w q).ofLp 1 + (w q).ofLp 2 * (dCoord 2 w q).ofLp 1 + (w q).ofLp 0 * (w q).ofLp 1 / q.ofLp 0

theorem NavierStokes.CylindricalResidual.vectorAdvection_axial (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : (vectorAdvection w q).ofLp 2 = (w q).ofLp 0 * (dCoord 0 w q).ofLp 2 + (w q).ofLp 1 / q.ofLp 0 * (dCoord 1 w q).ofLp 2 + (w q).ofLp 2 * (dCoord 2 w q).ofLp 2

theorem NavierStokes.CylindricalResidual.vectorLaplacian_radial (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : (vectorLaplacian w q).ofLp 0 = (scalarLaplacian w q).ofLp 0 - (w q).ofLp 0 / q.ofLp 0 ^ 2 - 2 * (dCoord 1 w q).ofLp 1 / q.ofLp 0 ^ 2

theorem NavierStokes.CylindricalResidual.vectorLaplacian_angular (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : (vectorLaplacian w q).ofLp 1 = (scalarLaplacian w q).ofLp 1 - (w q).ofLp 1 / q.ofLp 0 ^ 2 + 2 * (dCoord 1 w q).ofLp 0 / q.ofLp 0 ^ 2

theorem NavierStokes.CylindricalResidual.vectorLaplacian_axial (w : ProblemStatement.Space → ProblemStatement.Space) (q : ProblemStatement.Space) : (vectorLaplacian w q).ofLp 2 = (scalarLaplacian w q).ofLp 2

theorem NavierStokes.CylindricalResidual.dCoord_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.Space → E} {q : ProblemStatement.Space} (h : f =ᶠ[nhds q] g) (i : Fin 3) : dCoord i f =ᶠ[nhds q] dCoord i g

theorem NavierStokes.CylindricalResidual.scalarLaplacian_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ProblemStatement.Space → E} {q : ProblemStatement.Space} (h : f =ᶠ[nhds q] g) : scalarLaplacian f q = scalarLaplacian g q

theorem NavierStokes.CylindricalResidual.cylindricalResidual_congr {u v : ProblemStatement.VelocityField} {p P : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hu : u =ᶠ[nhds (t, q)] v) (hp : p =ᶠ[nhds (t, q)] P) : cylindricalResidual u p t q = cylindricalResidual v P t q

Every cylindrical operator depends only on the local germ of its fields.

theorem NavierStokes.CylindricalResidual.navierStokesResidual_of_representation {u w : ProblemStatement.VelocityField} {p P : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hu : ContDiffAt ℝ 2 u (t, chart q)) (hp : DifferentiableAt ℝ p (t, chart q)) (hr : 0 < q.ofLp 0) (hw : (fun (tq : ProblemStatement.SpaceTime) => u (tq.1, chart tq.2)) =ᶠ[nhds (t, q)] fun (tq : ℝ × ProblemStatement.Space) => (frame (tq.2.ofLp 1)) (w tq)) (hP : pressurePullback p =ᶠ[nhds (t, q)] P) : ProblemStatement.navierStokesResidual u p t (chart q) = (frame (q.ofLp 1)) (cylindricalResidual w P t q)

Apply the coordinate law to an arbitrary locally specified cylindrical ansatz. The velocity premise is an equality of values on a neighborhood, not an assumed identity between derivatives or differential operators.

theorem NavierStokes.CylindricalResidual.navierStokesResidual_zero_iff {u : ProblemStatement.VelocityField} {p : ProblemStatement.PressureField} {t : ℝ} {q : ProblemStatement.Space} (hu : ContDiffAt ℝ 2 u (t, chart q)) (hp : DifferentiableAt ℝ p (t, chart q)) (hr : 0 < q.ofLp 0) : ProblemStatement.navierStokesResidual u p t (chart q) = 0 ↔ cylindricalResidual (velocityComponents u) (pressurePullback p) t q = 0

theorem NavierStokes.CylindricalResidual.dCoord_dCoord_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : ContDiffAt ℝ 2 f q) (i : Fin 3) : dCoord i (dCoord i fun (y : ProblemStatement.Space) => L (f y)) q = L (dCoord i (dCoord i f) q)

theorem NavierStokes.CylindricalResidual.scalarLaplacian_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : E →L[ℝ] F) {f : ProblemStatement.Space → E} {q : ProblemStatement.Space} (hf : ContDiffAt ℝ 2 f q) : scalarLaplacian (fun (y : ProblemStatement.Space) => L (f y)) q = L (scalarLaplacian f q)

theorem NavierStokes.CylindricalResidual.scalarLaplacian_component {w : ProblemStatement.Space → ProblemStatement.Space} {q : ProblemStatement.Space} (hw : ContDiffAt ℝ 2 w q) (j : Fin 3) : scalarLaplacian (fun (y : ProblemStatement.Space) => (w y).ofLp j) q = (scalarLaplacian w q).ofLp j

The vector-valued scalar Laplacian has the expected actual scalar components.