The actual normalized radial base component

The radial coefficient is obtained from the same summed curl base and the same admissible schedule as the angular and axial coefficients. Its small factor is Q^h. The exact stream formula includes the factor 1/2 in AxisymmetricFields.velocity_zero.

@[reducible, inline]

abbrev NavierStokes.BaseRadialJets.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.BaseRadialJets.Slow = NavierStokes.PhaseCalculus.Slow

noncomputable def NavierStokes.BaseRadialJets.averageSequence (d : SlowBorelBase.Coefficients) : ℕ → BaseChartJets.Inner → ℝ

Average sequence, defined pointwise by ProfileHistories.average (d.axial j).

Equations

• NavierStokes.BaseRadialJets.averageSequence d j = NavierStokes.ProfileHistories.average (d.axial j)

theorem NavierStokes.BaseRadialJets.averageSequence_eq_component (C : ℝ) (d : SlowBorelBase.Coefficients) : averageSequence d = SlowBorelBase.bundleComponent C d 0

theorem NavierStokes.BaseRadialJets.averageSequence_smooth {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (j : ℕ) : ContDiff ℝ (↑⊤) (averageSequence d j)

theorem NavierStokes.BaseRadialJets.averageSequence_admissible {a : ℕ → ℕ} {h C : ℝ} {d : SlowBorelBase.Coefficients} {K : Set BaseChartJets.Inner} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) K a) : SlowBorelBase.AdmissibleScales h (averageSequence d) K a

noncomputable def NavierStokes.BaseRadialJets.bandInput (h Q : ℝ) (p : Slow) : BaseChartJets.Chart

Band input, given by (1 - Q * p.2.2, (Q * p.1 ^ 2 / 2, Q ^ CoordinateAlgebra.D h * p.2.1)).

Equations

• NavierStokes.BaseRadialJets.bandInput h Q p = (1 - Q * p.2.2, Q * p.1 ^ 2 / 2, Q ^ NavierStokes.CoordinateAlgebra.D h * p.2.1)

theorem NavierStokes.BaseRadialJets.bandInput_eq (h Q : ℝ) (p : Slow) : bandInput h Q p = SimilarityHomogeneity.physicalScale h Q (BaseChartJets.physicalInput p)

theorem NavierStokes.BaseRadialJets.bandInput_smooth (h Q : ℝ) : ContDiff ℝ (↑⊤) (bandInput h Q)

theorem NavierStokes.BaseRadialJets.bandInput_deriv_Z (h Q : ℝ) (p : Slow) : (fderiv ℝ (bandInput h Q) p) (0, 1, 0) = (0, 0, Q ^ CoordinateAlgebra.D h)

noncomputable def NavierStokes.BaseRadialJets.normalizedStream (a : ℕ → ℕ) (h : ℝ) (d : SlowBorelBase.Coefficients) (Q : ℝ) (p : Slow) : ℝ

Full normalized average stream; no new coefficient sequence or cutoff schedule is chosen.

Equations

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

theorem NavierStokes.BaseRadialJets.normalizedStream_eq {a : ℕ → ℕ} {h C Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) (d : SlowBorelBase.Coefficients) {p : Slow} (hT : 0 < p.2.2) : normalizedStream a h d Q p = Q ^ CoordinateAlgebra.A h * SlowBorelBase.streamFactor a h C d (bandInput h Q p)

theorem NavierStokes.BaseRadialJets.normalizedStream_smoothAt {a : ℕ → ℕ} (ha : StrictMono a) {h Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {p : Slow} (hT : 0 < p.2.2) : ContDiffAt ℝ (↑⊤) (normalizedStream a h d Q) p

theorem NavierStokes.BaseRadialJets.normalizedStream_deriv_Z {a : ℕ → ℕ} (ha : StrictMono a) {h C Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {p : Slow} (hT : 0 < p.2.2) : PhaseCalculus.slowZ (normalizedStream a h d Q) p = Q ^ CoordinateAlgebra.A h * Q ^ CoordinateAlgebra.D h * AxisymmetricFields.partialZ (SlowBorelBase.streamFactor a h C d) (bandInput h Q p)

Chain rule for the actual physical axial coordinate.

noncomputable def NavierStokes.BaseRadialJets.reducedRadial (a : ℕ → ℕ) (h : ℝ) (d : SlowBorelBase.Coefficients) (Q : ℝ) (p : Slow) : ℝ

Reduced radial, given by -(p.1 / 2) * PhaseCalculus.slowZ (normalizedStream a h d Q) p.

Equations

• NavierStokes.BaseRadialJets.reducedRadial a h d Q p = -(p.1 / 2) * NavierStokes.PhaseCalculus.slowZ (NavierStokes.BaseRadialJets.normalizedStream a h d Q) p

noncomputable def NavierStokes.BaseRadialJets.radial (a : ℕ → ℕ) (h C : ℝ) (d : SlowBorelBase.Coefficients) (Q : ℝ) (p : Slow) : ℝ

Literal normalized radial component of the constructed curl base.

Equations

• NavierStokes.BaseRadialJets.radial a h C d Q p = Q ^ NavierStokes.CoordinateAlgebra.A h * (NavierStokes.SlowBorelBase.baseVelocity a h C d (NavierStokes.BaseChartJets.bandPoint h Q p)).ofLp 0

theorem NavierStokes.BaseRadialJets.radial_eq {a : ℕ → ℕ} (ha : StrictMono a) {h C Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {p : Slow} (hT : 0 < p.2.2) : radial a h C d Q p = Q ^ h * reducedRadial a h d Q p

theorem NavierStokes.BaseRadialJets.radial_eq_stream {a : ℕ → ℕ} (ha : StrictMono a) {h C Q : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hQ : 0 < Q) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) {p : Slow} (hT : 0 < p.2.2) : radial a h C d Q p = -(Q ^ h * p.1 / 2) * PhaseCalculus.slowZ (normalizedStream a h d Q) p

Expanded formula, including the exact one-half factor.

theorem NavierStokes.BaseRadialJets.scaled_sum_polynomial {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {a : ℕ → ℕ} {h r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {f : ℕ → BaseChartJets.Inner → ℝ} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) (ha : SlowBorelBase.AdmissibleScales h f (SlowBorelBase.innerBox lo hi) a) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) (p : Slow) => SlowBorelBase.slowSum a h f ((SlowBorelBase.scaleMap (Q i)) (BaseChartJets.normalizedCoordinates h p))

The same scalar component schedule controls the actual normalized sum. The result is uniform in every band/label index of D.

theorem NavierStokes.BaseRadialJets.normalizedStream_polynomial {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {a : ℕ → ℕ} {h C r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) => normalizedStream a h d (Q i)

theorem NavierStokes.BaseRadialJets.reducedRadial_polynomial {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {a : ℕ → ℕ} {h C r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) => reducedRadial a h d (Q i)

theorem NavierStokes.BaseRadialJets.scalar_envelope {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (D : PhaseJetBounds.Domain ι E) (w : ι → ℝ) (hw : ∀ (i : ι), 0 ≤ w i) : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.unitScale D) (fun (i : ι) (x : E) => w i) fun (i : ι) (x : E) => w i

A band-only nonnegative factor is an exact envelope and has no slow derivatives. This does not divide by any vanishing spatial weight.

theorem NavierStokes.BaseRadialJets.radial_envelope {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {a : ℕ → ℕ} {h C r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.unitScale D) (fun (i : ι) (x : Slow) => Q i ^ h) fun (i : ι) => radial a h C d (Q i)

The actual physical radial coefficient has an all-order Q^h envelope, uniformly before the band and label are selected.

theorem NavierStokes.BaseRadialJets.radial_quotient_polynomial {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {a : ℕ → ℕ} {h C r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) (p : Slow) => radial a h C d (Q i) p / Q i ^ h

All actual derivatives of b/Q^h are uniformly bounded.

theorem NavierStokes.BaseRadialJets.radial_uniform_jets {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} {a : ℕ → ℕ} {h C r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) (N : ℕ) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ j ≤ N, ‖iteratedFDeriv ℝ j (radial a h C d (Q i)) p‖ ≤ K * Q i ^ h

A direct finite-jet statement for the actual physical component.

theorem NavierStokes.BaseRadialJets.radial_uniform_pullback {ι : Type u_1} {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : WeightedClasses.StripData E) (L : E →L[ℝ] Slow) {D : PhaseJetBounds.Domain (ℕ × ι) Slow} {a : ℕ → ℕ} {h C r M qlo qhi lo hi : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (H : BaseChartJets.GeometryBounds D h r M qlo qhi lo hi) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (Q : ℕ × ι → ℝ) (hQ : ∀ (i : ℕ × ι), 0 < Q i) (hQ1 : ∀ (i : ℕ × ι), Q i ≤ 1) (hsmall : ∀ (i : ℕ × ι), Q i * qhi ≤ 1) (heps : ∀ (n : ℕ) (l : ι), Q (n, l) ^ h = s.epsilon n) (hmap : ∀ (n : ℕ) (l : ι), Set.MapsTo (⇑L) s.domain (D.carrier (n, l))) : LabelSumBounds.UniformClass s (fun (x : ι) (x_1 : ℕ) (x_2 : E) => 1) 1 fun (l : ι) (n : ℕ) (x : E) => radial a h C d (Q (n, l)) (L x)

Fixed linear native/common coordinate changes preserve the genuine order-one class. Only the original small factor is used as a weight; there is no vanishing spatial zeta factor in this conclusion.

theorem NavierStokes.BaseRadialJets.final_radial_eq {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) {Q : ℝ} (hQ : 0 < Q) {p : Slow} (hT : 0 < p.2.2) : Q ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseChartJets.bandPoint F.data.h Q p)).ofLp 0 = -(Q ^ F.data.h * p.1 / 2) * PhaseCalculus.slowZ (normalizedStream (FinalSlowBase.scales H v upper B) F.data.h (FinalSlowBase.coefficients H v) Q) p

The corrected one-half identity for the same final aligned base.

theorem NavierStokes.BaseRadialJets.final_radial_envelope {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {ι : Type u_1} {D : PhaseJetBounds.Domain ι Slow} (upper : ℝ) (B : ℕ) {r M qlo qhi lo hi : ℝ} (hr : 0 < r) (hM : 1 ≤ M) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (hhi : hi ≤ FinalSlowBase.boxRadius W upper) (hgeom : BaseChartJets.GeometryBounds D F.data.h r M qlo qhi lo hi) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (hQ1 : ∀ (i : ι), Q i ≤ 1) (hsmall : ∀ (i : ι), Q i * qhi ≤ 1) : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.unitScale D) (fun (i : ι) (x : Slow) => Q i ^ F.data.h) fun (i : ι) (p : Slow) => Q i ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseChartJets.bandPoint F.data.h (Q i) p)).ofLp 0

The very same final weighted-bundle schedule supplies the averaged axial estimates. No replacement scale choice is introduced.