Algebra of the manuscript coordinates

This module checks the algebra in equations (3)--(5). It does not construct a smooth inverse coordinate chart, a Navier--Stokes solution, or a singularity. q ^ b below denotes the real power, while η ^ 2 is a natural power.

noncomputable def NavierStokes.CoordinateAlgebra.A (h : ℝ) : ℝ

A, given by 1 / 2 + h.

Equations

• NavierStokes.CoordinateAlgebra.A h = 1 / 2 + h

noncomputable def NavierStokes.CoordinateAlgebra.D (h : ℝ) : ℝ

D, given by 1 / 2 - h.

Equations

• NavierStokes.CoordinateAlgebra.D h = 1 / 2 - h

def NavierStokes.CoordinateAlgebra.d (η : ℝ) : ℝ

D, given by 1 - η ^ 2.

Equations

• NavierStokes.CoordinateAlgebra.d η = 1 - η ^ 2

def NavierStokes.CoordinateAlgebra.L (h η : ℝ) : ℝ

L, given by 1 - 2 * h * η ^ 2.

Equations

• NavierStokes.CoordinateAlgebra.L h η = 1 - 2 * h * η ^ 2

theorem NavierStokes.CoordinateAlgebra.A_add_D (h : ℝ) : A h + D h = 1

theorem NavierStokes.CoordinateAlgebra.L_sub_two_D (h η : ℝ) : L h η - 2 * D h * η ^ 2 = d η

theorem NavierStokes.CoordinateAlgebra.d_add_two_D (h η : ℝ) : d η + 2 * D h * η ^ 2 = L h η

theorem NavierStokes.CoordinateAlgebra.forward_coordinate_identity {q : ℝ} (hq : 0 < q) (h η : ℝ) : q * d η = q - (q ^ D h * η) ^ 2 * q ^ (2 * h)

Eliminating η from z = q^D η gives the implicit formula for τ.

theorem NavierStokes.CoordinateAlgebra.D_pos {h : ℝ} (hh : h < 1 / 2) : 0 < D h

theorem NavierStokes.CoordinateAlgebra.d_pos {η : ℝ} (hη : η ^ 2 < 1) : 0 < d η

theorem NavierStokes.CoordinateAlgebra.L_pos {h η : ℝ} (hh₀ : 0 ≤ h) (hh : h < 1 / 2) (hη : η ^ 2 ≤ 1) : 0 < L h η

The explicit smallness condition needed for the manuscript's L > 0.

theorem NavierStokes.CoordinateAlgebra.jacobian_det {q : ℝ} (hq : q ≠ 0) (h η : ℝ) : d η * q ^ D h - -2 * q * η * (D h * η * (q ^ D h / q)) = q ^ D h * L h η

Determinant of the forward coordinate Jacobian for τ = q (1-η²) and z = q^D η. The derivative of q^D is written as D * (q^D/q) on the positive half-line.

theorem NavierStokes.CoordinateAlgebra.jacobian_det_pos {q h η : ℝ} (hq : 0 < q) (hh₀ : 0 ≤ h) (hh : h < 1 / 2) (hη : η ^ 2 ≤ 1) : 0 < d η * q ^ D h - -2 * q * η * (D h * η * (q ^ D h / q))

noncomputable def NavierStokes.CoordinateAlgebra.inverseQ (q h η τ' z' : ℝ) : ℝ

The inverse Jacobian acting on (τ',z'), first component.

Equations

• NavierStokes.CoordinateAlgebra.inverseQ q h η τ' z' = (τ' + 2 * q * η * z' / q ^ NavierStokes.CoordinateAlgebra.D h) / NavierStokes.CoordinateAlgebra.L h η

noncomputable def NavierStokes.CoordinateAlgebra.inverseEta (q h η τ' z' : ℝ) : ℝ

The inverse Jacobian acting on (τ',z'), second component.

Equations

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

theorem NavierStokes.CoordinateAlgebra.inverse_satisfies_tau {q h η : ℝ} (hq : 0 < q) (hL : L h η ≠ 0) (τ' z' : ℝ) : d η * inverseQ q h η τ' z' - 2 * q * η * inverseEta q h η τ' z' = τ'

theorem NavierStokes.CoordinateAlgebra.inverse_satisfies_z {q h η : ℝ} (hq : 0 < q) (hL : L h η ≠ 0) (τ' z' : ℝ) : D h * η * (q ^ D h / q) * inverseQ q h η τ' z' + q ^ D h * inverseEta q h η τ' z' = z'

theorem NavierStokes.CoordinateAlgebra.inverseQ_recover {q h η : ℝ} (hq : 0 < q) (hL : L h η ≠ 0) (q' η' : ℝ) : inverseQ q h η (d η * q' - 2 * q * η * η') (D h * η * (q ^ D h / q) * q' + q ^ D h * η') = q'

theorem NavierStokes.CoordinateAlgebra.inverseEta_recover {q h η : ℝ} (hq : 0 < q) (hL : L h η ≠ 0) (q' η' : ℝ) : inverseEta q h η (d η * q' - 2 * q * η * η') (D h * η * (q ^ D h / q) * q' + q ^ D h * η') = η'

theorem NavierStokes.CoordinateAlgebra.rates_unique {q h η q' η' τ' z' : ℝ} (hq : 0 < q) (hL : L h η ≠ 0) (hτ : d η * q' - 2 * q * η * η' = τ') (hz : D h * η * (q ^ D h / q) * q' + q ^ D h * η' = z') : q' = inverseQ q h η τ' z' ∧ η' = inverseEta q h η τ' z'

Uniqueness of the coordinate rates from the two forward differential relations. This is a pointwise algebraic claim, with no inverse-function existence assumption hidden in its statement.

noncomputable def NavierStokes.CoordinateAlgebra.qTime (h η : ℝ) : ℝ

Q time, given by -1 / L h η.

Equations

• NavierStokes.CoordinateAlgebra.qTime h η = -1 / NavierStokes.CoordinateAlgebra.L h η

noncomputable def NavierStokes.CoordinateAlgebra.etaTime (q h η : ℝ) : ℝ

Eta time, given by D h * η / (q * L h η).

Equations

• NavierStokes.CoordinateAlgebra.etaTime q h η = NavierStokes.CoordinateAlgebra.D h * η / (q * NavierStokes.CoordinateAlgebra.L h η)

noncomputable def NavierStokes.CoordinateAlgebra.xTime (q h η X : ℝ) : ℝ

X time, given by X / (q * L h η).

Equations

• NavierStokes.CoordinateAlgebra.xTime q h η X = X / (q * NavierStokes.CoordinateAlgebra.L h η)

noncomputable def NavierStokes.CoordinateAlgebra.qAxial (q h η : ℝ) : ℝ

Q axial, given by 2 * η * q / (q ^ D h * L h η).

Equations

• NavierStokes.CoordinateAlgebra.qAxial q h η = 2 * η * q / (q ^ NavierStokes.CoordinateAlgebra.D h * NavierStokes.CoordinateAlgebra.L h η)

noncomputable def NavierStokes.CoordinateAlgebra.etaAxial (q h η : ℝ) : ℝ

Eta axial, given by d η / (q ^ D h * L h η).

Equations

• NavierStokes.CoordinateAlgebra.etaAxial q h η = NavierStokes.CoordinateAlgebra.d η / (q ^ NavierStokes.CoordinateAlgebra.D h * NavierStokes.CoordinateAlgebra.L h η)

noncomputable def NavierStokes.CoordinateAlgebra.xAxial (q h η X : ℝ) : ℝ

X axial, given by -2 * η * X / (q ^ D h * L h η).

Equations

• NavierStokes.CoordinateAlgebra.xAxial q h η X = -2 * η * X / (q ^ NavierStokes.CoordinateAlgebra.D h * NavierStokes.CoordinateAlgebra.L h η)

theorem NavierStokes.CoordinateAlgebra.time_rates (q h η : ℝ) : inverseQ q h η (-1) 0 = qTime h η ∧ inverseEta q h η (-1) 0 = etaTime q h η

theorem NavierStokes.CoordinateAlgebra.axial_rates (q h η : ℝ) : inverseQ q h η 0 1 = qAxial q h η ∧ inverseEta q h η 0 1 = etaAxial q h η

theorem NavierStokes.CoordinateAlgebra.qAxial_rpow {q : ℝ} (hq : 0 < q) (h η : ℝ) : qAxial q h η = 2 * η * q ^ (1 - D h) / L h η

theorem NavierStokes.CoordinateAlgebra.xTime_from_qTime (q h η X : ℝ) : xTime q h η X = -(X / q) * qTime h η

theorem NavierStokes.CoordinateAlgebra.xAxial_from_qAxial {q : ℝ} (hq : q ≠ 0) (h η X : ℝ) : xAxial q h η X = -(X / q) * qAxial q h η

noncomputable def NavierStokes.CoordinateAlgebra.timeCoeff (b h η X F FX Fη : ℝ) : ℝ

The T_b coefficient in equation (4), at a profile jet (F,FX,Fη).

Equations

• NavierStokes.CoordinateAlgebra.timeCoeff b h η X F FX Fη = (-b * F + NavierStokes.CoordinateAlgebra.D h * η * Fη + X * FX) / NavierStokes.CoordinateAlgebra.L h η

noncomputable def NavierStokes.CoordinateAlgebra.axialCoeff (b h η X F FX Fη : ℝ) : ℝ

The Z_b coefficient in equation (4), at a profile jet (F,FX,Fη).

Equations

• NavierStokes.CoordinateAlgebra.axialCoeff b h η X F FX Fη = (2 * η * b * F + NavierStokes.CoordinateAlgebra.d η * Fη - 2 * η * X * FX) / NavierStokes.CoordinateAlgebra.L h η

theorem NavierStokes.CoordinateAlgebra.time_chain_coefficient {q : ℝ} (hq : 0 < q) (b h η X F FX Fη : ℝ) : b * q ^ (b - 1) * qTime h η * F + q ^ b * (FX * xTime q h η X + Fη * etaTime q h η) = q ^ (b - 1) * timeCoeff b h η X F FX Fη

Product/chain-rule expression for the time derivative of q^b F(X,η). The theorem checks its exact coefficient and power of q; analytic derivative hypotheses are separate from this algebraic identity.

theorem NavierStokes.CoordinateAlgebra.axial_chain_coefficient {q : ℝ} (hq : 0 < q) (b h η X F FX Fη : ℝ) : b * q ^ (b - 1) * qAxial q h η * F + q ^ b * (FX * xAxial q h η X + Fη * etaAxial q h η) = q ^ (b - D h) * axialCoeff b h η X F FX Fη

Product/chain-rule expression for the axial derivative of q^b F(X,η).

theorem NavierStokes.CoordinateAlgebra.incompressibility_numerator (h η X U UX Uη Ubar UbarX Ubarη UbarηX : ℝ) (hU : Ubar + X * UbarX = U) (hUη : Ubarη + X * UbarηX = Uη) : 2 * η * U - 2 * D h * η * Ubar - d η * Ubarη + X * (2 * η * UX - 2 * D h * η * UbarX - d η * UbarηX) = 2 * A h * η * U - d η * Uη + 2 * η * X * UX

Algebra behind the incompressibility formula (5). The two hypotheses are the primitive identities (X Ubar)_X = U and its η derivative.

theorem NavierStokes.CoordinateAlgebra.incompressibility_coefficient (h η X U UX Uη Ubar UbarX Ubarη UbarηX : ℝ) (hU : Ubar + X * UbarX = U) (hUη : Ubarη + X * UbarηX = Uη) : (2 * η * U - 2 * D h * η * Ubar - d η * Ubarη + X * (2 * η * UX - 2 * D h * η * UbarX - d η * UbarηX)) / L h η = -axialCoeff (-A h) h η X U UX Uη