A radial gauge for the actual slow-base potential

Subtracting the swirl potential at the fixed physical coordinate s = 1 removes every radial integration constant, including those of the positive slow orders. The subtraction is a genuine curl-free axial field. In the heat exterior the resulting potential is a finite, anchored heat primitive, which has a smooth extension through the terminal central plane.

@[reducible, inline]

abbrev NavierStokes.TailGaugePotential.Point : Type

Point: an abbreviation for AxisymmetricFields.ProfilePoint.

Equations

• NavierStokes.TailGaugePotential.Point = NavierStokes.AxisymmetricFields.ProfilePoint

noncomputable def NavierStokes.TailGaugePotential.radialAnchor (p : Point) : Point

The radial anchor is physical and independent of the similarity scale.

Equations

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

noncomputable def NavierStokes.TailGaugePotential.radialNormalize (K : Point → ℝ) (p : Point) : ℝ

Radial normalize, given by K p - K (radialAnchor p).

Equations

• NavierStokes.TailGaugePotential.radialNormalize K p = K p - K (NavierStokes.TailGaugePotential.radialAnchor p)

theorem NavierStokes.TailGaugePotential.radialAnchor_contDiff {n : WithTop ℕ∞} : ContDiff ℝ n radialAnchor

theorem NavierStokes.TailGaugePotential.radialNormalize_contDiffAt {K : Point → ℝ} {p : Point} {n : WithTop ℕ∞} (hK : ContDiffAt ℝ n K p) (hA : ContDiffAt ℝ n K (radialAnchor p)) : ContDiffAt ℝ n (radialNormalize K) p

theorem NavierStokes.TailGaugePotential.radial_slice_hasDerivAt {K : Point → ℝ} {p : Point} (hK : DifferentiableAt ℝ K p) : HasDerivAt (fun (s : ℝ) => K (p.1, s, p.2.2)) (AxisymmetricFields.partialS K p) p.2.1

theorem NavierStokes.TailGaugePotential.partialS_radialNormalize {K : Point → ℝ} {p : Point} (hK : DifferentiableAt ℝ K p) (hA : DifferentiableAt ℝ K (radialAnchor p)) : AxisymmetricFields.partialS (radialNormalize K) p = AxisymmetricFields.partialS K p

theorem NavierStokes.TailGaugePotential.radialNormalize_anchor (K : Point → ℝ) (t z : ℝ) : radialNormalize K (t, 1, z) = 0

noncomputable def NavierStokes.TailGaugePotential.gaugedSwirl (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : Point → ℝ

This is the entire summed swirl potential, with all slow orders retained.

Equations

• NavierStokes.TailGaugePotential.gaugedSwirl a h C d = NavierStokes.TailGaugePotential.radialNormalize (NavierStokes.SlowBorelBase.swirlPotential a h C d)

theorem NavierStokes.TailGaugePotential.gaugedSwirl_apply (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) (p : Point) : gaugedSwirl a h C d p = SlowBorelBase.swirlPotential a h C d p - SlowBorelBase.swirlPotential a h C d (p.1, 1, p.2.2)

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

Potential, given by AxisymmetricFields.potential (SlowBorelBase.streamFactor a h C d) (gaugedSwirl a h C d).

Equations

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

theorem NavierStokes.TailGaugePotential.potential_eq_sub_gauge (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) (w : ProblemStatement.SpaceTime) : potential a h C d w = BaseResidual.summedPotential a h C d w - SlowBorelBase.swirlPotential a h C d (w.1, 1, w.2.ofLp 2) • ProblemStatement.coordinateVector 2

theorem NavierStokes.TailGaugePotential.gaugedSwirl_smoothAt {a : ℕ → ℕ} (ha : StrictMono a) {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {p : Point} (ht : p.1 < 1) : ContDiffAt ℝ (↑⊤) (gaugedSwirl a h C d) p

theorem NavierStokes.TailGaugePotential.potential_smooth {a : ℕ → ℕ} (ha : StrictMono a) {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) : ContDiffOn ℝ (↑⊤) (potential a h C d) (Set.Iio 1 ×ˢ Set.univ)

theorem NavierStokes.TailGaugePotential.spatialCurl_potential {a : ℕ → ℕ} (ha : StrictMono a) {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : SpatialCurl.spatialCurl (potential a h C d) w = SlowBorelBase.baseVelocity a h C d w

Equality of the actual Euclidean curls, also on the spatial axis.

An actual smooth heat primitive through the terminal time

noncomputable def NavierStokes.TailGaugePotential.extendedHeatCoefficient (C h : ℝ) (p : Point) : ℝ

The heat profile uses its proved smooth extension at negative time remaining; on the past side this is exactly the original heat coefficient.

Equations

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

theorem NavierStokes.TailGaugePotential.extendedHeatCoefficient_eq (C h : ℝ) {p : Point} (ht : p.1 ≤ 1) (hs : 0 < p.2.1) : extendedHeatCoefficient C h p = BaseExterior.heatCoefficient C h p

theorem NavierStokes.TailGaugePotential.extendedHeatCoefficient_smoothAt (C : ℝ) {h : ℝ} (hh : 0 < h) {p : Point} (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (extendedHeatCoefficient C h) p

noncomputable def NavierStokes.TailGaugePotential.shiftedRadialDomain : ProfileHistories.RadialDomain

Translating the radial variable by one makes the anchored integral a standard radial history on a domain stable under contraction to zero.

Equations

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

noncomputable def NavierStokes.TailGaugePotential.shiftedHeat (C h : ℝ) (p : ℝ × ℝ) : ℝ

Shifted heat, given by extendedHeatCoefficient C h (p.2, (p.1 + 1, 0)).

Equations

• NavierStokes.TailGaugePotential.shiftedHeat C h p = NavierStokes.TailGaugePotential.extendedHeatCoefficient C h (p.2, p.1 + 1, 0)

theorem NavierStokes.TailGaugePotential.shiftedHeat_smooth (C : ℝ) {h : ℝ} (hh : 0 < h) : ContDiffOn ℝ (↑⊤) (shiftedHeat C h) shiftedRadialDomain.carrier

noncomputable def NavierStokes.TailGaugePotential.heatPrimitive (C h : ℝ) (p : Point) : ℝ

A finite heat primitive anchored at physical s = 1, for every time. It equals -∫ᵣ₌₁ˢ F(t,r)dr and has no gauge divergence as t → 1.

Equations

• NavierStokes.TailGaugePotential.heatPrimitive C h p = -NavierStokes.ProfileHistories.primitive (NavierStokes.TailGaugePotential.shiftedHeat C h) (p.2.1 - 1, p.1)

theorem NavierStokes.TailGaugePotential.heatPrimitive_anchor (C h t z : ℝ) : heatPrimitive C h (t, 1, z) = 0

theorem NavierStokes.TailGaugePotential.heatPrimitive_eq_integral (C h : ℝ) (p : Point) : heatPrimitive C h p = -∫ (r : ℝ) in 1..p.2.1, extendedHeatCoefficient C h (p.1, r, p.2.2)

theorem NavierStokes.TailGaugePotential.heatPrimitive_smoothAt (C : ℝ) {h : ℝ} (hh : 0 < h) {p : Point} (hs : 0 < p.2.1) : ContDiffAt ℝ (↑⊤) (heatPrimitive C h) p

theorem NavierStokes.TailGaugePotential.heatPrimitive_hasDerivAt (C : ℝ) {h : ℝ} (hh : 0 < h) (t z : ℝ) {s : ℝ} (hs : 0 < s) : HasDerivAt (fun (r : ℝ) => heatPrimitive C h (t, r, z)) (-extendedHeatCoefficient C h (t, s, z)) s

noncomputable def NavierStokes.TailGaugePotential.heatPotential (C h : ℝ) : ProblemStatement.VelocityField

Heat potential, defined pointwise by heatPrimitive C h (AxisymmetricFields.profilePoint w.1 w.2) • coordinateVector 2.

Equations

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

theorem NavierStokes.TailGaugePotential.heatPotential_smoothAt (C : ℝ) {h : ℝ} (hh : 0 < h) {w : ProblemStatement.SpaceTime} (hs : 0 < AxisymmetricFields.radialEnergy w.2) : ContDiffAt ℝ (↑⊤) (heatPotential C h) w

Identifying the complete summed potential in the heat exterior

theorem NavierStokes.TailGaugePotential.gaugedSwirl_eq_heatPrimitive {a : ℕ → ℕ} (ha : StrictMono a) {h C R E : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hext : BaseExterior.ExteriorCoefficients d R) (hheat : Set.EqOn (BaseExterior.leadingAngular h C d) (BaseExterior.heatCoefficient E h) (BaseExterior.exteriorDomain h R)) {p : Point} (ht : p.1 < 1) (hs : 0 < p.2.1) (hseg : ∀ r ∈ Set.uIcc 1 p.2.1, (p.1, r, p.2.2) ∈ BaseExterior.exteriorDomain h R) : gaugedSwirl a h C d p = heatPrimitive E h p

theorem NavierStokes.TailGaugePotential.potential_eq_heatPotential {a : ℕ → ℕ} (ha : StrictMono a) {h C R E : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hext : BaseExterior.ExteriorCoefficients d R) (hheat : Set.EqOn (BaseExterior.leadingAngular h C d) (BaseExterior.heatCoefficient E h) (BaseExterior.exteriorDomain h R)) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) (hs : 0 < AxisymmetricFields.radialEnergy w.2) (hseg : ∀ r ∈ Set.uIcc 1 (AxisymmetricFields.radialEnergy w.2), (w.1, r, w.2.ofLp 2) ∈ BaseExterior.exteriorDomain h R) : potential a h C d w = heatPotential E h w

theorem NavierStokes.TailGaugePotential.exists_terminal_segment_neighborhood {h R : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : ∃ (U : Set ProblemStatement.SpaceTime), IsOpen U ∧ (1, x) ∈ U ∧ (∀ w ∈ U, 0 < AxisymmetricFields.radialEnergy w.2) ∧ ∀ w ∈ U, w.1 < 1 → ∀ r ∈ Set.uIcc 1 (AxisymmetricFields.radialEnergy w.2), (w.1, r, w.2.ofLp 2) ∈ BaseExterior.exteriorDomain h R

A single full spacetime neighborhood places every point of the radial integration segment in the actual heat exterior on the past side.

theorem NavierStokes.TailGaugePotential.central_oneSidedExtension {a : ℕ → ℕ} (ha : StrictMono a) {h C R E : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hext : BaseExterior.ExteriorCoefficients d R) (hheat : Set.EqOn (BaseExterior.leadingAngular h C d) (BaseExterior.heatCoefficient E h) (BaseExterior.exteriorDomain h R)) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : Nonempty (JointResidualLimits.OneSidedExtension (potential a h C d) x)

An explicit smooth ambient extension of the gauge-corrected potential near every nonzero point of the terminal central plane.

theorem NavierStokes.TailGaugePotential.gaugedSwirl_finite_sum {a : ℕ → ℕ} (ha : StrictMono a) {h C : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (d : SlowBorelBase.Coefficients) {p : Point} (ht : p.1 < 1) : ∃ (N : ℕ), gaugedSwirl a h C d p = SimilarityProfile.q h p ^ (1 / 2 - CoordinateAlgebra.A h) * (SlowBorelBase.bundleComponent C d 1 0 (SimilarityProfile.inner h p) - SlowBorelBase.bundleComponent C d 1 0 (SimilarityProfile.inner h (radialAnchor p)) + ∑ j ∈ Finset.range N, SlowBorelBase.coefficientWeight a h (SimilarityProfile.q h p) j * (SlowBorelBase.bundleComponent C d 1 j (SimilarityProfile.inner h p) - SlowBorelBase.bundleComponent C d 1 j (SimilarityProfile.inner h (radialAnchor p))))

At each positive scale, the gauge subtracts the radial constant of every active term in the actual common-cutoff sum.

theorem NavierStokes.TailGaugePotential.realized_central_oneSidedExtension {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) {a : ℕ → ℕ} (ha : StrictMono a) {x : ProblemStatement.Space} (hx : x.ofLp 2 = 0) (hs : 0 < AxisymmetricFields.radialEnergy x) : Nonempty (JointResidualLimits.OneSidedExtension (potential a F.data.h W.axis.normalization d) x)

The primitive hypotheses above are discharged for the actual repaired coefficient scheme with its literal leading profile and exterior support.

All terminal points away from the singular origin

theorem NavierStokes.TailGaugePotential.potential_eq_anchoredPotential (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) : potential a h C d = SlowBaseEndpoint.anchoredPotential a h C d

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

Nonzero axial extension, given by SlowBaseEndpoint.anchoredPotentialNonzeroAxial ha hh hh1 hd C hx.

Equations

• NavierStokes.TailGaugePotential.nonzeroAxialExtension ha hh hh1 hd hx = NavierStokes.SlowBaseEndpoint.anchoredPotentialNonzeroAxial ha hh hh1 hd C hx

theorem NavierStokes.TailGaugePotential.awayExtensions {a : ℕ → ℕ} (ha : StrictMono a) {h C R E : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hR : 0 ≤ R) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (hext : BaseExterior.ExteriorCoefficients d R) (hheat : Set.EqOn (BaseExterior.leadingAngular h C d) (BaseExterior.heatCoefficient E h) (BaseExterior.exteriorDomain h R)) : JointResidualLimits.AwayExtensions (potential a h C d)

theorem NavierStokes.TailGaugePotential.realized_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) {a : ℕ → ℕ} (ha : StrictMono a) : JointResidualLimits.AwayExtensions (potential a F.data.h W.axis.normalization d)

noncomputable def NavierStokes.TailGaugePotential.finalPotential {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

The actual entrance-aligned slow base with its selected cutoff schedule, in the anchored gauge.

Equations

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

theorem NavierStokes.TailGaugePotential.finalPotential_eq_sub_gauge {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (w : ProblemStatement.SpaceTime) : finalPotential H v upper B w = FinalSlowBase.vectorPotential H v upper B w - SlowBorelBase.swirlPotential (FinalSlowBase.scales H v upper B) F.data.h W.axis.normalization (FinalSlowBase.coefficients H v) (w.1, 1, w.2.ofLp 2) • ProblemStatement.coordinateVector 2

theorem NavierStokes.TailGaugePotential.finalPotential_smooth {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (finalPotential H v upper B) BaseResidual.past

theorem NavierStokes.TailGaugePotential.finalPotential_sameCurl {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {w : ProblemStatement.SpaceTime} (ht : w.1 < 1) : SpatialCurl.spatialCurl (finalPotential H v upper B) w = FinalSlowBase.velocity H v upper B w

theorem NavierStokes.TailGaugePotential.finalPotential_awayExtensions {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) : JointResidualLimits.AwayExtensions (finalPotential H v upper B)

noncomputable def NavierStokes.TailGaugePotential.constructedPotential (upper : ℝ) (B : ℕ) : ProblemStatement.VelocityField

A closed choice of the already constructed leading profile, repaired hierarchy, modulation, and common cutoff schedule.

Equations

• NavierStokes.TailGaugePotential.constructedPotential upper B = NavierStokes.TailGaugePotential.finalPotential ⋯ NavierStokes.FinalSlowBase.actualProfile.modulation upper B

theorem NavierStokes.TailGaugePotential.constructedPotential_properties (upper : ℝ) (B : ℕ) : ContDiffOn ℝ (↑⊤) (constructedPotential upper B) BaseResidual.past ∧ JointResidualLimits.AwayExtensions (constructedPotential upper B) ∧ Set.EqOn (SpatialCurl.spatialCurl (constructedPotential upper B)) (FinalSlowBase.velocity ⋯ FinalSlowBase.actualProfile.modulation upper B) BaseResidual.past