Actual similarity coordinates across the nonzero axial endpoint

At t=1, z != 0, the explicit positive root lies on the regular stable branch. The extension below is built from that branch and agrees with all actual physical coordinate jets at every point with t<1.

@[reducible, inline]

abbrev NavierStokes.EndpointCoordinates.PhysicalPoint : Type

Physical point: an abbreviation for SimilarityProfile.PhysicalPoint.

Equations

• NavierStokes.EndpointCoordinates.PhysicalPoint = NavierStokes.SimilarityProfile.PhysicalPoint

@[reducible, inline]

abbrev NavierStokes.EndpointCoordinates.Chart : Type

Chart: an abbreviation for SlowBorelBase.Chart.

Equations

• NavierStokes.EndpointCoordinates.Chart = NavierStokes.SlowBorelBase.Chart

noncomputable def NavierStokes.EndpointCoordinates.endpointRoot (a z : ℝ) : ℝ

The positive solution of the zero-time similarity equation.

Equations

• NavierStokes.EndpointCoordinates.endpointRoot a z = (z ^ 2) ^ (1 - a)⁻¹

theorem NavierStokes.EndpointCoordinates.endpointRoot_pos (a : ℝ) {z : ℝ} (hz : z ≠ 0) : 0 < endpointRoot a z

theorem NavierStokes.EndpointCoordinates.endpointRoot_power {a z : ℝ} (ha1 : a < 1) : endpointRoot a z ^ (1 - a) = z ^ 2

theorem NavierStokes.EndpointCoordinates.endpointRoot_equation {a z : ℝ} (ha1 : a < 1) (hz : z ≠ 0) : SimilarityCoordinates.forwardScalar a z (endpointRoot a z) = 0

theorem NavierStokes.EndpointCoordinates.endpointRoot_slope {a z : ℝ} (ha1 : a < 1) (hz : z ≠ 0) : SimilarityCoordinates.scalarSlope a z (endpointRoot a z) = 1 - a

theorem NavierStokes.EndpointCoordinates.zeroTime_mem_stableTarget {a z : ℝ} (_ha : 0 < a) (ha1 : a < 1) (hz : z ≠ 0) : (0, z) ∈ PositiveRepresentatives.stableTarget a

Every nonzero point of the zero-time axis belongs to the actual regular stable target. No inverse-coordinate extension is assumed.

theorem NavierStokes.EndpointCoordinates.stableInverse_zeroTime {a z : ℝ} (ha : 0 < a) (ha1 : a < 1) (hz : z ≠ 0) : PositiveRepresentatives.stableInverse a (0, z) = (endpointRoot a z, z)

noncomputable def NavierStokes.EndpointCoordinates.timeAxial (p : PhysicalPoint) : ℝ × ℝ

Time axial, given by (1 - p.1, p.2.2).

Equations

• NavierStokes.EndpointCoordinates.timeAxial p = (1 - p.1, p.2.2)

noncomputable def NavierStokes.EndpointCoordinates.domain (h : ℝ) : Set PhysicalPoint

Domain, given by timeAxial ⁻¹' PositiveRepresentatives.stableTarget (2 * h).

Equations

• NavierStokes.EndpointCoordinates.domain h = NavierStokes.EndpointCoordinates.timeAxial ⁻¹' NavierStokes.PositiveRepresentatives.stableTarget (2 * h)

noncomputable def NavierStokes.EndpointCoordinates.qExtension (h : ℝ) (p : PhysicalPoint) : ℝ

Q extension, given by (PositiveRepresentatives.stableInverse (2 * h) (timeAxial p)).1.

Equations

• NavierStokes.EndpointCoordinates.qExtension h p = (NavierStokes.PositiveRepresentatives.stableInverse (2 * h) (NavierStokes.EndpointCoordinates.timeAxial p)).1

noncomputable def NavierStokes.EndpointCoordinates.etaExtension (h : ℝ) (p : PhysicalPoint) : ℝ

Eta extension, given by p.2.2 / qExtension h p ^ ((1 - 2 * h) / 2).

Equations

• NavierStokes.EndpointCoordinates.etaExtension h p = p.2.2 / NavierStokes.EndpointCoordinates.qExtension h p ^ ((1 - 2 * h) / 2)

noncomputable def NavierStokes.EndpointCoordinates.XExtension (h : ℝ) (p : PhysicalPoint) : ℝ

X extension, given by p.2.1 / qExtension h p.

Equations

• NavierStokes.EndpointCoordinates.XExtension h p = p.2.1 / NavierStokes.EndpointCoordinates.qExtension h p

noncomputable def NavierStokes.EndpointCoordinates.innerExtension (h : ℝ) (p : PhysicalPoint) : ℝ × ℝ

Inner extension, given by (XExtension h p, etaExtension h p).

Equations

• NavierStokes.EndpointCoordinates.innerExtension h p = (NavierStokes.EndpointCoordinates.XExtension h p, NavierStokes.EndpointCoordinates.etaExtension h p)

noncomputable def NavierStokes.EndpointCoordinates.chartExtension (h : ℝ) (p : PhysicalPoint) : Chart

Chart extension, given by (qExtension h p, innerExtension h p).

Equations

• NavierStokes.EndpointCoordinates.chartExtension h p = (NavierStokes.EndpointCoordinates.qExtension h p, NavierStokes.EndpointCoordinates.innerExtension h p)

theorem NavierStokes.EndpointCoordinates.timeAxial_smooth : ContDiff ℝ (↑⊤) timeAxial

theorem NavierStokes.EndpointCoordinates.domain_open (h : ℝ) : IsOpen (domain h)

theorem NavierStokes.EndpointCoordinates.endpoint_mem_domain {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (s : ℝ) {z : ℝ} (hz : z ≠ 0) : (1, s, z) ∈ domain h

theorem NavierStokes.EndpointCoordinates.past_mem_domain {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : p ∈ domain h

theorem NavierStokes.EndpointCoordinates.qExtension_pos {h : ℝ} {p : PhysicalPoint} (hp : p ∈ domain h) : 0 < qExtension h p

theorem NavierStokes.EndpointCoordinates.qExtension_equation {h : ℝ} {p : PhysicalPoint} (hp : p ∈ domain h) : SimilarityCoordinates.forwardScalar (2 * h) p.2.2 (qExtension h p) = 1 - p.1

theorem NavierStokes.EndpointCoordinates.qExtension_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p ∈ domain h) : ContDiffAt ℝ (↑⊤) (qExtension h) p

theorem NavierStokes.EndpointCoordinates.innerExtension_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p ∈ domain h) : ContDiffAt ℝ (↑⊤) (innerExtension h) p

theorem NavierStokes.EndpointCoordinates.chartExtension_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p ∈ domain h) : ContDiffAt ℝ (↑⊤) (chartExtension h) p

theorem NavierStokes.EndpointCoordinates.chartExtension_smoothOn {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (chartExtension h) (domain h)

theorem NavierStokes.EndpointCoordinates.qExtension_endpoint {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (s : ℝ) {z : ℝ} (hz : z ≠ 0) : qExtension h (1, s, z) = endpointRoot (2 * h) z

theorem NavierStokes.EndpointCoordinates.chartExtension_endpoint {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (s : ℝ) {z : ℝ} (hz : z ≠ 0) : chartExtension h (1, s, z) = (endpointRoot (2 * h) z, s / endpointRoot (2 * h) z, z / endpointRoot (2 * h) z ^ ((1 - 2 * h) / 2))

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

theorem NavierStokes.EndpointCoordinates.innerExtension_eq_physical {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : innerExtension h p = SimilarityProfile.inner h p

theorem NavierStokes.EndpointCoordinates.chartExtension_eq_physical {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : chartExtension h p = SlowBorelBase.physicalChart h p

theorem NavierStokes.EndpointCoordinates.chartExtension_eventuallyEq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) : chartExtension h =ᶠ[nhds p] SlowBorelBase.physicalChart h

theorem NavierStokes.EndpointCoordinates.jets_eq_of_eventuallyEq {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {f g : E → V} {p : E} (he : f =ᶠ[nhds p] g) (n : ℕ) : iteratedFDeriv ℝ n f p = iteratedFDeriv ℝ n g p

theorem NavierStokes.EndpointCoordinates.chartExtension_jets_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {p : PhysicalPoint} (hp : p.1 < 1) (n : ℕ) : iteratedFDeriv ℝ n (chartExtension h) p = iteratedFDeriv ℝ n (SlowBorelBase.physicalChart h) p

noncomputable def NavierStokes.EndpointCoordinates.lowerDomain (h c : ℝ) : Set PhysicalPoint

Lower domain, given by domain h ∩ {p | c < qExtension h p}.

Equations

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

theorem NavierStokes.EndpointCoordinates.lowerDomain_open {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (c : ℝ) : IsOpen (lowerDomain h c)

theorem NavierStokes.EndpointCoordinates.endpoint_neighborhood {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (s : ℝ) {z : ℝ} (hz : z ≠ 0) : ∃ (U : Set PhysicalPoint), IsOpen U ∧ (1, s, z) ∈ U ∧ U ⊆ domain h ∧ ContDiffOn ℝ (↑⊤) (chartExtension h) U ∧ 0 < endpointRoot (2 * h) z / 2 ∧ ∀ p ∈ U, endpointRoot (2 * h) z / 2 < qExtension h p ∧ (p.1 < 1 → endpointRoot (2 * h) z / 2 < SimilarityProfile.q h p)

An actual open neighborhood across the endpoint, with an explicit positive lower bound. The bound applies to the physical coordinate on its past portion and to the smooth extension throughout the neighborhood.

The actual Cartesian chart used by the slow base

noncomputable def NavierStokes.EndpointCoordinates.cartesianDomain (h : ℝ) : Set ProblemStatement.SpaceTime

Cartesian domain, given by (fun z => AxisymmetricFields.profilePoint z.1 z.2) ⁻¹' domain h.

Equations

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

noncomputable def NavierStokes.EndpointCoordinates.cartesianExtension (h : ℝ) (z : ProblemStatement.SpaceTime) : Chart

Cartesian extension, given by chartExtension h (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.EndpointCoordinates.cartesianExtension h z = NavierStokes.EndpointCoordinates.chartExtension h (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.EndpointCoordinates.cartesianDomain_open (h : ℝ) : IsOpen (cartesianDomain h)

theorem NavierStokes.EndpointCoordinates.cartesian_endpoint_mem {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : (1, x) ∈ cartesianDomain h

theorem NavierStokes.EndpointCoordinates.cartesianExtension_smoothAt {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianDomain h) : ContDiffAt ℝ (↑⊤) (cartesianExtension h) z

theorem NavierStokes.EndpointCoordinates.cartesianExtension_smoothOn {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContDiffOn ℝ (↑⊤) (cartesianExtension h) (cartesianDomain h)

theorem NavierStokes.EndpointCoordinates.cartesianExtension_pos {h : ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianDomain h) : 0 < (cartesianExtension h z).1

theorem NavierStokes.EndpointCoordinates.cartesianExtension_X_nonneg {h : ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianDomain h) : 0 ≤ (cartesianExtension h z).2.1

theorem NavierStokes.EndpointCoordinates.cartesianExtension_endpoint {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : cartesianExtension h (1, x) = (endpointRoot (2 * h) (x.ofLp 2), AxisymmetricFields.radialEnergy x / endpointRoot (2 * h) (x.ofLp 2), x.ofLp 2 / endpointRoot (2 * h) (x.ofLp 2) ^ ((1 - 2 * h) / 2))

theorem NavierStokes.EndpointCoordinates.cartesianExtension_eq_physical {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : cartesianExtension h z = SlowBorelBase.cartesianChart h z

theorem NavierStokes.EndpointCoordinates.cartesianExtension_eventuallyEq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : cartesianExtension h =ᶠ[nhds z] SlowBorelBase.cartesianChart h

theorem NavierStokes.EndpointCoordinates.cartesianExtension_jets_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) (n : ℕ) : iteratedFDeriv ℝ n (cartesianExtension h) z = iteratedFDeriv ℝ n (SlowBorelBase.cartesianChart h) z

Equality is for arbitrary orders of the genuine space-time derivative.

theorem NavierStokes.EndpointCoordinates.cartesian_endpoint_neighborhood {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ U ⊆ cartesianDomain h ∧ ContDiffOn ℝ (↑⊤) (cartesianExtension h) U ∧ 0 < endpointRoot (2 * h) (x.ofLp 2) / 2 ∧ ∀ z ∈ U, endpointRoot (2 * h) (x.ofLp 2) / 2 < (cartesianExtension h z).1 ∧ (z.1 < 1 → endpointRoot (2 * h) (x.ofLp 2) / 2 < (SlowBorelBase.cartesianChart h z).1)

Smooth composition and genuine derivative transfer

theorem NavierStokes.EndpointCoordinates.composition_smoothAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {z : ProblemStatement.SpaceTime} (hz : z ∈ cartesianDomain h) {f : Chart → V} (hf : ContDiffAt ℝ (↑⊤) f (cartesianExtension h z)) : ContDiffAt ℝ (↑⊤) (fun (p : ProblemStatement.SpaceTime) => f (cartesianExtension h p)) z

theorem NavierStokes.EndpointCoordinates.composition_endpoint_smoothAt {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) {f : Chart → V} (hf : ContDiffAt ℝ (↑⊤) f (cartesianExtension h (1, x))) : ContDiffAt ℝ (↑⊤) (fun (p : ProblemStatement.SpaceTime) => f (cartesianExtension h p)) (1, x)

theorem NavierStokes.EndpointCoordinates.composition_jets_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (f : Chart → V) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) (n : ℕ) : iteratedFDeriv ℝ n (fun (p : ProblemStatement.SpaceTime) => f (cartesianExtension h p)) z = iteratedFDeriv ℝ n (fun (p : ProblemStatement.SpaceTime) => f (SlowBorelBase.cartesianChart h p)) z