Analytic existence of the similarity coordinates

Here a = 2h. We construct the unique positive solution of τ = q - z² q^a for 0 < a < 1 and τ > 0.

noncomputable def NavierStokes.SimilarityCoordinates.forwardScalar (a z q : ℝ) : ℝ

Forward scalar, given by q - z ^ 2 * q ^ a.

Equations

• NavierStokes.SimilarityCoordinates.forwardScalar a z q = q - z ^ 2 * q ^ a

theorem NavierStokes.SimilarityCoordinates.forwardScalar_factor {q : ℝ} (hq : 0 < q) (a z : ℝ) : forwardScalar a z q = q ^ a * (q ^ (1 - a) - z ^ 2)

theorem NavierStokes.SimilarityCoordinates.exists_positive_solution {a τ : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) (z : ℝ) : ∃ (q : ℝ), 0 < q ∧ forwardScalar a z q = τ

A positive solution exists. The proof uses the intermediate value theorem after the change of variable w = q^(1-a).

theorem NavierStokes.SimilarityCoordinates.forwardScalar_lt {a z q₁ q₂ : ℝ} (ha : 0 < a) (ha1 : a < 1) (hq₁ : 0 < q₁) (hqq : q₁ < q₂) (hf₁ : 0 < forwardScalar a z q₁) : forwardScalar a z q₁ < forwardScalar a z q₂

On the region where the scalar map is positive, it is strictly increasing. No global monotonicity below the positive branch is asserted.

theorem NavierStokes.SimilarityCoordinates.positive_solution_unique {a τ z q₁ q₂ : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) (hq₁ : 0 < q₁) (hq₂ : 0 < q₂) (he₁ : forwardScalar a z q₁ = τ) (he₂ : forwardScalar a z q₂ = τ) : q₁ = q₂

theorem NavierStokes.SimilarityCoordinates.existsUnique_positive_solution {a τ : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) (z : ℝ) : ∃! q : ℝ, 0 < q ∧ forwardScalar a z q = τ

noncomputable def NavierStokes.SimilarityCoordinates.coordinateQ (a : ℝ) (p : ℝ × ℝ) : ℝ

The unique positive coordinate, with value 1 outside the intended parameter domain. Only its restriction to that open domain is used.

Equations

• NavierStokes.SimilarityCoordinates.coordinateQ a p = if hp : 0 < a ∧ a < 1 ∧ 0 < p.1 then Classical.choose ⋯ else 1

theorem NavierStokes.SimilarityCoordinates.coordinateQ_spec {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : 0 < coordinateQ a p ∧ forwardScalar a p.2 (coordinateQ a p) = p.1

theorem NavierStokes.SimilarityCoordinates.eq_coordinateQ {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) {q : ℝ} (hq : 0 < q) (he : forwardScalar a p.2 q = p.1) : q = coordinateQ a p

noncomputable def NavierStokes.SimilarityCoordinates.scalarSlope (a z q : ℝ) : ℝ

Scalar slope, given by 1 - z ^ 2 * a * q ^ (a - 1).

Equations

• NavierStokes.SimilarityCoordinates.scalarSlope a z q = 1 - z ^ 2 * a * q ^ (a - 1)

theorem NavierStokes.SimilarityCoordinates.scalarSlope_pos {a z q : ℝ} (ha : 0 < a) (ha1 : a < 1) (hq : 0 < q) (hf : 0 < forwardScalar a z q) : 0 < scalarSlope a z q

noncomputable def NavierStokes.SimilarityCoordinates.forwardMap (a : ℝ) (p : ℝ × ℝ) : ℝ × ℝ

The forward map whose inverse supplies smooth dependence on (τ,z).

Equations

• NavierStokes.SimilarityCoordinates.forwardMap a p = (NavierStokes.SimilarityCoordinates.forwardScalar a p.2 p.1, p.2)

noncomputable def NavierStokes.SimilarityCoordinates.triangularEquiv (m b : ℝ) (hm : m ≠ 0) : (ℝ × ℝ) ≃L[ℝ] ℝ × ℝ

Explicit invertible triangular linear map used by the inverse theorem.

Equations

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

theorem NavierStokes.SimilarityCoordinates.forwardMap_smooth {a : ℝ} {p : ℝ × ℝ} (hp : p.1 ≠ 0) : ContDiffAt ℝ (↑⊤) (forwardMap a) p

theorem NavierStokes.SimilarityCoordinates.forwardMap_hasFDerivAt {a : ℝ} {p : ℝ × ℝ} (hp : p.1 ≠ 0) (hm : scalarSlope a p.2 p.1 ≠ 0) : HasFDerivAt (forwardMap a) (↑(triangularEquiv (scalarSlope a p.2 p.1) (-2 * p.2 * p.1 ^ a) hm)) p

noncomputable def NavierStokes.SimilarityCoordinates.inverseMap (a : ℝ) (p : ℝ × ℝ) : ℝ × ℝ

Inverse map, given by (coordinateQ a p, p.2).

Equations

• NavierStokes.SimilarityCoordinates.inverseMap a p = (NavierStokes.SimilarityCoordinates.coordinateQ a p, p.2)

theorem NavierStokes.SimilarityCoordinates.inverseMap_forwardMap {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hq : 0 < p.1) (hF : 0 < forwardScalar a p.2 p.1) : inverseMap a (forwardMap a p) = p

theorem NavierStokes.SimilarityCoordinates.eventually_inverseMap_forwardMap {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hq : 0 < p.1) (hF : 0 < forwardScalar a p.2 p.1) : ∀ᶠ (x : ℝ × ℝ) in nhds p, inverseMap a (forwardMap a x) = x

theorem NavierStokes.SimilarityCoordinates.inverseMap_smooth_at_image {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hq : 0 < p.1) (hF : 0 < forwardScalar a p.2 p.1) : ContDiffAt ℝ (↑⊤) (inverseMap a) (forwardMap a p)

The canonical inverse is smooth at every image point on the positive branch, by the actual inverse function theorem.

theorem NavierStokes.SimilarityCoordinates.inverseMap_hasFDerivAt_image {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hq : 0 < p.1) (hF : 0 < forwardScalar a p.2 p.1) : HasFDerivAt (inverseMap a) (↑(triangularEquiv (scalarSlope a p.2 p.1) (-2 * p.2 * p.1 ^ a) ⋯).symm) (forwardMap a p)

theorem NavierStokes.SimilarityCoordinates.coordinateQ_smooth {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : ContDiffAt ℝ (↑⊤) (coordinateQ a) p

Smooth dependence on both physical parameters (τ,z) for τ>0.

theorem NavierStokes.SimilarityCoordinates.coordinateQ_smoothOn {a : ℝ} (ha : 0 < a) (ha1 : a < 1) : ContDiffOn ℝ (↑⊤) (coordinateQ a) {p : ℝ × ℝ | 0 < p.1}

theorem NavierStokes.SimilarityCoordinates.coordinateQ_fderiv_apply {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) (v : ℝ × ℝ) : (fderiv ℝ (coordinateQ a) p) v = (v.1 + 2 * p.2 * coordinateQ a p ^ a * v.2) / scalarSlope a p.2 (coordinateQ a p)

Full Fréchet derivative of the actual implicitly defined coordinate.

theorem NavierStokes.SimilarityCoordinates.coordinateQ_hasDerivAt_tau {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (t : ℝ) => coordinateQ a (t, z)) (1 / scalarSlope a z (coordinateQ a (τ, z))) τ

theorem NavierStokes.SimilarityCoordinates.coordinateQ_hasDerivAt_z {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => coordinateQ a (τ, x)) (2 * z * coordinateQ a (τ, z) ^ a / scalarSlope a z (coordinateQ a (τ, z))) z

theorem NavierStokes.SimilarityCoordinates.coordinateQ_hasDerivAt_time {a t z : ℝ} (ha : 0 < a) (ha1 : a < 1) (ht : t < 1) : HasDerivAt (fun (s : ℝ) => coordinateQ a (1 - s, z)) (-1 / scalarSlope a z (coordinateQ a (1 - t, z))) t

The physical time is t=1-τ, giving the required negative sign.

noncomputable def NavierStokes.SimilarityCoordinates.coordinateEta (a : ℝ) (p : ℝ × ℝ) : ℝ

Coordinate eta, given by p.2 / coordinateQ a p ^ ((1 - a) / 2).

Equations

• NavierStokes.SimilarityCoordinates.coordinateEta a p = p.2 / NavierStokes.SimilarityCoordinates.coordinateQ a p ^ ((1 - a) / 2)

theorem NavierStokes.SimilarityCoordinates.coordinateEta_smooth {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : ContDiffAt ℝ (↑⊤) (coordinateEta a) p

theorem NavierStokes.SimilarityCoordinates.coordinateEta_sq {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : coordinateEta a p ^ 2 = p.2 ^ 2 * coordinateQ a p ^ a / coordinateQ a p

theorem NavierStokes.SimilarityCoordinates.coordinateEta_sq_lt_one {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : coordinateEta a p ^ 2 < 1

theorem NavierStokes.SimilarityCoordinates.coordinateEta_abs_lt_one {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : |coordinateEta a p| < 1

theorem NavierStokes.SimilarityCoordinates.coordinateQ_above_threshold {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : |p.2| ^ ((1 - a) / 2)⁻¹ < coordinateQ a p

The branch lies strictly beyond the manuscript's threshold |z|^(1/D), where D=(1-a)/2.

theorem NavierStokes.SimilarityCoordinates.tau_coordinate_identity {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : p.1 = coordinateQ a p * (1 - coordinateEta a p ^ 2)

Both implicit descriptions in equation (3) agree for the constructed coordinates: τ=q(1-η²).

theorem NavierStokes.SimilarityCoordinates.scalarSlope_eq_L {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : scalarSlope a p.2 (coordinateQ a p) = 1 - a * coordinateEta a p ^ 2

The actual Jacobian denominator equals the manuscript's L.

theorem NavierStokes.SimilarityCoordinates.coordinateQ_hasDerivAt_tau_L {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (t : ℝ) => coordinateQ a (t, z)) (1 / (1 - a * coordinateEta a (τ, z) ^ 2)) τ

theorem NavierStokes.SimilarityCoordinates.coordinateQ_hasDerivAt_time_L {a t z : ℝ} (ha : 0 < a) (ha1 : a < 1) (ht : t < 1) : HasDerivAt (fun (s : ℝ) => coordinateQ a (1 - s, z)) (-1 / (1 - a * coordinateEta a (1 - t, z) ^ 2)) t

theorem NavierStokes.SimilarityCoordinates.coordinateEta_hasDerivAt_tau {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (t : ℝ) => coordinateEta a (t, z)) (-((1 - a) / 2) * coordinateEta a (τ, z) / (coordinateQ a (τ, z) * scalarSlope a z (coordinateQ a (τ, z)))) τ

theorem NavierStokes.SimilarityCoordinates.coordinateEta_hasDerivAt_z {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => coordinateEta a (τ, x)) ((1 - coordinateEta a (τ, z) ^ 2) / (coordinateQ a (τ, z) ^ ((1 - a) / 2) * scalarSlope a z (coordinateQ a (τ, z)))) z

theorem NavierStokes.SimilarityCoordinates.coordinateEta_hasDerivAt_time {a t z : ℝ} (ha : 0 < a) (ha1 : a < 1) (ht : t < 1) : HasDerivAt (fun (s : ℝ) => coordinateEta a (1 - s, z)) ((1 - a) / 2 * coordinateEta a (1 - t, z) / (coordinateQ a (1 - t, z) * (1 - a * coordinateEta a (1 - t, z) ^ 2))) t

theorem NavierStokes.SimilarityCoordinates.coordinateEta_hasDerivAt_z_L {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => coordinateEta a (τ, x)) ((1 - coordinateEta a (τ, z) ^ 2) / (coordinateQ a (τ, z) ^ ((1 - a) / 2) * (1 - a * coordinateEta a (τ, z) ^ 2))) z

theorem NavierStokes.SimilarityCoordinates.coordinateQ_hasDerivAt_z_L {a τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => coordinateQ a (τ, x)) (2 * coordinateEta a (τ, z) * coordinateQ a (τ, z) ^ (1 - (1 - a) / 2) / (1 - a * coordinateEta a (τ, z) ^ 2)) z

noncomputable def NavierStokes.SimilarityCoordinates.coordinateX (a s : ℝ) (p : ℝ × ℝ) : ℝ

Coordinate X, given by s / coordinateQ a p.

Equations

• NavierStokes.SimilarityCoordinates.coordinateX a s p = s / NavierStokes.SimilarityCoordinates.coordinateQ a p

theorem NavierStokes.SimilarityCoordinates.coordinateX_smooth {a s : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : 0 < p.1) : ContDiffAt ℝ (↑⊤) (coordinateX a s) p

theorem NavierStokes.SimilarityCoordinates.coordinateX_hasDerivAt_time {a s t z : ℝ} (ha : 0 < a) (ha1 : a < 1) (ht : t < 1) : HasDerivAt (fun (u : ℝ) => coordinateX a s (1 - u, z)) (coordinateX a s (1 - t, z) / (coordinateQ a (1 - t, z) * (1 - a * coordinateEta a (1 - t, z) ^ 2))) t

theorem NavierStokes.SimilarityCoordinates.coordinateX_hasDerivAt_z {a s τ z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hτ : 0 < τ) : HasDerivAt (fun (x : ℝ) => coordinateX a s (τ, x)) (-2 * coordinateEta a (τ, z) * coordinateX a s (τ, z) / (coordinateQ a (τ, z) ^ ((1 - a) / 2) * (1 - a * coordinateEta a (τ, z) ^ 2))) z

theorem NavierStokes.SimilarityCoordinates.physical_coordinates_smooth {a : ℝ} (ha : 0 < a) (ha1 : a < 1) {p : ℝ × ℝ} (hp : p.1 < 1) : ContDiffAt ℝ (↑⊤) (fun (x : ℝ × ℝ) => (coordinateQ a (1 - x.1, x.2), coordinateEta a (1 - x.1, x.2))) p

Joint physical (t,z) smoothness of the actual coordinate functions.

theorem NavierStokes.SimilarityCoordinates.manuscript_coordinate_existsUnique {h τ : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hτ : 0 < τ) (z : ℝ) : ∃! q : ℝ, 0 < q ∧ q - z ^ 2 * q ^ (2 * h) = τ

Equation (3), with exactly the manuscript's exponent 2h.