Smooth axisymmetric fields in Cartesian coordinates

Profiles use coordinates (t,s,z), where s=(x₀²+x₁²)/2. The velocity is an actual Euclidean curl. No division by the radius is used, including at the axis.

@[reducible, inline]

abbrev NavierStokes.AxisymmetricFields.ProfilePoint : Type

Profile point: an abbreviation for ℝ × (ℝ × ℝ).

Equations

• NavierStokes.AxisymmetricFields.ProfilePoint = (ℝ × ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.AxisymmetricFields.Profile : Type

Profile: an abbreviation for ProfilePoint → ℝ.

Equations

• NavierStokes.AxisymmetricFields.Profile = (NavierStokes.AxisymmetricFields.ProfilePoint → ℝ)

noncomputable def NavierStokes.AxisymmetricFields.projection (i : Fin 3) : ProblemStatement.Space →L[ℝ] ℝ

Projection, given by EuclideanSpace.proj i.

Equations

• NavierStokes.AxisymmetricFields.projection i = EuclideanSpace.proj i

@[simp]

theorem NavierStokes.AxisymmetricFields.projection_apply (i : Fin 3) (x : ProblemStatement.Space) : (projection i) x = x.ofLp i

noncomputable def NavierStokes.AxisymmetricFields.radialEnergy (x : ProblemStatement.Space) : ℝ

Radial energy, given by (x 0 ^ 2 + x 1 ^ 2) / 2.

Equations

• NavierStokes.AxisymmetricFields.radialEnergy x = (x.ofLp 0 ^ 2 + x.ofLp 1 ^ 2) / 2

noncomputable def NavierStokes.AxisymmetricFields.profilePoint (t : ℝ) (x : ProblemStatement.Space) : ProfilePoint

Profile point, given by (t, (radialEnergy x, x 2)).

Equations

• NavierStokes.AxisymmetricFields.profilePoint t x = (t, NavierStokes.AxisymmetricFields.radialEnergy x, x.ofLp 2)

noncomputable def NavierStokes.AxisymmetricFields.partialS (F : Profile) (p : ProfilePoint) : ℝ

Partial S, given by fderiv ℝ F p (0, (1, 0)).

Equations

• NavierStokes.AxisymmetricFields.partialS F p = (fderiv ℝ F p) (0, 1, 0)

noncomputable def NavierStokes.AxisymmetricFields.partialZ (F : Profile) (p : ProfilePoint) : ℝ

Partial Z, given by fderiv ℝ F p (0, (0, 1)).

Equations

• NavierStokes.AxisymmetricFields.partialZ F p = (fderiv ℝ F p) (0, 0, 1)

noncomputable def NavierStokes.AxisymmetricFields.potential (H K : Profile) : ProblemStatement.VelocityField

Potential as an element of VelocityField.

Equations

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

noncomputable def NavierStokes.AxisymmetricFields.velocity (H K : Profile) : ProblemStatement.VelocityField

Velocity, given by SpatialCurl.spatialCurl (potential H K).

Equations

• NavierStokes.AxisymmetricFields.velocity H K = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.AxisymmetricFields.potential H K)

theorem NavierStokes.AxisymmetricFields.radialEnergy_nonneg (x : ProblemStatement.Space) : 0 ≤ radialEnergy x

theorem NavierStokes.AxisymmetricFields.contDiff_radialEnergy {n : WithTop ℕ∞} : ContDiff ℝ n radialEnergy

theorem NavierStokes.AxisymmetricFields.contDiff_profilePoint {n : WithTop ℕ∞} : ContDiff ℝ n fun (w : ProblemStatement.SpaceTime) => profilePoint w.1 w.2

theorem NavierStokes.AxisymmetricFields.contDiff_profilePoint_slice (t : ℝ) {n : WithTop ℕ∞} : ContDiff ℝ n (profilePoint t)

noncomputable def NavierStokes.AxisymmetricFields.radialLinear (x : ProblemStatement.Space) : ProblemStatement.Space →L[ℝ] ℝ

Radial linear, given by x 0 • projection 0 + x 1 • projection 1.

Equations

• NavierStokes.AxisymmetricFields.radialLinear x = x.ofLp 0 • NavierStokes.AxisymmetricFields.projection 0 + x.ofLp 1 • NavierStokes.AxisymmetricFields.projection 1

theorem NavierStokes.AxisymmetricFields.hasFDerivAt_radialEnergy (x : ProblemStatement.Space) : HasFDerivAt radialEnergy (radialLinear x) x

noncomputable def NavierStokes.AxisymmetricFields.profileJacobian (x : ProblemStatement.Space) : ProblemStatement.Space →L[ℝ] ProfilePoint

Profile jacobian, given by (0 : Space →L[ℝ] ℝ).prod ((radialLinear x).prod (projection 2)).

Equations

• NavierStokes.AxisymmetricFields.profileJacobian x = ContinuousLinearMap.prod 0 ((NavierStokes.AxisymmetricFields.radialLinear x).prod (NavierStokes.AxisymmetricFields.projection 2))

theorem NavierStokes.AxisymmetricFields.hasFDerivAt_profilePoint (t : ℝ) (x : ProblemStatement.Space) : HasFDerivAt (profilePoint t) (profileJacobian x) x

@[simp]

theorem NavierStokes.AxisymmetricFields.profileJacobian_apply (x v : ProblemStatement.Space) : (profileJacobian x) v = (0, x.ofLp 0 * v.ofLp 0 + x.ofLp 1 * v.ofLp 1, v.ofLp 2)

noncomputable def NavierStokes.AxisymmetricFields.profileDerivative (F : Profile) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space →L[ℝ] ℝ

Profile derivative, given by (fderiv ℝ F (profilePoint t x)).comp (profileJacobian x).

Equations

• NavierStokes.AxisymmetricFields.profileDerivative F t x = fderiv ℝ F (NavierStokes.AxisymmetricFields.profilePoint t x) ∘SL NavierStokes.AxisymmetricFields.profileJacobian x

theorem NavierStokes.AxisymmetricFields.hasFDerivAt_profile_composition (F : Profile) (t : ℝ) (x : ProblemStatement.Space) (hF : DifferentiableAt ℝ F (profilePoint t x)) : HasFDerivAt (fun (y : ProblemStatement.Space) => F (profilePoint t y)) (profileDerivative F t x) x

theorem NavierStokes.AxisymmetricFields.profileDerivative_apply (F : Profile) (t : ℝ) (x v : ProblemStatement.Space) : (profileDerivative F t x) v = (x.ofLp 0 * v.ofLp 0 + x.ofLp 1 * v.ofLp 1) * partialS F (profilePoint t x) + v.ofLp 2 * partialZ F (profilePoint t x)

noncomputable def NavierStokes.AxisymmetricFields.potentialJacobian (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.Space →L[ℝ] ProblemStatement.Space

Potential jacobian as an element of Space →L[ℝ] Space.

Equations

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

theorem NavierStokes.AxisymmetricFields.hasFDerivAt_potential (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : DifferentiableAt ℝ H (profilePoint t x)) (hK : DifferentiableAt ℝ K (profilePoint t x)) : HasFDerivAt (fun (y : ProblemStatement.Space) => potential H K (t, y)) (potentialJacobian H K t x) x

theorem NavierStokes.AxisymmetricFields.velocity_zero (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : DifferentiableAt ℝ H (profilePoint t x)) (hK : DifferentiableAt ℝ K (profilePoint t x)) : (velocity H K (t, x)).ofLp 0 = -x.ofLp 0 * partialZ H (profilePoint t x) / 2 + x.ofLp 1 * partialS K (profilePoint t x)

theorem NavierStokes.AxisymmetricFields.velocity_one (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : DifferentiableAt ℝ H (profilePoint t x)) (hK : DifferentiableAt ℝ K (profilePoint t x)) : (velocity H K (t, x)).ofLp 1 = -x.ofLp 1 * partialZ H (profilePoint t x) / 2 - x.ofLp 0 * partialS K (profilePoint t x)

theorem NavierStokes.AxisymmetricFields.velocity_two (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : DifferentiableAt ℝ H (profilePoint t x)) (hK : DifferentiableAt ℝ K (profilePoint t x)) : (velocity H K (t, x)).ofLp 2 = H (profilePoint t x) + radialEnergy x * partialS H (profilePoint t x)

theorem NavierStokes.AxisymmetricFields.contDiff_potential {H K : Profile} {n : WithTop ℕ∞} (hH : ContDiff ℝ n H) (hK : ContDiff ℝ n K) : ContDiff ℝ n (potential H K)

The Cartesian potential is smooth on all of space, including the axis.

theorem NavierStokes.AxisymmetricFields.contDiffOn_potential {H K : Profile} {times : Set ℝ} {n : WithTop ℕ∞} (hH : ContDiffOn ℝ n H (times ×ˢ Set.univ)) (hK : ContDiffOn ℝ n K (times ×ˢ Set.univ)) : ContDiffOn ℝ n (potential H K) (times ×ˢ Set.univ)

Smoothness may be required only on a prescribed set of times.

theorem NavierStokes.AxisymmetricFields.contDiff_velocity {H K : Profile} {m n : WithTop ℕ∞} (hH : ContDiff ℝ n H) (hK : ContDiff ℝ n K) (hmn : m + 1 ≤ n) : ContDiff ℝ m (velocity H K)

theorem NavierStokes.AxisymmetricFields.smooth_velocity {H K : Profile} (hH : ContDiff ℝ (↑⊤) H) (hK : ContDiff ℝ (↑⊤) K) : ContDiff ℝ (↑⊤) (velocity H K)

theorem NavierStokes.AxisymmetricFields.contDiffOn_velocity {H K : Profile} {times : Set ℝ} {m n : WithTop ℕ∞} (hH : ContDiffOn ℝ n H (times ×ˢ Set.univ)) (hK : ContDiffOn ℝ n K (times ×ˢ Set.univ)) (hmn : m + 1 ≤ n) : ContDiffOn ℝ m (velocity H K) (times ×ˢ Set.univ)

theorem NavierStokes.AxisymmetricFields.divergence_velocity {H K : Profile} (hH : ContDiff ℝ 2 H) (hK : ContDiff ℝ 2 K) (t : ℝ) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (velocity H K) t x = 0

theorem NavierStokes.AxisymmetricFields.divergence_velocity_on {H K : Profile} {times : Set ℝ} (hH : ContDiffOn ℝ 2 H (times ×ˢ Set.univ)) (hK : ContDiffOn ℝ 2 K (times ×ˢ Set.univ)) {t : ℝ} (ht : t ∈ times) (x : ProblemStatement.Space) : ProblemStatement.spatialDivergence (velocity H K) t x = 0

theorem NavierStokes.AxisymmetricFields.velocity_on_axis (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : DifferentiableAt ℝ H (profilePoint t x)) (hK : DifferentiableAt ℝ K (profilePoint t x)) (hx0 : x.ofLp 0 = 0) (hx1 : x.ofLp 1 = 0) : velocity H K (t, x) = H (t, 0, x.ofLp 2) • ProblemStatement.coordinateVector 2

On the axis the field is purely axial with value H(t,0,z), with no limit or removable-singularity argument required.

theorem NavierStokes.AxisymmetricFields.tsupport_potential_slice_subset (H K : Profile) (t : ℝ) : (tsupport fun (x : ProblemStatement.Space) => potential H K (t, x)) ⊆ profilePoint t ⁻¹' (tsupport H ∪ tsupport K)

The potential's closed spatial support is controlled by the two profile supports, pulled back under the smooth (t,s,z) coordinate map.

theorem NavierStokes.AxisymmetricFields.tsupport_velocity_slice_subset (H K : Profile) (t : ℝ) : (tsupport fun (x : ProblemStatement.Space) => velocity H K (t, x)) ⊆ profilePoint t ⁻¹' (tsupport H ∪ tsupport K)

Taking the actual curl does not enlarge this closed spatial support.

theorem NavierStokes.AxisymmetricFields.velocity_eq_zero_outside_profile_support (H K : Profile) (t : ℝ) (x : ProblemStatement.Space) (hH : profilePoint t x ∉ tsupport H) (hK : profilePoint t x ∉ tsupport K) : velocity H K (t, x) = 0

theorem NavierStokes.AxisymmetricFields.isCompact_cylinder (R Z : ℝ) : IsCompact {x : ProblemStatement.Space | radialEnergy x ≤ R ∧ |x.ofLp 2| ≤ Z}

The Cartesian cylinder cut out by bounds on s and z is compact.

theorem NavierStokes.AxisymmetricFields.tsupport_velocity_cylinder_subset (H K : Profile) (t R Z : ℝ) (hH : tsupport H ⊆ {p : ProfilePoint | p.2.1 ≤ R ∧ |p.2.2| ≤ Z}) (hK : tsupport K ⊆ {p : ProfilePoint | p.2.1 ≤ R ∧ |p.2.2| ≤ Z}) : (tsupport fun (x : ProblemStatement.Space) => velocity H K (t, x)) ⊆ {x : ProblemStatement.Space | radialEnergy x ≤ R ∧ |x.ofLp 2| ≤ Z}

Bounds on profile support give a literal closed cylinder in Cartesian space: s ≤ R and |z| ≤ Z.

theorem NavierStokes.AxisymmetricFields.hasCompactSupport_velocity_of_profile_bounds (H K : Profile) (t R Z : ℝ) (hH : tsupport H ⊆ {p : ProfilePoint | p.2.1 ≤ R ∧ |p.2.2| ≤ Z}) (hK : tsupport K ⊆ {p : ProfilePoint | p.2.1 ≤ R ∧ |p.2.2| ≤ Z}) : HasCompactSupport fun (x : ProblemStatement.Space) => velocity H K (t, x)