Endpoint extensions of the actual summed slow base

At nonzero axial coordinate the stable coordinate extension has positive q. The original cutoff schedule therefore gives a locally finite series on an open neighborhood crossing t = 1. No new summation or cutoff choice is made.

For velocity and pressure, the nonzero-axial extension combines with the proved heat exterior on the central plane. The forward-integral potential is only extended at nonzero axial coordinate here; a central-plane gauge correction is a separate construction.

noncomputable def NavierStokes.SlowBaseEndpoint.profileExtension {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h b : ℝ) (f : ℕ → SlowBorelBase.Inner → V) (p : SimilarityProfile.PhysicalPoint) : V

The same coefficient series evaluated at the actual stable coordinate extension, including the original leading power.

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.cartesianProfileExtension {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h b : ℝ) (f : ℕ → SlowBorelBase.Inner → V) (z : ProblemStatement.SpaceTime) : V

Cartesian profile extension, given by profileExtension a h b f (AxisymmetricFields.profilePoint z.1 z.2).

Equations

• NavierStokes.SlowBaseEndpoint.cartesianProfileExtension a h b f z = NavierStokes.SlowBaseEndpoint.profileExtension a h b f (NavierStokes.AxisymmetricFields.profilePoint z.1 z.2)

theorem NavierStokes.SlowBaseEndpoint.profileExtension_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) {p : SimilarityProfile.PhysicalPoint} (hp : p ∈ EndpointCoordinates.domain h) : ContDiffAt ℝ (↑⊤) (profileExtension a h b f) p

theorem NavierStokes.SlowBaseEndpoint.profileExtension_smoothOn {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) : ContDiffOn ℝ (↑⊤) (profileExtension a h b f) (EndpointCoordinates.domain h)

theorem NavierStokes.SlowBaseEndpoint.profileExtension_eq_physical {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (b : ℝ) (f : ℕ → SlowBorelBase.Inner → V) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : profileExtension a h b f p = SlowBorelBase.physicalProfile a h b f p

theorem NavierStokes.SlowBaseEndpoint.profileExtension_eventuallyEq {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (b : ℝ) (f : ℕ → SlowBorelBase.Inner → V) {p : SimilarityProfile.PhysicalPoint} (hp : p.1 < 1) : profileExtension a h b f =ᶠ[nhds p] SlowBorelBase.physicalProfile a h b f

theorem NavierStokes.SlowBaseEndpoint.cartesianProfileExtension_smoothAt {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) {z : ProblemStatement.SpaceTime} (hz : z ∈ EndpointCoordinates.cartesianDomain h) : ContDiffAt ℝ (↑⊤) (cartesianProfileExtension a h b f) z

theorem NavierStokes.SlowBaseEndpoint.cartesianProfileExtension_smoothOn {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {f : ℕ → SlowBorelBase.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (b : ℝ) : ContDiffOn ℝ (↑⊤) (cartesianProfileExtension a h b f) (EndpointCoordinates.cartesianDomain h)

theorem NavierStokes.SlowBaseEndpoint.endpoint_common_finite_index {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : StrictMono a) {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 ⊆ EndpointCoordinates.cartesianDomain h ∧ ∃ (N : ℕ), ∀ z ∈ U, ∀ (f : ℕ → SlowBorelBase.Inner → V), (∀ (j : ℕ), N ≤ j → SlowBorelBase.slowStage a h f j (EndpointCoordinates.cartesianExtension h z) = 0) ∧ SlowBorelBase.slowSum a h f (EndpointCoordinates.cartesianExtension h z) = f 0 (EndpointCoordinates.cartesianExtension h z).2 + ∑ j ∈ Finset.range N, SlowBorelBase.slowStage a h f j (EndpointCoordinates.cartesianExtension h z)

One neighborhood and one finite index work for every coefficient family. In particular the seven bundled fields keep the same schedule.

noncomputable def NavierStokes.SlowBaseEndpoint.streamExtension (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SimilarityProfile.PhysicalProfile

Stream extension, given by profileExtension a h (-CoordinateAlgebra.A h) (bundleComponent C d 0).

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.swirlExtension (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : SimilarityProfile.PhysicalProfile

Swirl extension, given by profileExtension a h (1 / 2 - CoordinateAlgebra.A h) (bundleComponent C d 1).

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.potentialExtension (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

Potential extension, given by AxisymmetricFields.potential (streamExtension a h C d) (swirlExtension a h C d).

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.velocityExtension (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

Velocity extension, given by SpatialCurl.spatialCurl (potentialExtension a h C d).

Equations

• NavierStokes.SlowBaseEndpoint.velocityExtension a h C d = NavierStokes.SpatialCurl.spatialCurl (NavierStokes.SlowBaseEndpoint.potentialExtension a h C d)

noncomputable def NavierStokes.SlowBaseEndpoint.pressureExtension (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.PressureField

Pressure extension, given by cartesianProfileExtension a h (-2 * CoordinateAlgebra.A h) (bundleComponent C d 2).

Equations

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

theorem NavierStokes.SlowBaseEndpoint.potentialExtension_smoothOn {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (potentialExtension a h C d) (EndpointCoordinates.cartesianDomain h)

theorem NavierStokes.SlowBaseEndpoint.velocityExtension_smoothOn {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (velocityExtension a h C d) (EndpointCoordinates.cartesianDomain h)

theorem NavierStokes.SlowBaseEndpoint.pressureExtension_smoothOn {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (pressureExtension a h C d) (EndpointCoordinates.cartesianDomain h)

theorem NavierStokes.SlowBaseEndpoint.potentialExtension_eq (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : SlowBorelBase.Coefficients) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : potentialExtension a h C d z = BaseResidual.summedPotential a h C d z

theorem NavierStokes.SlowBaseEndpoint.potentialExtension_eventuallyEq (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : SlowBorelBase.Coefficients) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : potentialExtension a h C d =ᶠ[nhds z] BaseResidual.summedPotential a h C d

theorem NavierStokes.SlowBaseEndpoint.velocityExtension_eventuallyEq (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : SlowBorelBase.Coefficients) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : velocityExtension a h C d =ᶠ[nhds z] SlowBorelBase.baseVelocity a h C d

theorem NavierStokes.SlowBaseEndpoint.pressureExtension_eventuallyEq (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : SlowBorelBase.Coefficients) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : pressureExtension a h C d =ᶠ[nhds z] SlowBorelBase.basePressure a h C d

noncomputable def NavierStokes.SlowBaseEndpoint.potentialNonzeroAxial {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (BaseResidual.summedPotential a h C d) x

The original forward-integral potential extends at every nonzero axial endpoint, with exactly the original cutoff schedule.

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.velocityNonzeroAxial {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (SlowBorelBase.baseVelocity a h C d) x

Velocity nonzero axial, bundling value, domain, isOpen, mem and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.pressureNonzeroAxial {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (SlowBorelBase.basePressure a h C d) x

Pressure nonzero axial, bundling value, domain, isOpen, mem and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.radialAnchor (p : SimilarityProfile.PhysicalPoint) : SimilarityProfile.PhysicalPoint

The fixed physical radial anchor used for the exact gauge correction.

Equations

• NavierStokes.SlowBaseEndpoint.radialAnchor p = (p.1, 1, p.2.2)

theorem NavierStokes.SlowBaseEndpoint.radialAnchor_smooth : ContDiff ℝ (↑⊤) radialAnchor

noncomputable def NavierStokes.SlowBaseEndpoint.anchoredPotential (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

This is the literal anchored-potential formula. Equality of its curl with the original velocity is proved in the separate gauge module.

Equations

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

noncomputable def NavierStokes.SlowBaseEndpoint.anchoredPotentialExtension (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : ProblemStatement.VelocityField

Anchored potential extension, constructed using AxisymmetricFields.potential.

Equations

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

theorem NavierStokes.SlowBaseEndpoint.anchoredPotentialExtension_smoothOn {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) : ContDiffOn ℝ (↑⊤) (anchoredPotentialExtension a h C d) (EndpointCoordinates.cartesianDomain h)

theorem NavierStokes.SlowBaseEndpoint.anchoredPotentialExtension_eq (a : ℕ → ℕ) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (C : ℝ) (d : SlowBorelBase.Coefficients) {z : ProblemStatement.SpaceTime} (hz : z.1 < 1) : anchoredPotentialExtension a h C d z = anchoredPotential a h C d z

noncomputable def NavierStokes.SlowBaseEndpoint.anchoredPotentialNonzeroAxial {a : ℕ → ℕ} (ha : StrictMono a) {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (C : ℝ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (anchoredPotential a h C d) x

The exact anchored potential also extends at every nonzero axial endpoint. In particular the subtracted gauge uses the same sum and schedule.

Equations

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

theorem NavierStokes.SlowBaseEndpoint.oneSidedExtension_of_closed_local {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {f g : ProblemStatement.SpaceTime → V} {x : ProblemStatement.Space} {U : Set ProblemStatement.SpaceTime} (hU : IsOpen U) (hxU : (1, x) ∈ U) (hg : ContDiffOn ℝ (↑⊤) g (U ∩ SpacetimeEndpoint.closedPast 1)) (he : Set.EqOn g f (U ∩ SpacetimeEndpoint.openPast 1)) : Nonempty (JointResidualLimits.OneSidedExtension f x)

Convert a genuine locally smooth closed-side continuation into an ambient smooth extension. A local bump and the already proved joint Taylor--Borel extension are the actual construction.

theorem NavierStokes.SlowBaseEndpoint.radialEnergy_pos_of_nonzero_of_axial_zero {x : ProblemStatement.Space} (hx : x ≠ 0) (hz : x.ofLp 2 = 0) : 0 < AxisymmetricFields.radialEnergy x

theorem NavierStokes.SlowBaseEndpoint.realized_fields_awayExtensions {F : OutgoingProfile.Profile} (W : NominalProfile.Witness F) {D : ProfileHistories.RadialDomain} (Q : ProfileHistories.Profiles D) {S : Set ℝ} {lo hi : ℝ} (M : AssembledSlowBase.FiniteModification W Q S lo hi) {s : GlobalSlowProfiles.Scheme S F.data.h W.axis.normalization} {d : SlowBorelBase.Coefficients} (hd : ModulatedExterior.RealizesScheme s ⋯ d) (hbase : s.base = (AssembledSlowBase.modifiedScheme W Q M).base) (houter : s.B = AssembledSlowBase.nominalOuterRadius W) (hds : SlowBorelBase.SmoothCoefficients d) (henergy : ModulatedExterior.RestoredSquaredSwirl W Q) {a : ℕ → ℕ} (ha : StrictMono a) : JointResidualLimits.AwayExtensions (SlowBorelBase.baseVelocity a F.data.h W.axis.normalization d) ∧ JointResidualLimits.AwayExtensions (SlowBorelBase.basePressure a F.data.h W.axis.normalization d)

For the actual repaired scheme, velocity and pressure have ambient smooth continuations at every nonzero point of the terminal slice.

noncomputable def NavierStokes.SlowBaseEndpoint.finalPotentialNonzeroAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (FinalSlowBase.vectorPotential H v upper B) x

The original potential of the actual entrance-aligned base extends at nonzero axial coordinate, with its selected scale sequence unchanged.

Equations

• NavierStokes.SlowBaseEndpoint.finalPotentialNonzeroAxial H v upper B hx = NavierStokes.SlowBaseEndpoint.potentialNonzeroAxial ⋯ ⋯ ⋯ ⋯ W.axis.normalization hx

noncomputable def NavierStokes.SlowBaseEndpoint.finalVelocityNonzeroAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (FinalSlowBase.velocity H v upper B) x

Final velocity nonzero axial, constructed using velocityNonzeroAxial.

Equations

• NavierStokes.SlowBaseEndpoint.finalVelocityNonzeroAxial H v upper B hx = NavierStokes.SlowBaseEndpoint.velocityNonzeroAxial ⋯ ⋯ ⋯ ⋯ W.axis.normalization hx

noncomputable def NavierStokes.SlowBaseEndpoint.finalPressureNonzeroAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (FinalSlowBase.pressure H v upper B) x

Final pressure nonzero axial, constructed using pressureNonzeroAxial.

Equations

• NavierStokes.SlowBaseEndpoint.finalPressureNonzeroAxial H v upper B hx = NavierStokes.SlowBaseEndpoint.pressureNonzeroAxial ⋯ ⋯ ⋯ ⋯ W.axis.normalization hx

noncomputable def NavierStokes.SlowBaseEndpoint.finalAnchoredPotentialNonzeroAxial {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) : JointResidualLimits.OneSidedExtension (anchoredPotential (FinalSlowBase.scales H v upper B) F.data.h W.axis.normalization (FinalSlowBase.coefficients H v)) x

Final anchored potential nonzero axial, constructed using anchoredPotentialNonzeroAxial.

Equations

• NavierStokes.SlowBaseEndpoint.finalAnchoredPotentialNonzeroAxial H v upper B hx = NavierStokes.SlowBaseEndpoint.anchoredPotentialNonzeroAxial ⋯ ⋯ ⋯ ⋯ W.axis.normalization hx

theorem NavierStokes.SlowBaseEndpoint.final_fields_awayExtensions {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : JointResidualLimits.AwayExtensions (FinalSlowBase.velocity H v upper B) ∧ JointResidualLimits.AwayExtensions (FinalSlowBase.pressure H v upper B)

This includes the central plane and the spatial axis away from zero. The inputs are the actual finite profile witnesses, not endpoint assumptions.

theorem NavierStokes.SlowBaseEndpoint.final_potential_jets_tendsto {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {x : ProblemStatement.Space} (hx : x.ofLp 2 ≠ 0) (n : ℕ) : Filter.Tendsto (iteratedFDeriv ℝ n (FinalSlowBase.vectorPotential H v upper B)) (nhdsWithin (1, x) (SpacetimeEndpoint.openPast 1)) (nhds (iteratedFDeriv ℝ n (finalPotentialNonzeroAxial H v upper B hx).value (1, x)))

theorem NavierStokes.SlowBaseEndpoint.constructed_fields_awayExtensions (upper : ℝ) (B : ℕ) : JointResidualLimits.AwayExtensions (FinalSlowBase.velocity ⋯ FinalSlowBase.actualProfile.modulation upper B) ∧ JointResidualLimits.AwayExtensions (FinalSlowBase.pressure ⋯ FinalSlowBase.actualProfile.modulation upper B)

The already constructed finite profile gives actual endpoint extensions for the selected slow base without another profile input.