Base-field jet bounds on every dyadic band

The positive-order Borel stages vanish when their physical scale is at least one. Their error jets therefore vanish on the open region above one. This extends the normalized bounds to every positive physical scale and removes the auxiliary restriction Q * qhi ≤ 1 from the chart estimates.

@[reducible, inline]

abbrev NavierStokes.AllBandBaseJets.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.AllBandBaseJets.Slow = NavierStokes.PhaseCalculus.Slow

theorem NavierStokes.AllBandBaseJets.slowStage_eq_zero_of_one_le {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : ∀ (j : ℕ), 0 < a j) (h : ℝ) (f : ℕ → BaseChartJets.Inner → V) (j : ℕ) {y : BaseChartJets.Chart} (hy : 1 ≤ y.1) : SlowBorelBase.slowStage a h f j y = 0

Positivity of the integer cutoff scales is enough; no asymptotic band condition is used.

theorem NavierStokes.AllBandBaseJets.slowSum_eq_leading_of_one_le {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : ∀ (j : ℕ), 0 < a j) (h : ℝ) (f : ℕ → BaseChartJets.Inner → V) {y : BaseChartJets.Chart} (hy : 1 ≤ y.1) : SlowBorelBase.slowSum a h f y = f 0 y.2

The literal infinite sum equals its uncut order-zero coefficient above the cutoff.

theorem NavierStokes.AllBandBaseJets.blownJet_eq_zero_of_above_one {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : BaseChartJets.Chart → V} (hf : ∀ (y : BaseChartJets.Chart), 1 < y.1 → f y = 0) {q : ℝ} (hq : 1 < q) (w : BaseChartJets.Inner) (m : ℕ) : SlowBorelBase.blownJet m f (q, w) = 0

A zero germ, rather than only a zero value, kills every actual blown derivative. The lemma does not assume differentiability of the function.

theorem NavierStokes.AllBandBaseJets.correction_blownJet_eq_zero {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} (ha : ∀ (j : ℕ), 0 < a j) (h : ℝ) (f : ℕ → BaseChartJets.Inner → V) {q : ℝ} (hq : 1 < q) (w : BaseChartJets.Inner) (m : ℕ) : SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => SlowBorelBase.slowSum a h f y - f 0 y.2) (q, w) = 0

theorem NavierStokes.AllBandBaseJets.normalized_correction_bound {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a : ℕ → ℕ} {h : ℝ} (hh : 0 < h) {f : ℕ → BaseChartJets.Inner → V} (hf : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (f j)) {K : Set BaseChartJets.Inner} (hK : IsCompact K) (ha : SlowBorelBase.AdmissibleScales h f K a) (m : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℝ), 0 < q → ∀ w ∈ K, ‖SlowBorelBase.blownJet m (fun (y : SlowBorelBase.Chart) => SlowBorelBase.slowSum a h f y - f 0 y.2) (q, w)‖ ≤ C * q ^ (2 * h)

The existing small-scale theorem and the exact cutoff identity cover all positive scales, with the same constant.

theorem NavierStokes.AllBandBaseJets.normalized_tangential_bounds {a : ℕ → ℕ} {h C lo hi : ℝ} (hh : 0 < h) (hlo : 0 < lo) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (m : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∀ (q : ℝ), 0 < q → ∀ w ∈ SlowBorelBase.innerBox lo hi, ‖SlowBorelBase.blownJet m (BaseChartJets.swirlError a h C d) (q, w)‖ ≤ B * q ^ (2 * h) ∧ ‖SlowBorelBase.blownJet m (BaseChartJets.axialError a h d) (q, w)‖ ≤ B * q ^ (2 * h)

Both tangential errors retain their original q^(2*h) bounds at every positive physical scale.

theorem NavierStokes.AllBandBaseJets.normalized_error_envelope {ι : Type u_1} {h qlo qhi lo hi : ℝ} (hh : 0 < h) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) (Q : ι → ℝ) (hQ : ∀ (i : ι), 0 < Q i) (f : BaseChartJets.Chart → ℝ) (hf : ContDiffOn ℝ (↑⊤) f BaseChartJets.sumRegion) (hb : ∀ (j : ℕ), ∃ (B : ℝ), 0 < B ∧ ∀ (q : ℝ), 0 < q → ∀ w ∈ SlowBorelBase.innerBox lo hi, ‖SlowBorelBase.blownJet j f (q, w)‖ ≤ B * q ^ (2 * h)) : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.oneDomain ι (fun (x : ι) => BaseChartJets.innerRegion qlo qhi lo hi) ⋯) (fun (i : ι) (x : BaseChartJets.Chart) => Q i ^ (2 * h)) fun (i : ι) => f ∘ ⇑(SlowBorelBase.scaleMap (Q i))

Pulling back an all-positive-scale estimate needs only fixed upper and lower bounds on the normalized scale, not a band cutoff.

theorem NavierStokes.AllBandBaseJets.actual_error_envelopes {ι : Type u_1} {a : ℕ → ℕ} {h C qlo qhi lo hi : ℝ} (hh : 0 < h) (hqlo : 0 < qlo) (hqhi : 0 < qhi) (hlo : 0 < lo) {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) : (PrimaryPulseBounds.EnvelopeJets (BaseChartJets.oneDomain ι (fun (x : ι) => BaseChartJets.innerRegion qlo qhi lo hi) ⋯) (fun (i : ι) (x : BaseChartJets.Chart) => Q i ^ (2 * h)) fun (i : ι) => BaseChartJets.swirlError a h C d ∘ ⇑(SlowBorelBase.scaleMap (Q i))) ∧ PrimaryPulseBounds.EnvelopeJets (BaseChartJets.oneDomain ι (fun (x : ι) => BaseChartJets.innerRegion qlo qhi lo hi) ⋯) (fun (i : ι) (x : BaseChartJets.Chart) => Q i ^ (2 * h)) fun (i : ι) => BaseChartJets.axialError a h d ∘ ⇑(SlowBorelBase.scaleMap (Q i))

The actual swirl and axial errors on the fixed normalized chart.

theorem NavierStokes.AllBandBaseJets.actual_estimates {ι : 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) : BaseChartJets.Estimates D Q a h C d

The same literal field estimates as BaseChartJets.Estimates, now for every band with 0 < Q ≤ 1.

theorem NavierStokes.AllBandBaseJets.actual_localBase_and_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) (hconvex : ∀ (i : ι), Convex ℝ (D.carrier i)) {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) : (PhaseJetBounds.PolynomialJets D fun (i : ι) => BaseChartJets.frequency a h C d (Q i)) ∧ (PhaseJetBounds.PolynomialJets D fun (i : ι) => BaseChartJets.axial a h d (Q i)) ∧ ∃ (B : ℝ), 1 ≤ B ∧ ∀ (i : ι), PhaseEstimates.LocalBaseBounds (BaseChartJets.frequency a h C d (Q i)) (BaseChartJets.axial a h d (Q i)) (BaseChartJets.leadingFrequency h C d) (BaseChartJets.leadingAxial h d) (D.carrier i) B (Q i ^ h)

All fixed jets and the local first/second derivative base bounds share constants chosen before any band or label.

theorem NavierStokes.AllBandBaseJets.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) : 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 Borel sum has bounded chart jets on every band.

theorem NavierStokes.AllBandBaseJets.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) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) => BaseRadialJets.normalizedStream a h d (Q i)

theorem NavierStokes.AllBandBaseJets.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) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) => BaseRadialJets.reducedRadial a h d (Q i)

theorem NavierStokes.AllBandBaseJets.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) : PrimaryPulseBounds.EnvelopeJets (BaseChartJets.unitScale D) (fun (i : ι) (x : Slow) => Q i ^ h) fun (i : ι) => BaseRadialJets.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.AllBandBaseJets.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) : PhaseJetBounds.PolynomialJets (BaseChartJets.unitScale D) fun (i : ι) (p : Slow) => BaseRadialJets.radial a h C d (Q i) p / Q i ^ h

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

theorem NavierStokes.AllBandBaseJets.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) (N : ℕ) : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (i : ι), ∀ p ∈ D.carrier i, ∀ j ≤ N, ‖iteratedFDeriv ℝ j (BaseRadialJets.radial a h C d (Q i)) p‖ ≤ K * Q i ^ h

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

theorem NavierStokes.AllBandBaseJets.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) (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) => BaseRadialJets.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.AllBandBaseJets.dyadic_actual_bounds {ι : 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) (hconvex : ∀ (i : ι), Convex ℝ (D.carrier i)) {d : SlowBorelBase.Coefficients} (hd : SlowBorelBase.SmoothCoefficients d) (ha : SlowBorelBase.AdmissibleScales h (SlowBorelBase.coefficientBundle C d) (SlowBorelBase.innerBox lo hi) a) (band : ι → ℕ) : (PhaseJetBounds.PolynomialJets D fun (i : ι) => BaseChartJets.frequency a h C d (ChartScales.Q (band i))) ∧ (PhaseJetBounds.PolynomialJets D fun (i : ι) => BaseChartJets.axial a h d (ChartScales.Q (band i))) ∧ ∃ (B : ℝ), 1 ≤ B ∧ ∀ (i : ι), PhaseEstimates.LocalBaseBounds (BaseChartJets.frequency a h C d (ChartScales.Q (band i))) (BaseChartJets.axial a h d (ChartScales.Q (band i))) (BaseChartJets.leadingFrequency h C d) (BaseChartJets.leadingAxial h d) (D.carrier i) B (ChartScales.epsilon h (band i))

Every original dyadic band is covered; the epsilon sequence is unchanged.

theorem NavierStokes.AllBandBaseJets.final_estimates {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) : BaseChartJets.Estimates D Q (FinalSlowBase.scales H v upper B) F.data.h W.axis.normalization (FinalSlowBase.coefficients H v)

The fixed final aligned schedule supplies the all-band tangential estimates without a replacement schedule or a low-band exception.

theorem NavierStokes.AllBandBaseJets.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) : 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.