Actual derivatives of reconstructed similarity profiles

The physical variables are (t,s,z), with s = r²/2. Inner profiles use (X,η). All partial derivatives below are genuine Fréchet derivatives.

@[reducible, inline]

abbrev NavierStokes.SimilarityProfile.PhysicalPoint : Type

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

Equations

• NavierStokes.SimilarityProfile.PhysicalPoint = (ℝ × ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.SimilarityProfile.InnerPoint : Type

Inner point: an abbreviation for ℝ × ℝ.

Equations

• NavierStokes.SimilarityProfile.InnerPoint = (ℝ × ℝ)

@[reducible, inline]

abbrev NavierStokes.SimilarityProfile.InnerProfile : Type

Inner profile: an abbreviation for InnerPoint → ℝ.

Equations

• NavierStokes.SimilarityProfile.InnerProfile = (NavierStokes.SimilarityProfile.InnerPoint → ℝ)

@[reducible, inline]

abbrev NavierStokes.SimilarityProfile.PhysicalProfile : Type

Physical profile: an abbreviation for PhysicalPoint → ℝ.

Equations

• NavierStokes.SimilarityProfile.PhysicalProfile = (NavierStokes.SimilarityProfile.PhysicalPoint → ℝ)

@[reducible, inline]

noncomputable abbrev NavierStokes.SimilarityProfile.D (h : ℝ) : ℝ

D: an abbreviation for CoordinateAlgebra.D.

Equations

• NavierStokes.SimilarityProfile.D = NavierStokes.CoordinateAlgebra.D

@[reducible, inline]

abbrev NavierStokes.SimilarityProfile.d (η : ℝ) : ℝ

D: an abbreviation for CoordinateAlgebra.d.

Equations

• NavierStokes.SimilarityProfile.d = NavierStokes.CoordinateAlgebra.d

@[reducible, inline]

abbrev NavierStokes.SimilarityProfile.L (h η : ℝ) : ℝ

L: an abbreviation for CoordinateAlgebra.L.

Equations

• NavierStokes.SimilarityProfile.L = NavierStokes.CoordinateAlgebra.L

noncomputable def NavierStokes.SimilarityProfile.q (h : ℝ) (p : PhysicalPoint) : ℝ

Q, given by SimilarityCoordinates.coordinateQ (2 * h) (1 - p.1, p.2.2).

Equations

• NavierStokes.SimilarityProfile.q h p = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) (1 - p.1, p.2.2)

noncomputable def NavierStokes.SimilarityProfile.eta (h : ℝ) (p : PhysicalPoint) : ℝ

Eta, given by SimilarityCoordinates.coordinateEta (2 * h) (1 - p.1, p.2.2).

Equations

• NavierStokes.SimilarityProfile.eta h p = NavierStokes.SimilarityCoordinates.coordinateEta (2 * h) (1 - p.1, p.2.2)

noncomputable def NavierStokes.SimilarityProfile.X (h : ℝ) (p : PhysicalPoint) : ℝ

X, given by p.2.1 / q h p.

Equations

• NavierStokes.SimilarityProfile.X h p = p.2.1 / NavierStokes.SimilarityProfile.q h p

noncomputable def NavierStokes.SimilarityProfile.inner (h : ℝ) (p : PhysicalPoint) : InnerPoint

Inner, given by (X h p, eta h p).

Equations

• NavierStokes.SimilarityProfile.inner h p = (NavierStokes.SimilarityProfile.X h p, NavierStokes.SimilarityProfile.eta h p)

noncomputable def NavierStokes.SimilarityProfile.partialX (f : InnerProfile) (w : InnerPoint) : ℝ

Partial X, given by fderiv ℝ f w (1, 0).

Equations

• NavierStokes.SimilarityProfile.partialX f w = (fderiv ℝ f w) (1, 0)

noncomputable def NavierStokes.SimilarityProfile.partialEta (f : InnerProfile) (w : InnerPoint) : ℝ

Partial eta, given by fderiv ℝ f w (0, 1).

Equations

• NavierStokes.SimilarityProfile.partialEta f w = (fderiv ℝ f w) (0, 1)

noncomputable def NavierStokes.SimilarityProfile.T (h b : ℝ) (f : InnerProfile) (w : InnerPoint) : ℝ

T, given by CoordinateAlgebra.timeCoeff b h w.2 w.1 (f w) (partialX f w) (partialEta f w).

Equations

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

noncomputable def NavierStokes.SimilarityProfile.Z (h b : ℝ) (f : InnerProfile) (w : InnerPoint) : ℝ

Z, given by CoordinateAlgebra.axialCoeff b h w.2 w.1 (f w) (partialX f w) (partialEta f w).

Equations

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

noncomputable def NavierStokes.SimilarityProfile.pullback (h b : ℝ) (f : InnerProfile) (p : PhysicalPoint) : ℝ

Pullback, given by q h p ^ b * f (inner h p).

Equations

• NavierStokes.SimilarityProfile.pullback h b f p = NavierStokes.SimilarityProfile.q h p ^ b * f (NavierStokes.SimilarityProfile.inner h p)

noncomputable def NavierStokes.SimilarityProfile.partialT (F : PhysicalProfile) (p : PhysicalPoint) : ℝ

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

Equations

• NavierStokes.SimilarityProfile.partialT F p = (fderiv ℝ F p) (1, 0, 0)

noncomputable def NavierStokes.SimilarityProfile.partialS (F : PhysicalProfile) (p : PhysicalPoint) : ℝ

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

Equations

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

noncomputable def NavierStokes.SimilarityProfile.partialZ (F : PhysicalProfile) (p : PhysicalPoint) : ℝ

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

Equations

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

theorem NavierStokes.SimilarityProfile.D_eq (h : ℝ) : (1 - 2 * h) / 2 = D h

theorem NavierStokes.SimilarityProfile.q_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : 0 < q h p

theorem NavierStokes.SimilarityProfile.eta_sq_lt_one {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : eta h p ^ 2 < 1

theorem NavierStokes.SimilarityProfile.L_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : 0 < L h (eta h p)

theorem NavierStokes.SimilarityProfile.q_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (q h) p

theorem NavierStokes.SimilarityProfile.eta_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (eta h) p

theorem NavierStokes.SimilarityProfile.inner_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (inner h) p

theorem NavierStokes.SimilarityProfile.pullback_smoothAt {h b : ℝ} {f : InnerProfile} {n : ℕ∞} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : ContDiffAt ℝ (↑n) f (inner h p)) : ContDiffAt ℝ (↑n) (pullback h b f) p

theorem NavierStokes.SimilarityProfile.pullback_differentiableAt {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : DifferentiableAt ℝ (pullback h b f) p

theorem NavierStokes.SimilarityProfile.q_hasDerivAt_time {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : HasDerivAt (fun (t : ℝ) => q h (t, p.2)) (CoordinateAlgebra.qTime h (eta h p)) p.1

theorem NavierStokes.SimilarityProfile.eta_hasDerivAt_time {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : HasDerivAt (fun (t : ℝ) => eta h (t, p.2)) (CoordinateAlgebra.etaTime (q h p) h (eta h p)) p.1

theorem NavierStokes.SimilarityProfile.X_hasDerivAt_time {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : HasDerivAt (fun (t : ℝ) => X h (t, p.2)) (CoordinateAlgebra.xTime (q h p) h (eta h p) (X h p)) p.1

theorem NavierStokes.SimilarityProfile.q_hasDerivAt_z {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : HasDerivAt (fun (z : ℝ) => q h (p.1, p.2.1, z)) (CoordinateAlgebra.qAxial (q h p) h (eta h p)) p.2.2

theorem NavierStokes.SimilarityProfile.eta_hasDerivAt_z {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : HasDerivAt (fun (z : ℝ) => eta h (p.1, p.2.1, z)) (CoordinateAlgebra.etaAxial (q h p) h (eta h p)) p.2.2

theorem NavierStokes.SimilarityProfile.X_hasDerivAt_z {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : HasDerivAt (fun (z : ℝ) => X h (p.1, p.2.1, z)) (CoordinateAlgebra.xAxial (q h p) h (eta h p) (X h p)) p.2.2

theorem NavierStokes.SimilarityProfile.fderiv_inner_apply (f : InnerProfile) (w v : InnerPoint) : (fderiv ℝ f w) v = partialX f w * v.1 + partialEta f w * v.2

theorem NavierStokes.SimilarityProfile.hasDerivAt_pullback_time {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : HasDerivAt (fun (t : ℝ) => pullback h b f (t, p.2)) (pullback h (b - 1) (T h b f) p) p.1

The physical time derivative, obtained by product and chain rules.

theorem NavierStokes.SimilarityProfile.hasDerivAt_pullback_z {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : HasDerivAt (fun (z : ℝ) => pullback h b f (p.1, p.2.1, z)) (pullback h (b - D h) (Z h b f) p) p.2.2

The physical axial derivative, including the change of both inner coordinates.

theorem NavierStokes.SimilarityProfile.hasDerivAt_pullback_s {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : HasDerivAt (fun (s : ℝ) => pullback h b f (p.1, s, p.2.2)) (pullback h (b - 1) (partialX f) p) p.2.1

theorem NavierStokes.SimilarityProfile.partialT_pullback {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : partialT (pullback h b f) p = pullback h (b - 1) (T h b f) p

Joint-coordinate time partial, in the same convention as AxisymmetricResidual.

theorem NavierStokes.SimilarityProfile.partialS_pullback {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : partialS (pullback h b f) p = pullback h (b - 1) (partialX f) p

theorem NavierStokes.SimilarityProfile.partialZ_pullback {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : DifferentiableAt ℝ f (inner h p)) : partialZ (pullback h b f) p = pullback h (b - D h) (Z h b f) p

theorem NavierStokes.SimilarityProfile.partialX_smoothAt {f : InnerProfile} {w : InnerPoint} {m n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f w) (hmn : m + 1 ≤ n) : ContDiffAt ℝ m (partialX f) w

theorem NavierStokes.SimilarityProfile.partialEta_smoothAt {f : InnerProfile} {w : InnerPoint} {m n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f w) (hmn : m + 1 ≤ n) : ContDiffAt ℝ m (partialEta f) w

theorem NavierStokes.SimilarityProfile.Z_smoothAt {h b : ℝ} {f : InnerProfile} {w : InnerPoint} (hf : ContDiffAt ℝ 2 f w) (hL : L h w.2 ≠ 0) : ContDiffAt ℝ 1 (Z h b f) w

A local C² profile gives the local C¹ axial coefficient required for the second physical derivative. The denominator condition is explicit.

theorem NavierStokes.SimilarityProfile.T_smoothAt {h b : ℝ} {f : InnerProfile} {w : InnerPoint} (hf : ContDiffAt ℝ 2 f w) (hL : L h w.2 ≠ 0) : ContDiffAt ℝ 1 (T h b f) w

theorem NavierStokes.SimilarityProfile.eventually_C2_inner {h : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : ContDiffAt ℝ 2 f (inner h p)) : ∀ᶠ (p' : PhysicalPoint) in nhds p, ContDiffAt ℝ 2 f (inner h p')

theorem NavierStokes.SimilarityProfile.partialS_partialS_pullback {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : ContDiffAt ℝ 2 f (inner h p)) : partialS (partialS (pullback h b f)) p = pullback h (b - 2) (partialX (partialX f)) p

theorem NavierStokes.SimilarityProfile.partialZ_partialZ_pullback {h b : ℝ} {f : InnerProfile} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (hf : ContDiffAt ℝ 2 f (inner h p)) : partialZ (partialZ (pullback h b f)) p = pullback h (b - 2 * D h) (Z h (b - D h) (Z h b f)) p

The complete iterated axial chain rule for the actual reconstructed profile.

def NavierStokes.SimilarityProfile.physicalDomain (h : ℝ) (U : Set InnerPoint) : Set PhysicalPoint

The natural open physical domain associated to an open inner-profile domain.

Equations

• NavierStokes.SimilarityProfile.physicalDomain h U = {p : NavierStokes.SimilarityProfile.PhysicalPoint | p.1 < 1 ∧ NavierStokes.SimilarityProfile.inner h p ∈ U}

theorem NavierStokes.SimilarityProfile.isOpen_physicalDomain {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {U : Set InnerPoint} (hU : IsOpen U) : IsOpen (physicalDomain h U)

theorem NavierStokes.SimilarityProfile.pullback_smoothOn {h b : ℝ} {f : InnerProfile} {n : ℕ∞} (hh : 0 < h) (hh1 : h < 1 / 2) {U : Set InnerPoint} (hU : IsOpen U) (hf : ContDiffOn ℝ (↑n) f U) : ContDiffOn ℝ (↑n) (pullback h b f) (physicalDomain h U)

Joint smoothness in (t,s,z) on the open coordinate domain; no global smooth extension through the singular time or the edge of the profile is assumed.