Primitive correction formulas at a nonzero axial endpoint

The positive stable branch of the similarity coordinate continues across T = 0 when Z ≠ 0. This file uses that branch in the actual moving-radius mean operations. Agreement of primitive data is on whole slow fibers, because radial and torus integrals are nonlocal on each such fiber.

@[reducible, inline]

abbrev NavierStokes.OffplaneCorrectionExtensions.Slow : Type

Slow: an abbreviation for PressureStream.Plane.

Equations

• NavierStokes.OffplaneCorrectionExtensions.Slow = NavierStokes.PressureStream.Plane

@[reducible, inline]

abbrev NavierStokes.OffplaneCorrectionExtensions.Lift : Type

Lift: an abbreviation for PressureStream.Lift Slow.

Equations

• NavierStokes.OffplaneCorrectionExtensions.Lift = NavierStokes.PressureStream.Lift NavierStokes.OffplaneCorrectionExtensions.Slow

@[reducible, inline]

abbrev NavierStokes.OffplaneCorrectionExtensions.Model : Type

Model: an abbreviation for MeanRankUpdate.ModelPoint × PressureStream.Plane.

Equations

• NavierStokes.OffplaneCorrectionExtensions.Model = (NavierStokes.MeanRankUpdate.ModelPoint × NavierStokes.PressureStream.Plane)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.stableQ (coord : ℝ) (s : Slow) : ℝ

Stable Q, given by (PositiveRepresentatives.stableInverse coord s).1.

Equations

• NavierStokes.OffplaneCorrectionExtensions.stableQ coord s = (NavierStokes.PositiveRepresentatives.stableInverse coord s).1

noncomputable def NavierStokes.OffplaneCorrectionExtensions.stableLength (coord : ℝ) (s : Slow) : ℝ

Stable length, given by Real.sqrt (stableQ coord s).

Equations

• NavierStokes.OffplaneCorrectionExtensions.stableLength coord s = √(NavierStokes.OffplaneCorrectionExtensions.stableQ coord s)

theorem NavierStokes.OffplaneCorrectionExtensions.stableQ_pos {coord : ℝ} {s : Slow} (hs : s ∈ PositiveRepresentatives.stableTarget coord) : 0 < stableQ coord s

theorem NavierStokes.OffplaneCorrectionExtensions.stableQ_contDiffAt {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {s : Slow} (hs : s ∈ PositiveRepresentatives.stableTarget coord) : ContDiffAt ℝ (↑⊤) (stableQ coord) s

theorem NavierStokes.OffplaneCorrectionExtensions.stableLength_pos {coord : ℝ} {s : Slow} (hs : s ∈ PositiveRepresentatives.stableTarget coord) : 0 < stableLength coord s

theorem NavierStokes.OffplaneCorrectionExtensions.stableLength_contDiffAt {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {s : Slow} (hs : s ∈ PositiveRepresentatives.stableTarget coord) : ContDiffAt ℝ (↑⊤) (stableLength coord) s

theorem NavierStokes.OffplaneCorrectionExtensions.stableLength_contDiffOn {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) : ContDiffOn ℝ (↑⊤) (stableLength coord) (PositiveRepresentatives.stableTarget coord)

theorem NavierStokes.OffplaneCorrectionExtensions.stableQ_eq_coordinateQ {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {s : Slow} (hs : 0 < s.1) : stableQ coord s = SimilarityCoordinates.coordinateQ coord s

theorem NavierStokes.OffplaneCorrectionExtensions.stableLength_eq_qLength {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {s : Slow} (hs : 0 < s.1) : stableLength coord s = VariableGaugeMean.qLength coord s

structure NavierStokes.OffplaneCorrectionExtensions.Window (coord a b : ℝ) : Type

A neighborhood on which the moving radial interval has fixed positive inner and finite outer bounds. These bounds are constructed from the actual stable branch below.

• carrier : Set Slow

  Carrier of Window, of type Set Slow.

• isOpen : IsOpen self.carrier
• stable : self.carrier ⊆ PositiveRepresentatives.stableTarget coord
• lower : ℝ

  Lower of Window, of type ℝ.

• upper : ℝ

  Upper of Window, of type ℝ.

• lower_pos : 0 < self.lower
• lower_lt_upper : self.lower < self.upper
• left (s : Slow) : s ∈ self.carrier → self.lower ≤ stableLength coord s * a
• right (s : Slow) : s ∈ self.carrier → stableLength coord s * b ≤ self.upper

theorem NavierStokes.OffplaneCorrectionExtensions.exists_window_at {coord a b : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) {s₀ : Slow} (hs : s₀ ∈ PositiveRepresentatives.stableTarget coord) : ∃ (W : Window coord a b), s₀ ∈ W.carrier

theorem NavierStokes.OffplaneCorrectionExtensions.exists_endpoint_window {coord a b Z : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) (hZ : Z ≠ 0) : ∃ (W : Window coord a b), (0, Z) ∈ W.carrier

theorem NavierStokes.OffplaneCorrectionExtensions.Window.length_pos {coord a b : ℝ} (W : Window coord a b) {s : Slow} (hs : s ∈ W.carrier) : 0 < stableLength coord s

theorem NavierStokes.OffplaneCorrectionExtensions.Window.length_smooth {coord a b : ℝ} (W : Window coord a b) (hc : 0 < coord) (hc1 : coord < 1) : ContDiffOn ℝ (↑⊤) (stableLength coord) W.carrier

theorem NavierStokes.OffplaneCorrectionExtensions.Window.fixed_support {coord a b : ℝ} (W : Window coord a b) {f : Lift → ℝ} (hf : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier f) : PhysicalMeanDomain.SupportedOn W.lower W.upper W.carrier f

noncomputable def NavierStokes.OffplaneCorrectionExtensions.positiveSlow : Set Slow

Positive time is restricted only in the agreement assertion. The continued formulas themselves are defined on the full stable neighborhood.

Equations

• NavierStokes.OffplaneCorrectionExtensions.positiveSlow = {s : NavierStokes.OffplaneCorrectionExtensions.Slow | 0 < s.1}

theorem NavierStokes.OffplaneCorrectionExtensions.positiveSlow_open : IsOpen positiveSlow

def NavierStokes.OffplaneCorrectionExtensions.FiberAgreement {V : Type u_1} (U : Set Slow) (F f : Lift → V) : Prop

Fiber agreement, given by EqOn F f (PhysicalMeanDomain.slowDomain (U ∩ positiveSlow)).

Equations

• NavierStokes.OffplaneCorrectionExtensions.FiberAgreement U F f = Set.EqOn F f (NavierStokes.PhysicalMeanDomain.slowDomain (U ∩ NavierStokes.OffplaneCorrectionExtensions.positiveSlow))

theorem NavierStokes.OffplaneCorrectionExtensions.FiberAgreement.fiber {V : Type u_1} {U : Set Slow} {F f : Lift → V} (h : FiberAgreement U F f) {s : Slow} (hs : s ∈ U) (ht : 0 < s.1) (r : ℝ) (Y : PressureStream.Plane) : F (r, s, Y) = f (r, s, Y)

theorem NavierStokes.OffplaneCorrectionExtensions.FiberAgreement.eventuallyEq {V : Type u_1} {U : Set Slow} (hU : IsOpen U) {F f : Lift → V} (h : FiberAgreement U F f) {p : Lift} (hp : p.2.1 ∈ U) (ht : 0 < p.2.1.1) : F =ᶠ[nhds p] f

noncomputable def NavierStokes.OffplaneCorrectionExtensions.stableModel (coord : ℝ) (p : Lift) : Model

A primitive model retains the fast torus coordinate and the physical radial variable; only the time coordinate is replaced by q.

Equations

• NavierStokes.OffplaneCorrectionExtensions.stableModel coord p = ((NavierStokes.OffplaneCorrectionExtensions.stableQ coord p.2.1, p.1, p.2.1.2), p.2.2)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalModel (coord : ℝ) (p : Lift) : Model

Physical model, given by ((SimilarityCoordinates.coordinateQ coord p.2.1, (p.1, p.2.1.2)), p.2.2).

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalModel coord p = ((NavierStokes.SimilarityCoordinates.coordinateQ coord p.2.1, p.1, p.2.1.2), p.2.2)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.modelDomain : Set Model

Model domain, given by {y | 0 < y.1.1}.

Equations

• NavierStokes.OffplaneCorrectionExtensions.modelDomain = {y : NavierStokes.OffplaneCorrectionExtensions.Model | 0 < y.1.1}

theorem NavierStokes.OffplaneCorrectionExtensions.modelDomain_open : IsOpen modelDomain

theorem NavierStokes.OffplaneCorrectionExtensions.stableModel_contDiffOn {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) : ContDiffOn ℝ (↑⊤) (stableModel coord) (PhysicalMeanDomain.slowDomain (PositiveRepresentatives.stableTarget coord))

theorem NavierStokes.OffplaneCorrectionExtensions.stableModel_mem {coord : ℝ} {p : Lift} (hp : p.2.1 ∈ PositiveRepresentatives.stableTarget coord) : stableModel coord p ∈ modelDomain

noncomputable def NavierStokes.OffplaneCorrectionExtensions.continuedSource (coord : ℝ) (F : Model → ℝ) : Lift → ℝ

Continued source, given by F ∘ stableModel coord.

Equations

• NavierStokes.OffplaneCorrectionExtensions.continuedSource coord F = F ∘ NavierStokes.OffplaneCorrectionExtensions.stableModel coord

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalSource (coord : ℝ) (F : Model → ℝ) : Lift → ℝ

Physical source, given by F ∘ physicalModel coord.

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalSource coord F = F ∘ NavierStokes.OffplaneCorrectionExtensions.physicalModel coord

theorem NavierStokes.OffplaneCorrectionExtensions.continuedSource_smooth {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {F : Model → ℝ} (hF : ContDiffOn ℝ (↑⊤) F modelDomain) : ContDiffOn ℝ (↑⊤) (continuedSource coord F) (PhysicalMeanDomain.slowDomain (PositiveRepresentatives.stableTarget coord))

theorem NavierStokes.OffplaneCorrectionExtensions.continuedSource_agreement {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (F : Model → ℝ) (U : Set Slow) : FiberAgreement U (continuedSource coord F) (physicalSource coord F)

def NavierStokes.OffplaneCorrectionExtensions.ModelSupported {V : Type u_1} [Zero V] (a b : ℝ) (F : Model → V) : Prop

A support condition on the explicit primitive model, before any mean operation is performed.

Equations

• NavierStokes.OffplaneCorrectionExtensions.ModelSupported a b F = ∀ y ∈ NavierStokes.OffplaneCorrectionExtensions.modelDomain, F y ≠ 0 → y.1.2.1 ∈ Set.Icc (√y.1.1 * a) (√y.1.1 * b)

def NavierStokes.OffplaneCorrectionExtensions.ModelPeriodic (F : Model → ℝ) : Prop

Model periodic, given by ∀ y : MeanRankUpdate.ModelPoint, 0 < y.1 → FourierAlias.TorusPeriodic (fun Y => F (y, Y)).

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.continuedSource_periodic {coord : ℝ} {F : Model → ℝ} (hF : ModelPeriodic F) {U : Set Slow} (hU : U ⊆ PositiveRepresentatives.stableTarget coord) : PhysicalMeanDomain.PeriodicOn U (continuedSource coord F)

theorem NavierStokes.OffplaneCorrectionExtensions.continuedSource_supported {coord a b : ℝ} {F : Model → ℝ} (hF : ModelSupported a b F) {U : Set Slow} (hU : U ⊆ PositiveRepresentatives.stableTarget coord) : VariableGaugeMean.SupportedGauge a b (stableLength coord) U (continuedSource coord F)

theorem NavierStokes.OffplaneCorrectionExtensions.Window.compactPrimitive_smooth {coord a b : ℝ} (W : Window coord a b) (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain W.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier f) : ContDiffOn ℝ (↑⊤) (VariableGaugeMean.compactPrimitive d a b M (stableLength coord) v f) (PhysicalMeanDomain.slowDomain W.carrier)

theorem NavierStokes.OffplaneCorrectionExtensions.Window.pressureSource_smooth {coord a b : ℝ} (W : Window coord a b) (hc : 0 < coord) (hc1 : coord < 1) (hab : a < b) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain W.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier f) : ContDiffOn ℝ (↑⊤) (VariableGaugeMean.pressureSource a b hab (stableLength coord) f) (PhysicalMeanDomain.slowDomain W.carrier)

theorem NavierStokes.OffplaneCorrectionExtensions.Window.meanPressure_smooth {coord a b : ℝ} (W : Window coord a b) (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain W.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier f) : ContDiffOn ℝ (↑⊤) (VariableGaugeMean.meanPressure d a b M hab (stableLength coord) v f) (PhysicalMeanDomain.slowDomain W.carrier)

theorem NavierStokes.OffplaneCorrectionExtensions.Window.streamPotential_smooth {coord a b : ℝ} (W : Window coord a b) (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain W.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier f) : ContDiffOn ℝ (↑⊤) (VariableGaugeMean.streamPotential d a b M (stableLength coord) v f) (PhysicalMeanDomain.slowDomain W.carrier)

theorem NavierStokes.OffplaneCorrectionExtensions.Window.compactAlias_smooth {coord a b : ℝ} (W : Window coord a b) (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain W.carrier)) (hs : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier f) : ContDiffOn ℝ (↑⊤) (VariableGaugeMean.compactAlias d a b M (stableLength coord) v f) (PhysicalMeanDomain.slowDomain W.carrier)

theorem NavierStokes.OffplaneCorrectionExtensions.compactPrimitive_agreement {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {U : Set Slow} {F f : Lift → ℝ} (he : FiberAgreement U F f) (d a b M : ℝ) (v : Slow) : FiberAgreement U (VariableGaugeMean.compactPrimitive d a b M (stableLength coord) v F) (VariableGaugeMean.compactPrimitive d a b M (VariableGaugeMean.qLength coord) v f)

theorem NavierStokes.OffplaneCorrectionExtensions.pressureSource_agreement {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {U : Set Slow} {F f : Lift → ℝ} (he : FiberAgreement U F f) (a b : ℝ) (hab : a < b) : FiberAgreement U (VariableGaugeMean.pressureSource a b hab (stableLength coord) F) (VariableGaugeMean.pressureSource a b hab (VariableGaugeMean.qLength coord) f)

theorem NavierStokes.OffplaneCorrectionExtensions.meanPressure_agreement {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {U : Set Slow} {F f : Lift → ℝ} (he : FiberAgreement U F f) (d a b M : ℝ) (hab : a < b) (v : Slow) : FiberAgreement U (VariableGaugeMean.meanPressure d a b M hab (stableLength coord) v F) (VariableGaugeMean.meanPressure d a b M hab (VariableGaugeMean.qLength coord) v f)

theorem NavierStokes.OffplaneCorrectionExtensions.streamPotential_agreement {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {U : Set Slow} {F f : Lift → ℝ} (he : FiberAgreement U F f) (d a b M : ℝ) (v : Slow) : FiberAgreement U (VariableGaugeMean.streamPotential d a b M (stableLength coord) v F) (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength coord) v f)

theorem NavierStokes.OffplaneCorrectionExtensions.compactAlias_agreement {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) {U : Set Slow} {F f : Lift → ℝ} (he : FiberAgreement U F f) (d a b M : ℝ) (v : Slow) : FiberAgreement U (VariableGaugeMean.compactAlias d a b M (stableLength coord) v F) (VariableGaugeMean.compactAlias d a b M (VariableGaugeMean.qLength coord) v f)

theorem NavierStokes.OffplaneCorrectionExtensions.temporalAtIndex_agreement {U : Set Slow} {F f : Lift → ℝ} (he : FiberAgreement U F f) (h : ℝ) (n i : ℕ) : FiberAgreement U (MeanChartCompatibility.temporalAtIndex h n i F) (MeanChartCompatibility.temporalAtIndex h n i f)

structure NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation {coord a b : ℝ} (W : Window coord a b) (f : Lift → ℝ) : Type

A full-fiber primitive continuation. Constructors below obtain such data from explicit positive-q models, then preserve it through the actual nonlocal mean operations.

• value : Lift → ℝ

  Value of SupportedContinuation, of type Lift → ℝ.

• smooth : ContDiffOn ℝ (↑⊤) self.value (PhysicalMeanDomain.slowDomain W.carrier)
• supported : VariableGaugeMean.SupportedGauge a b (stableLength coord) W.carrier self.value
• agrees : FiberAgreement W.carrier self.value f

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.ofModel {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) (F : Model → ℝ) (hF : ContDiffOn ℝ (↑⊤) F modelDomain) (hs : ModelSupported a b F) : SupportedContinuation W (physicalSource coord F)

Of model, bundling value, smooth, supported, agrees.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.primitive {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) {f : Lift → ℝ} (e : SupportedContinuation W f) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) : SupportedContinuation W (VariableGaugeMean.compactPrimitive d a b M (VariableGaugeMean.qLength coord) v f)

Primitive, bundling value, smooth, supported, W and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.pressure {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) {f : Lift → ℝ} (e : SupportedContinuation W f) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) : SupportedContinuation W (VariableGaugeMean.meanPressure d a b M hab (VariableGaugeMean.qLength coord) v f)

Pressure, bundling value, smooth, supported, W and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.stream {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) {f : Lift → ℝ} (e : SupportedContinuation W f) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) : SupportedContinuation W (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength coord) v f)

Stream, bundling value, smooth, supported, W and the required compatibility proofs.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.aliasField {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) {f : Lift → ℝ} (e : SupportedContinuation W f) (ha : 0 < a) (hab : a < b) {d : ℝ} (hd : 0 < d) (M : ℝ) (v : Slow) : SupportedContinuation W (VariableGaugeMean.compactAlias d a b M (VariableGaugeMean.qLength coord) v f)

Alias field, bundling value, smooth, supported, agrees.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.temporal {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) (h : ℝ) (n i : ℕ) (hp : PhysicalMeanDomain.PeriodicOn W.carrier e.value) : SupportedContinuation W (MeanChartCompatibility.temporalAtIndex h n i f)

Temporal, bundling value, smooth, supported, agrees.

Equations

• e.temporal h n i hp = { value := NavierStokes.MeanChartCompatibility.temporalAtIndex h n i e.value, smooth := ⋯, supported := ⋯, agrees := ⋯ }

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.scaleSlow {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) {c : Slow → ℝ} (C : Slow → ℝ) (hC : ContDiffOn ℝ (↑⊤) C W.carrier) (he : Set.EqOn C c (W.carrier ∩ positiveSlow)) : SupportedContinuation W fun (p : Lift) => c p.2.1 * f p

Scale slow, bundling value, smooth, supported, agrees.

Equations

• e.scaleSlow C hC he = { value := fun (p : NavierStokes.OffplaneCorrectionExtensions.Lift) => C p.2.1 * e.value p, smooth := ⋯, supported := ⋯, agrees := ⋯ }

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.finiteSum {coord a b : ℝ} {W : Window coord a b} {ι : Type u_1} (s : Finset ι) (f : ι → Lift → ℝ) (e : (i : ι) → SupportedContinuation W (f i)) : SupportedContinuation W fun (p : Lift) => ∑ i ∈ s, f i p

Finite sum, bundling value, smooth, supported, agrees and the required compatibility proofs.

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.pressureMass_smooth {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) : ContDiffOn ℝ (↑⊤) (PressureStream.pressureMass e.value) W.carrier

Actual radial/torus integration produces smooth slow debt coefficients on the continued neighborhood.

theorem NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.pressureMass_agreement {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) : Set.EqOn (PressureStream.pressureMass e.value) (PressureStream.pressureMass f) (W.carrier ∩ positiveSlow)

theorem NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.support_on_past {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) (hc : 0 < coord) (hc1 : coord < 1) {p : Lift} (hp : p.2.1 ∈ W.carrier) (ht : 0 < p.2.1.1) (hn : f p ≠ 0) : p.1 ∈ Set.Icc (VariableGaugeMean.qLength coord p.2.1 * a) (VariableGaugeMean.qLength coord p.2.1 * b)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.pullLinearData {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : P → Q) (d : CommonCoverSolve.LinearData Q V E) : CommonCoverSolve.LinearData P V E

Reparameterize primitive ODE coefficients and forcing, while keeping the native-copy path and its entry point unchanged.

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.coefficientPath_pull {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : P → Q) (d : CommonCoverSolve.LinearData Q V E) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (p : P × Slow) (a b : ℝ) : (pullLinearData φ d).coefficientPath g k p = d.coefficientPath g k (φ p.1, p.2)

theorem NavierStokes.OffplaneCorrectionExtensions.forcingPath_pull {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : P → Q) (d : CommonCoverSolve.LinearData Q V E) (g : CommonCoverSolve.Geometry) (k : TorusInverse.Frequency) (p : P × Slow) (a b : ℝ) : (pullLinearData φ d).forcingPath g k p = d.forcingPath g k (φ p.1, p.2)

theorem NavierStokes.OffplaneCorrectionExtensions.copySolve_pull {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (φ : P → Q) (d : CommonCoverSolve.LinearData Q V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (k : TorusInverse.Frequency) (p : P × Slow) : (pullLinearData φ d).copySolve g hab k p = d.copySolve g hab k (φ p.1, p.2)

This is the actual Volterra solution operator, including its anchored path. Reparameterization is an equality of definitions.

theorem NavierStokes.OffplaneCorrectionExtensions.commonSolve_pull {P Q V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (φ : P → Q) (d : CommonCoverSolve.LinearData Q V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : Slow → ℝ) (p : P × Slow) : (pullLinearData φ d).commonSolve g hab κ p = d.commonSolve g hab κ (φ p.1, p.2)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.stableParameter (coord : ℝ) (p : ℝ × Slow) : MeanRankUpdate.ModelPoint

Stable parameter, given by (stableQ coord p.2, (p.1, p.2.2)).

Equations

• NavierStokes.OffplaneCorrectionExtensions.stableParameter coord p = (NavierStokes.OffplaneCorrectionExtensions.stableQ coord p.2, p.1, p.2.2)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalParameter (coord : ℝ) (p : ℝ × Slow) : MeanRankUpdate.ModelPoint

Physical parameter, given by (SimilarityCoordinates.coordinateQ coord p.2, (p.1, p.2.2)).

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalParameter coord p = (NavierStokes.SimilarityCoordinates.coordinateQ coord p.2, p.1, p.2.2)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.continuedReferenceSolve {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (coord : ℝ) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : Slow → ℝ) : Lift → E

Continued reference solve, defined pointwise by (pullLinearData (stableParameter coord) d).commonSolve g hab κ ((p.1, p.2.1), p.2.2).

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalReferenceSolve {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (coord : ℝ) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : Slow → ℝ) : Lift → E

Physical reference solve, defined pointwise by (pullLinearData (physicalParameter coord) d).commonSolve g hab κ ((p.1, p.2.1), p.2.2).

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.continuedReferenceSolve_eq {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (coord : ℝ) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : Slow → ℝ) : continuedReferenceSolve coord d g hab κ = d.commonSolve g hab κ ∘ stableModel coord

theorem NavierStokes.OffplaneCorrectionExtensions.physicalReferenceSolve_eq {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (coord : ℝ) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : Slow → ℝ) : physicalReferenceSolve coord d g hab κ = d.commonSolve g hab κ ∘ physicalModel coord

theorem NavierStokes.OffplaneCorrectionExtensions.continuedReferenceSolve_smooth {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) {κ : Slow → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hcκ : HasCompactSupport κ) (hsκ : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo a b) : ContDiffOn ℝ (↑⊤) (continuedReferenceSolve coord d g hab κ) (PhysicalMeanDomain.slowDomain (PositiveRepresentatives.stableTarget coord))

The actual sum of localized native Volterra solves continues smoothly from smooth primitive matrix, conversion map, and source models. No regularity assumption is made on a solved amplitude.

theorem NavierStokes.OffplaneCorrectionExtensions.referenceSolve_agreement {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {a b : ℝ} (hab : a ≤ b) (κ : Slow → ℝ) (U : Set Slow) : FiberAgreement U (continuedReferenceSolve coord d g hab κ) (physicalReferenceSolve coord d g hab κ)

theorem NavierStokes.OffplaneCorrectionExtensions.referenceSolve_model_supported {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {s t : ℝ} (hst : s ≤ t) (κ : Slow → ℝ) {a b : ℝ} (hs : ModelSupported a b d.source) : ModelSupported a b (d.commonSolve g hst κ)

Radial support of the primitive forcing propagates through the zero-entry Volterra solve and the actual sum of its native copies.

noncomputable def NavierStokes.OffplaneCorrectionExtensions.referenceContinuation {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {s t : ℝ} (hst : s ≤ t) (hA : ContDiffOn ℝ (↑⊤) d.coefficient (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hB : ContDiffOn ℝ (↑⊤) d.forcingMap (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hs : ModelSupported a b d.source) {κ : Slow → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hcκ : HasCompactSupport κ) (hsκ : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo s t) (L : E →L[ℝ] ℝ) : SupportedContinuation W fun (p : Lift) => L (physicalReferenceSolve coord d g hst κ p)

A real component of an actual reference solve supplies a primitive continuation for the mean calculus. Its smoothness and support are derived from the ODE inputs, not assumed for the solved component.

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.continued_periodic_phase_smooth {coord : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (g : CommonCoverSolve.Geometry) (w : PeriodicPhaseAssembly.ClockWindow) {A B : MeanRankUpdate.ModelPoint → ℝ} (hA : ContDiffOn ℝ (↑⊤) A PhysicalCoordinateBounds.positiveTime) (hB : ContDiffOn ℝ (↑⊤) B PhysicalCoordinateBounds.positiveTime) : ContDiffOn ℝ (↑⊤) (continuedSource coord (PeriodicPhaseAssembly.phase g w.cutoff A B)) (PhysicalMeanDomain.slowDomain (PositiveRepresentatives.stableTarget coord))

The actual periodic-clock phase is continued by the same stable parameter substitution, keeping every clock and native-copy datum fixed.

noncomputable def NavierStokes.OffplaneCorrectionExtensions.referenceCarrierModel {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {s t : ℝ} (hst : s ≤ t) (κ : Slow → ℝ) (w : PeriodicPhaseAssembly.ClockWindow) (A B : MeanRankUpdate.ModelPoint → ℝ) (frequency : ℝ) (L : E →L[ℝ] ℂ) (y : Model) : ℝ

Reference carrier model, given by (HarmonicCalculus.mode frequency (PeriodicPhaseAssembly.phase g w.cutoff A B) (fun z => L (d.commonSolve g hst κ z)) y).re.

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.referenceCarrier_physical_formula {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (coord : ℝ) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {s t : ℝ} (hst : s ≤ t) (κ : Slow → ℝ) (w : PeriodicPhaseAssembly.ClockWindow) (A B : MeanRankUpdate.ModelPoint → ℝ) (frequency : ℝ) (L : E →L[ℝ] ℂ) (p : Lift) : physicalSource coord (referenceCarrierModel d g hst κ w A B frequency L) p = (L (physicalReferenceSolve coord d g hst κ p) * HarmonicCalculus.carrier frequency (physicalSource coord (PeriodicPhaseAssembly.phase g w.cutoff A B)) p).re

The complete carrier keeps the genuine periodic clock and multiplies the actual reference solve. The phase is not replaced by an unwrapped single-copy expression.

noncomputable def NavierStokes.OffplaneCorrectionExtensions.referenceCarrierContinuation {V E : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) (d : CommonCoverSolve.LinearData MeanRankUpdate.ModelPoint V E) (g : CommonCoverSolve.Geometry) {s t : ℝ} (hst : s ≤ t) (hM : ContDiffOn ℝ (↑⊤) d.coefficient (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hL : ContDiffOn ℝ (↑⊤) d.forcingMap (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hf : ContDiffOn ℝ (↑⊤) d.source (PhysicalCoordinateBounds.positiveTime ×ˢ Set.univ)) (hs : ModelSupported a b d.source) {κ : Slow → ℝ} (hκ : ContDiff ℝ (↑⊤) κ) (hcκ : HasCompactSupport κ) (hsκ : tsupport κ ⊆ Set.univ ×ˢ Set.Ioo s t) (w : PeriodicPhaseAssembly.ClockWindow) (A B : MeanRankUpdate.ModelPoint → ℝ) (hA : ContDiffOn ℝ (↑⊤) A PhysicalCoordinateBounds.positiveTime) (hB : ContDiffOn ℝ (↑⊤) B PhysicalCoordinateBounds.positiveTime) (frequency : ℝ) (L : E →L[ℝ] ℂ) : SupportedContinuation W (physicalSource coord (referenceCarrierModel d g hst κ w A B frequency L))

Reference carrier continuation as an element of SupportedContinuation W (physicalSource coord (referenceCarrierModel d g hst κ w A B frequency L)).

Equations

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

theorem NavierStokes.OffplaneCorrectionExtensions.rankAngular_model_supported (coord A B lam a b : ℝ) (hab : a < b) (d : MeanRankUpdate.Debt) : ModelSupported a b fun (y : Model) => MeanRankUpdate.angularModel coord A B lam a b d y.1

theorem NavierStokes.OffplaneCorrectionExtensions.rankAxial_model_supported (coord A B lam a b : ℝ) (hab : a < b) (d : MeanRankUpdate.Debt) : ModelSupported a b fun (y : Model) => MeanRankUpdate.axialModel coord A B lam a b d y.1

noncomputable def NavierStokes.OffplaneCorrectionExtensions.rankAngularContinuation {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) (A B lam : ℝ) (hB : B ≠ 0) (hab : a < b) (d : MeanRankUpdate.Debt) : SupportedContinuation W (MeanRankUpdate.chartKernel coord (MeanRankUpdate.angularModel coord A B lam a b d))

The explicit five-row angular kernel supplies its own primitive continuation; its smoothness is not an additional source assumption.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.rankAxialContinuation {coord a b : ℝ} {W : Window coord a b} (hc : 0 < coord) (hc1 : coord < 1) (A B lam : ℝ) (hB : B ≠ 0) (hab : a < b) (d : MeanRankUpdate.Debt) : SupportedContinuation W (MeanRankUpdate.chartKernel coord (MeanRankUpdate.axialModel coord A B lam a b d))

Rank axial continuation as an element of SupportedContinuation W (MeanRankUpdate.chartKernel coord (MeanRankUpdate.axialModel coord A B lam a b d)).

Equations

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

@[reducible, inline]

abbrev NavierStokes.OffplaneCorrectionExtensions.Space : Type

Space: an abbreviation for ProblemStatement.Space.

Equations

• NavierStokes.OffplaneCorrectionExtensions.Space = NavierStokes.ProblemStatement.Space

@[reducible, inline]

abbrev NavierStokes.OffplaneCorrectionExtensions.SpaceTime : Type

Space time: an abbreviation for ProblemStatement.SpaceTime.

Equations

• NavierStokes.OffplaneCorrectionExtensions.SpaceTime = NavierStokes.ProblemStatement.SpaceTime

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalSlow (w : SpaceTime) : Slow

Physical slow, given by (1 - w.1, w.2 2).

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalSlow w = (1 - w.1, w.2.ofLp 2)

theorem NavierStokes.OffplaneCorrectionExtensions.physicalSlow_contDiff : ContDiff ℝ (↑⊤) physicalSlow

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalLift (h : ℝ) (n : ℕ) (w : SpaceTime) : Lift

The actual radial/slow/native-graph restriction of a full-fiber mean field. The common covering level remains the supplied n.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalDomain (U : Set Slow) : Set SpaceTime

Physical domain, given by physicalSlow ⁻¹' U.

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalDomain U = NavierStokes.OffplaneCorrectionExtensions.physicalSlow ⁻¹' U

theorem NavierStokes.OffplaneCorrectionExtensions.physicalDomain_open {U : Set Slow} (hU : IsOpen U) : IsOpen (physicalDomain U)

theorem NavierStokes.OffplaneCorrectionExtensions.radius_pos_of_projection {w : SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : 0 < AnnularEndpoint.radius w

theorem NavierStokes.OffplaneCorrectionExtensions.radius_contDiffAt {w : SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : ContDiffAt ℝ (↑⊤) AnnularEndpoint.radius w

theorem NavierStokes.OffplaneCorrectionExtensions.physicalLift_contDiffAt (h : ℝ) (n : ℕ) {w : SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : ContDiffAt ℝ (↑⊤) (physicalLift h n) w

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalScalar (h : ℝ) (n : ℕ) (f : Lift → ℝ) : SpaceTime → ℝ

Physical scalar, given by f ∘ physicalLift h n.

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalScalar h n f = f ∘ NavierStokes.OffplaneCorrectionExtensions.physicalLift h n

theorem NavierStokes.OffplaneCorrectionExtensions.physicalScalar_zero_germ (h : ℝ) (n : ℕ) {U : Set Slow} (hU : IsOpen U) {c e : ℝ} {f : Lift → ℝ} (hs : PhysicalMeanDomain.SupportedOn c e U f) {w : SpaceTime} (hw : w ∈ physicalDomain U) (hr : AnnularEndpoint.radius w < c) : physicalScalar h n f =ᶠ[nhds w] fun (x : SpaceTime) => 0

theorem NavierStokes.OffplaneCorrectionExtensions.physicalScalar_smooth (h : ℝ) (n : ℕ) {U : Set Slow} (hU : IsOpen U) {c e : ℝ} (hc : 0 < c) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn c e U f) : ContDiffOn ℝ (↑⊤) (physicalScalar h n f) (physicalDomain U)

A positive lower radial support bound removes the coordinate singularity on the symmetry axis. No smoothness of the graph at the axis is assumed.

noncomputable def NavierStokes.OffplaneCorrectionExtensions.azimuthalPotential (h : ℝ) (n : ℕ) (f : Lift → ℝ) (w : SpaceTime) : Space

streamPotential is already the azimuthal component of the vector potential, including its division by the radial variable.

Equations

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

noncomputable def NavierStokes.OffplaneCorrectionExtensions.angularField (h : ℝ) (n : ℕ) (f : Lift → ℝ) : SpaceTime → Space

A direct angular velocity uses the same Cartesian multiplication by e_theta. This definition does not apply a curl or a radial primitive.

Equations

• NavierStokes.OffplaneCorrectionExtensions.angularField h n f = NavierStokes.OffplaneCorrectionExtensions.azimuthalPotential h n f

theorem NavierStokes.OffplaneCorrectionExtensions.azimuthalPotential_smooth (h : ℝ) (n : ℕ) {U : Set Slow} (hU : IsOpen U) {c e : ℝ} (hc : 0 < c) {f : Lift → ℝ} (hf : ContDiffOn ℝ (↑⊤) f (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanDomain.SupportedOn c e U f) : ContDiffOn ℝ (↑⊤) (azimuthalPotential h n f) (physicalDomain U)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.SupportedContinuation.physicalExtension {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) (h : ℝ) (n : ℕ) {x : Space} (hx : (0, x.ofLp 2) ∈ W.carrier) : JointResidualLimits.OneSidedExtension (physicalScalar h n f) x

Physical extension, 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.OffplaneCorrectionExtensions.SupportedContinuation.azimuthalExtension {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) (h : ℝ) (n : ℕ) {x : Space} (hx : (0, x.ofLp 2) ∈ W.carrier) : JointResidualLimits.OneSidedExtension (azimuthalPotential h n f) x

Azimuthal extension, 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.OffplaneCorrectionExtensions.SupportedContinuation.angularExtension {coord a b : ℝ} {W : Window coord a b} {f : Lift → ℝ} (e : SupportedContinuation W f) (h : ℝ) (n : ℕ) {x : Space} (hx : (0, x.ofLp 2) ∈ W.carrier) : JointResidualLimits.OneSidedExtension (angularField h n f) x

Angular extension, given by e.azimuthalExtension h n hx.

Equations

• e.angularExtension h n hx = e.azimuthalExtension h n hx

theorem NavierStokes.OffplaneCorrectionExtensions.mean_model_extensions {h a b d : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : Slow) (n : ℕ) (F : Model → ℝ) (hF : ContDiffOn ℝ (↑⊤) F modelDomain) (hs : ModelSupported a b F) {x : Space} (hx : x.ofLp 2 ≠ 0) : Nonempty (JointResidualLimits.OneSidedExtension (physicalScalar h n (VariableGaugeMean.meanPressure d a b M hab (VariableGaugeMean.qLength (2 * h)) v (physicalSource (2 * h) F))) x) ∧ Nonempty (JointResidualLimits.OneSidedExtension (azimuthalPotential h n (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength (2 * h)) v (physicalSource (2 * h) F))) x) ∧ Nonempty (JointResidualLimits.OneSidedExtension (SpatialCurl.spatialCurl (azimuthalPotential h n (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength (2 * h)) v (physicalSource (2 * h) F)))) x)

The scalar pressure and the actual azimuthal mean potential (and hence its Cartesian curl) have ambient endpoint extensions from primitive model smoothness and support. No extension of a solved field is an input.

theorem NavierStokes.OffplaneCorrectionExtensions.temporal_mean_model_extension {h a b d : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : Slow) (n i : ℕ) (F : Model → ℝ) (hF : ContDiffOn ℝ (↑⊤) F modelDomain) (hs : ModelSupported a b F) (hp : ModelPeriodic F) {x : Space} (hx : x.ofLp 2 ≠ 0) : Nonempty (JointResidualLimits.OneSidedExtension (azimuthalPotential h n (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength (2 * h)) v (MeanChartCompatibility.temporalAtIndex h n i (physicalSource (2 * h) F)))) x)

The actual temporal inverse is taken before reconstructing its mean stream potential. Its full-fiber continuation comes from the input torus periodicity and the proved inverse construction.

theorem NavierStokes.OffplaneCorrectionExtensions.mean_models_supported {coord a b d : ℝ} (hc : 0 < coord) (hc1 : coord < 1) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℝ) (v : Slow) (F : Model → ℝ) (hF : ContDiffOn ℝ (↑⊤) F modelDomain) (hs : ModelSupported a b F) : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) positiveSlow (VariableGaugeMean.meanPressure d a b M hab (VariableGaugeMean.qLength coord) v (physicalSource coord F)) ∧ VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength coord) positiveSlow (VariableGaugeMean.streamPotential d a b M (VariableGaugeMean.qLength coord) v (physicalSource coord F))

theorem NavierStokes.OffplaneCorrectionExtensions.physicalScalar_shrinkingSupport (h : ℝ) (n : ℕ) {a b : ℝ} {f : Lift → ℝ} (hf : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) positiveSlow f) : AnnularEndpoint.ShrinkingSupport h b (physicalScalar h n f)

theorem NavierStokes.OffplaneCorrectionExtensions.azimuthalPotential_shrinkingSupport (h : ℝ) (n : ℕ) {a b : ℝ} {f : Lift → ℝ} (hf : VariableGaugeMean.SupportedGauge a b (VariableGaugeMean.qLength (2 * h)) positiveSlow f) : AnnularEndpoint.ShrinkingSupport h b (azimuthalPotential h n f)

noncomputable def NavierStokes.OffplaneCorrectionExtensions.physicalQExtension (h : ℝ) (w : SpaceTime) : ℝ

Physical Q extension, given by (EndpointCoordinates.cartesianExtension h w).1.

Equations

• NavierStokes.OffplaneCorrectionExtensions.physicalQExtension h w = (NavierStokes.EndpointCoordinates.cartesianExtension h w).1

theorem NavierStokes.OffplaneCorrectionExtensions.physicalQExtension_eq {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {w : SpaceTime} (ht : w.1 < 1) : physicalQExtension h w = PhysicalWaveSum.physicalQ h w

theorem NavierStokes.OffplaneCorrectionExtensions.diagonal_extension {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {h : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) {a : ℕ → ℝ} (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {F : ℕ → SpaceTime → V} {x : Space} (hx : x.ofLp 2 ≠ 0) (he : ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (F j) x)) : Nonempty (JointResidualLimits.OneSidedExtension (SolenoidalDiagonal.potentialSum a (PhysicalWaveSum.physicalQ h) F) x)

Only finitely many stages survive near a positive-q endpoint. Their extensions are combined with the same scalar cutoffs and the same schedule. The preceding model/mean constructors supply the finite-stage extensions.

theorem NavierStokes.OffplaneCorrectionExtensions.mean_diagonal_extensions {h a b d : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℕ → ℝ) (v : ℕ → Slow) (n : ℕ → ℕ) (F : ℕ → Model → ℝ) (hF : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (F j) modelDomain) (hs : ∀ (j : ℕ), ModelSupported a b (F j)) {scale : ℕ → ℝ} (hscale : Filter.Tendsto scale Filter.atTop Filter.atTop) {x : Space} (hx : x.ofLp 2 ≠ 0) : have p := fun (j : ℕ) => physicalScalar h (n j) (VariableGaugeMean.meanPressure d a b (M j) hab (VariableGaugeMean.qLength (2 * h)) (v j) (physicalSource (2 * h) (F j))); have A := fun (j : ℕ) => azimuthalPotential h (n j) (VariableGaugeMean.streamPotential d a b (M j) (VariableGaugeMean.qLength (2 * h)) (v j) (physicalSource (2 * h) (F j))); Nonempty (JointResidualLimits.OneSidedExtension (SolenoidalDiagonal.potentialSum scale (PhysicalWaveSum.physicalQ h) p) x) ∧ Nonempty (JointResidualLimits.OneSidedExtension (SolenoidalDiagonal.potentialSum scale (PhysicalWaveSum.physicalQ h) A) x) ∧ Nonempty (JointResidualLimits.OneSidedExtension (SolenoidalDiagonal.velocitySum scale (PhysicalWaveSum.physicalQ h) A) x)

All stages of actual moving mean reconstruction can be summed with the chosen cutoff schedule at a nonzero-axial endpoint. The model assumptions are on the primitive source of each stage.

theorem NavierStokes.OffplaneCorrectionExtensions.mean_diagonal_awayExtensions {h a b d : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hd : 0 < d) (M : ℕ → ℝ) (v : ℕ → Slow) (n : ℕ → ℕ) (F : ℕ → Model → ℝ) (hF : ∀ (j : ℕ), ContDiffOn ℝ (↑⊤) (F j) modelDomain) (hs : ∀ (j : ℕ), ModelSupported a b (F j)) {scale : ℕ → ℝ} (hscale : Filter.Tendsto scale Filter.atTop Filter.atTop) : have p := fun (j : ℕ) => physicalScalar h (n j) (VariableGaugeMean.meanPressure d a b (M j) hab (VariableGaugeMean.qLength (2 * h)) (v j) (physicalSource (2 * h) (F j))); have A := fun (j : ℕ) => azimuthalPotential h (n j) (VariableGaugeMean.streamPotential d a b (M j) (VariableGaugeMean.qLength (2 * h)) (v j) (physicalSource (2 * h) (F j))); JointResidualLimits.AwayExtensions (SolenoidalDiagonal.potentialSum scale (PhysicalWaveSum.physicalQ h) p) ∧ JointResidualLimits.AwayExtensions (SolenoidalDiagonal.potentialSum scale (PhysicalWaveSum.physicalQ h) A) ∧ JointResidualLimits.AwayExtensions (SolenoidalDiagonal.velocitySum scale (PhysicalWaveSum.physicalQ h) A)

Combining the new positive-q continuation with the shrinking-support argument gives full away-extensions for these actually reconstructed mean families. The common outer support bound is a conclusion of the primitive model support, rather than an additional output assumption.