The reserved mean-rank patch of the actual summed base

The positive-order repair patch precedes the mean patch. The selected global profiles retain their seed values beyond the repair patch; the seeds have already been cut off there. The full summed tangential base therefore has the exact shaped power required by the five-row mean inverse.

@[reducible, inline]

abbrev NavierStokes.BaseRankPatch.Slow : Type

Slow: an abbreviation for PhaseCalculus.Slow.

Equations

• NavierStokes.BaseRankPatch.Slow = NavierStokes.PhaseCalculus.Slow

theorem NavierStokes.BaseRankPatch.positive_before_mean (F : OutgoingProfile.Profile) {XR : ℝ} (hXR : 0 < XR) : ReservedPatches.right F XR ReservedPatches.Slot.positive < ReservedPatches.left F XR ReservedPatches.Slot.mean

theorem NavierStokes.BaseRankPatch.modulation_before_mean {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} : (ModulatedProfileAssembly.repairPatch W).right < ReservedPatches.left F W.controls.radius ReservedPatches.Slot.mean

The finite modulation also ends before the later mean patch.

theorem NavierStokes.BaseRankPatch.nominal_mean_fields {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {p : BaseChartJets.Inner} (hp : p.1 ∈ ReservedPatches.window F W.controls.radius ReservedPatches.Slot.mean) (heta : |p.2| ≤ 1) : W.U p = 0 ∧ W.E p = ReservedPatches.xAmplitude F W.controls.radius p.2 * p.1 ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.BaseRankPatch.modulated_mean_fields {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {p : BaseChartJets.Inner} (hp : p.1 ∈ ReservedPatches.window F W.controls.radius ReservedPatches.Slot.mean) (heta : |p.2| ≤ 1) : v.profiles.U p = 0 ∧ v.profiles.E p = ReservedPatches.xAmplitude F W.controls.radius p.2 * p.1 ^ (-(1 / 2 + F.data.core.lam))

theorem NavierStokes.BaseRankPatch.modulated_radial_mean_fields {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {R eta : ℝ} (hR : R ∈ ReservedPatches.radialWindow F W.controls.radius ReservedPatches.Slot.mean) (heta : |eta| ≤ 1) : v.profiles.U (R ^ 2 / 2, eta) = 0 ∧ v.profiles.E (R ^ 2 / 2, eta) = FiveRowRank.background F.data.core.lam (ReservedPatches.radialAmplitude F W.controls.radius eta) R

theorem NavierStokes.BaseRankPatch.slowSum_eq_leading {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] (a : ℕ → ℕ) (h : ℝ) (f : ℕ → BaseChartJets.Inner → V) (y : BaseChartJets.Chart) (hf : ∀ (n : ℕ), 0 < n → f n y.2 = 0) : SlowBorelBase.slowSum a h f y = f 0 y.2

Pointwise vanishing of every positive coefficient eliminates the entire actual infinite sum, for any cutoff schedule and any scale.

noncomputable def NavierStokes.BaseRankPatch.rankScale (h : ℝ) (s : ℝ × ℝ) : ℝ

The slow variables here have the physical rank convention (T,Z).

Equations

• NavierStokes.BaseRankPatch.rankScale h s = NavierStokes.SimilarityCoordinates.coordinateQ (2 * h) s

noncomputable def NavierStokes.BaseRankPatch.rankEta (h : ℝ) (s : ℝ × ℝ) : ℝ

Rank eta, given by SimilarityCoordinates.coordinateEta (2 * h) s.

Equations

• NavierStokes.BaseRankPatch.rankEta h s = NavierStokes.SimilarityCoordinates.coordinateEta (2 * h) s

noncomputable def NavierStokes.BaseRankPatch.rankCoefficient (F : OutgoingProfile.Profile) (XR : ℝ) (s : ℝ × ℝ) : ℝ

Rank coefficient, given by MeanRankUpdate.shapedAmplitude (ReservedPatches.radialAmplitude F XR 0) (rankEta F.data.h s).

Equations

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

noncomputable def NavierStokes.BaseRankPatch.rankLength (h : ℝ) (s : ℝ × ℝ) : ℝ

Rank length, given by Real.sqrt (rankScale h s).

Equations

• NavierStokes.BaseRankPatch.rankLength h s = √(NavierStokes.BaseRankPatch.rankScale h s)

noncomputable def NavierStokes.BaseRankPatch.rankVelocity (h : ℝ) (s : ℝ × ℝ) : ℝ

Rank velocity, given by rankScale h s ^ (-CoordinateAlgebra.A h).

Equations

• NavierStokes.BaseRankPatch.rankVelocity h s = NavierStokes.BaseRankPatch.rankScale h s ^ (-NavierStokes.CoordinateAlgebra.A h)

theorem NavierStokes.BaseRankPatch.rankLength_eq_qLength (h : ℝ) : rankLength h = VariableGaugeMean.qLength (2 * h)

theorem NavierStokes.BaseRankPatch.rankScale_eq_chartQ (h R : ℝ) (s Y : ℝ × ℝ) : rankScale h s = MeanRankUpdate.chartQ (2 * h) (R, s, Y)

theorem NavierStokes.BaseRankPatch.rankEta_eq_chartEta (h R : ℝ) (s Y : ℝ × ℝ) : rankEta h s = MeanRankUpdate.chartEta (2 * h) (R, s, Y)

theorem NavierStokes.BaseRankPatch.coordinates_rankScale (h R : ℝ) (s : ℝ × ℝ) : (BaseChartJets.normalizedCoordinates h (R, s.2, s.1)).1 = rankScale h s

theorem NavierStokes.BaseRankPatch.coordinates_rankEta (h R : ℝ) (s : ℝ × ℝ) : (BaseChartJets.normalizedCoordinates h (R, s.2, s.1)).2.2 = rankEta h s

theorem NavierStokes.BaseRankPatch.rankScale_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {s : ℝ × ℝ} (hs : 0 < s.1) : 0 < rankScale h s

theorem NavierStokes.BaseRankPatch.rankLength_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {s : ℝ × ℝ} (hs : 0 < s.1) : 0 < rankLength h s

theorem NavierStokes.BaseRankPatch.rankVelocity_pos {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {s : ℝ × ℝ} (hs : 0 < s.1) : 0 < rankVelocity h s

theorem NavierStokes.BaseRankPatch.rankCoefficient_pos (F : OutgoingProfile.Profile) (XR : ℝ) (s : ℝ × ℝ) : 0 < rankCoefficient F XR s

theorem NavierStokes.BaseRankPatch.rank_parameters_smooth (F : OutgoingProfile.Profile) (XR : ℝ) : ContDiffOn ℝ (↑⊤) (rankCoefficient F XR) {s : ℝ × ℝ | 0 < s.1} ∧ ContDiffOn ℝ (↑⊤) (rankLength F.data.h) {s : ℝ × ℝ | 0 < s.1} ∧ ContDiffOn ℝ (↑⊤) (rankVelocity F.data.h) {s : ℝ × ℝ | 0 < s.1}

theorem NavierStokes.BaseRankPatch.coordinates_radius_sq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {s : ℝ × ℝ} (hs : 0 < s.1) (R : ℝ) : (R / rankLength h s) ^ 2 / 2 = (BaseChartJets.normalizedCoordinates h (R, s.2, s.1)).2.1

theorem NavierStokes.BaseRankPatch.positive_fields_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) {n : ℕ} (hn : 0 < n) {p : BaseChartJets.Inner} (hp : ReservedPatches.right F W.controls.radius ReservedPatches.Slot.positive ≤ p.1) (heta : |p.2| ≤ 1) : (FinalSlowBase.coefficients H v).phi n p = 0 ∧ (FinalSlowBase.coefficients H v).axial n p = 0

Every positive angular and axial coefficient vanishes past the actual positive-order repair patch. The selected witness retains this support.

theorem NavierStokes.BaseRankPatch.normalized_mean_fields {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (a : ℕ → ℕ) (q : ℝ) {p : BaseChartJets.Inner} (hp : p.1 ∈ ReservedPatches.window F W.controls.radius ReservedPatches.Slot.mean) (heta : |p.2| ≤ 1) : SlowBorelBase.normalizedSwirl a F.data.h W.axis.normalization (FinalSlowBase.coefficients H v) (q, p) = ReservedPatches.xAmplitude F W.controls.radius p.2 * p.1 ^ (-(1 / 2 + F.data.core.lam)) ∧ SlowBorelBase.slowSum a F.data.h (FinalSlowBase.coefficients H v).axial (q, p) = 0

The complete summed tangential fields on the mean patch, for every cutoff schedule and expansion scale.

noncomputable def NavierStokes.BaseRankPatch.angularSlice {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (s : ℝ × ℝ) (R : ℝ) : ℝ

The literal normalized angular and axial slices of the final base.

Equations

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

noncomputable def NavierStokes.BaseRankPatch.axialSlice {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) (s : ℝ × ℝ) (R : ℝ) : ℝ

Axial slice, given by axial (FinalSlowBase.scales H v upper B) F.data.h (FinalSlowBase.coefficients H v) Q (R, (s.2, s.1)).

Equations

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

theorem NavierStokes.BaseRankPatch.angularSlice_physical {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) {s : ℝ × ℝ} (hs : 0 < s.1) {R : ℝ} (hR : 0 < R) : angularSlice H v upper B Q s R = Q ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseChartJets.bandPoint F.data.h Q (R, s.2, s.1))).ofLp 1

theorem NavierStokes.BaseRankPatch.axialSlice_physical {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) {s : ℝ × ℝ} (hs : 0 < s.1) (R : ℝ) : axialSlice H v upper B Q s R = Q ^ CoordinateAlgebra.A F.data.h * (FinalSlowBase.velocity H v upper B (BaseChartJets.bandPoint F.data.h Q (R, s.2, s.1))).ofLp 2

theorem NavierStokes.BaseRankPatch.rank_fields {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) {s : ℝ × ℝ} (hs : 0 < s.1) {R : ℝ} (hR : R ∈ Set.Ioo (rankLength F.data.h s * ReservedPatches.radialSupportLeft F W.controls.radius ReservedPatches.Slot.mean) (rankLength F.data.h s * ReservedPatches.radialSupportRight F W.controls.radius ReservedPatches.Slot.mean)) : angularSlice H v upper B Q s R = MeanRankUpdate.background F.data.core.lam (rankCoefficient F W.controls.radius s) (rankLength F.data.h s) (rankVelocity F.data.h s) R ∧ axialSlice H v upper B Q s R = 0

The actual background identities required by the local rank inverse. All scales and amplitudes are fixed by the original profile.

theorem NavierStokes.BaseRankPatch.five_rows {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (B : ℕ) (Q : ℝ) {s : ℝ × ℝ} (hs : 0 < s.1) (debt : MeanRankUpdate.Debt) : FiveRowRank.FiveRows (angularSlice H v upper B Q s) (axialSlice H v upper B Q s) debt (MeanRankUpdate.angularIncrement F.data.core.lam (rankCoefficient F W.controls.radius s) (ReservedPatches.radialSupportLeft F W.controls.radius ReservedPatches.Slot.mean) (ReservedPatches.radialSupportRight F W.controls.radius ReservedPatches.Slot.mean) (rankLength F.data.h s) (rankVelocity F.data.h s) debt) (MeanRankUpdate.desiredAxialIncrement F.data.core.lam (rankCoefficient F W.controls.radius s) (ReservedPatches.radialSupportLeft F W.controls.radius ReservedPatches.Slot.mean) (ReservedPatches.radialSupportRight F W.controls.radius ReservedPatches.Slot.mean) (rankLength F.data.h s) (rankVelocity F.data.h s) debt)

Five exact physical rows for the full final base, with the original mean-patch radii and the actual similarity length and velocity scales.