Angular stage data for the actual physical means

The scalar is the same physical mean evaluated on the positive radial half-plane. Radial symmetry of the actual auxiliary graph proves its Cartesian angular representation. Native annulus support gives a positive inner radius and the common shrinking outer support.

noncomputable def NavierStokes.ActualMeanStageData.radialSection (p : DirectAngularDiagonal.CylPoint) : ProblemStatement.SpaceTime

The fixed positive radial half-plane, without changing any graph data.

Equations

• NavierStokes.ActualMeanStageData.radialSection p = (p.1, NavierStokes.AxisymmetricResidual.pack p.2.1 0 p.2.2)

theorem NavierStokes.ActualMeanStageData.radialSection_smooth : ContDiff ℝ (↑⊤) radialSection

theorem NavierStokes.ActualMeanStageData.radialSection_slow (p : DirectAngularDiagonal.CylPoint) : DirectAngularDiagonal.slowPoint (radialSection p) = DirectAngularDiagonal.slowOfCyl p

theorem NavierStokes.ActualMeanStageData.radialSection_radius {p : DirectAngularDiagonal.CylPoint} (hp : 0 ≤ p.2.1) : DirectAngularDiagonal.radius (radialSection p) = p.2.1

theorem NavierStokes.ActualMeanStageData.physicalPoint_radialSection (h : ℝ) (w : ProblemStatement.SpaceTime) : PhysicalMeanJetBounds.physicalPoint h (radialSection (DirectAngularDiagonal.cylPoint w)) = PhysicalMeanJetBounds.physicalPoint h w

The auxiliary graph, as well as the slow and radial coordinates, is unchanged when a Cartesian point is moved to its positive radial half-plane.

noncomputable def NavierStokes.ActualMeanStageData.coefficient {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) : DirectAngularDiagonal.Coefficient

Coefficient, given by D.field ∘ radialSection.

Equations

• NavierStokes.ActualMeanStageData.coefficient D = D.field ∘ NavierStokes.ActualMeanStageData.radialSection

theorem NavierStokes.ActualMeanStageData.coefficient_cylPoint {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (w : ProblemStatement.SpaceTime) : coefficient D (DirectAngularDiagonal.cylPoint w) = D.field w

theorem NavierStokes.ActualMeanStageData.coefficient_angularField {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) : DirectAngularDiagonal.angularField (coefficient D) = D.angularField

This is a global identity, including the totalized angular frame at the axis.

noncomputable def NavierStokes.ActualMeanStageData.innerRadius (h a : ℝ) (s : DirectAngularDiagonal.Slow) : ℝ

A conservative inner radius common to every native band and stage.

Equations

• NavierStokes.ActualMeanStageData.innerRadius h a s = a / 4 * √(NavierStokes.LocalAngularDiagonal.slowQ h s)

theorem NavierStokes.ActualMeanStageData.innerRadius_continuous {h a qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) : ContinuousOn (innerRadius h a) (LocalAngularDiagonal.localSlowDomain h qbig)

theorem NavierStokes.ActualMeanStageData.innerRadius_pos {h a qbig : ℝ} (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) {s : DirectAngularDiagonal.Slow} (hs : s ∈ LocalAngularDiagonal.localSlowDomain h qbig) : 0 < innerRadius h a s

theorem NavierStokes.ActualMeanStageData.physical_radius_scale (n : ℕ) (w : ProblemStatement.SpaceTime) : DirectAngularDiagonal.radius w = √(ChartScales.Q n) * PolarCharts.radius ((PhysicalGraphBounds.scaledRadial n) w)

theorem NavierStokes.ActualMeanStageData.innerRadius_le_of_ne {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) {a b : ℝ} (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hq : PhysicalWaveSum.physicalQ h w ≤ ChartScales.Q N) (hne : D.field w ≠ 0) : innerRadius h a (DirectAngularDiagonal.slowPoint w) ≤ DirectAngularDiagonal.radius w

An actual nonzero physical coefficient must lie outside the positive inner radius. The proof selects a valid comparable band and uses its native support.

theorem NavierStokes.ActualMeanStageData.coefficient_smooth {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) {a b : ℝ} (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : ContDiffOn ℝ (↑⊤) (coefficient D) (DirectAngularDiagonal.positiveDomain (LocalAngularDiagonal.localSlowDomain h qbig))

theorem NavierStokes.ActualMeanStageData.coefficient_vanishes {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) {a b : ℝ} (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) (p : DirectAngularDiagonal.CylPoint) (hp : DirectAngularDiagonal.slowOfCyl p ∈ LocalAngularDiagonal.localSlowDomain h qbig) (hr : 0 ≤ p.2.1) (hinner : p.2.1 < innerRadius h a (DirectAngularDiagonal.slowOfCyl p)) : coefficient D p = 0

noncomputable def NavierStokes.ActualMeanStageData.coherentAngularData {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) {a b : ℝ} (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain h qbig)

Coherent angular data, bundling scalar, smooth, inner, inner_continuous and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualMeanStageData.coherentAngularData_field {h degree : ℝ} {N Δ : ℕ} {U : Set PhysicalGraphBounds.Plane} (D : PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) {a b : ℝ} (ha : 0 < a) (hab : a < b) (hU : IsOpen U) (hcover : PhysicalMeanDomain.normalizedSlowDomain (2 * h) (1 / 2) 2 ⊆ U) (hsm : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (coherentAngularData D hh hh1 ha hab hU hcover hsm hs qbig hq).scalar = D.angularField

The fixed actual atlas and native moving support

theorem NavierStokes.ActualMeanStageData.nativeSupport_of_moving {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) : PhysicalMeanJetBounds.NativeSupport CorrectionInitialization.ActualPrimary.h ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b N CorrectionInitialization.ActualPrimary.standardRegion.carrier D.native

noncomputable def NavierStokes.ActualMeanStageData.actualAngularData {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Actual angular data, constructed using coherentAngularData.

Equations

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

@[simp]

theorem NavierStokes.ActualMeanStageData.actualAngularData_field {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (actualAngularData D Hm qbig hq).scalar = D.angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.actualAngularData_inner {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (actualAngularData D Hm qbig hq).inner = innerRadius CorrectionInitialization.ActualPrimary.h ActualInitialization.geometry.patch.a

noncomputable def NavierStokes.ActualMeanStageData.actualAngularSupport {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Actual angular support, given by MixedAxisPreservation.AngularSupport.ofAngularData (actualAngularData D Hm qbig hq) (fun _ hw => hw).

Equations

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

@[simp]

theorem NavierStokes.ActualMeanStageData.actualAngularSupport_field {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (actualAngularSupport D Hm qbig hq).field = D.angularField

theorem NavierStokes.ActualMeanStageData.actualAngularData_shrinkingSupport {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (DirectAngularDiagonal.angularField (actualAngularData D Hm qbig hq).scalar)

theorem NavierStokes.ActualMeanStageData.actualAngularSupport_shrinkingSupport {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (actualAngularSupport D Hm qbig hq).field

theorem NavierStokes.ActualMeanStageData.actualAngular_zero_germ {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (hw : w ∈ MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig) (hr : DirectAngularDiagonal.radius w < innerRadius CorrectionInitialization.ActualPrimary.h ActualInitialization.geometry.patch.a (DirectAngularDiagonal.slowPoint w)) : D.angularField =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

theorem NavierStokes.ActualMeanStageData.actualAngular_axis_zero_germ {degree : ℝ} {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily CorrectionInitialization.ActualPrimary.h degree N Δ CorrectionInitialization.ActualPrimary.standardRegion.carrier ℝ) (Hm : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer D.native) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) {w : ProblemStatement.SpaceTime} (hw : w ∈ MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig) (hr : DirectAngularDiagonal.radius w = 0) : D.angularField =ᶠ[nhds w] fun (x : ProblemStatement.SpaceTime) => 0

Initialized direct angular mean and actual temporal/rank streams

noncomputable def NavierStokes.ActualMeanStageData.initialAngularData (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial angular data, given by actualAngularData (initialAngularFamily B N0 N) (initial_mean_moving B N0).angular qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.initialTemporalData (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial temporal data, given by actualAngularData (initialTemporalFamily B N0 N) (initialTemporal_moving B N0) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.initialRankData (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial rank data, given by actualAngularData (initialRankFamily B N0 N) (initialRank_moving B N0) qbig hq.

Equations

• NavierStokes.ActualMeanStageData.initialRankData B N0 N qbig hq = NavierStokes.ActualMeanStageData.actualAngularData (NavierStokes.ActualMeanPhysicalData.initialRankFamily B N0 N) ⋯ qbig hq

noncomputable def NavierStokes.ActualMeanStageData.initialStreamData (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial stream data, given by actualAngularData (initialStreamFamily B N0 N) (initialStream_moving B N0) qbig hq.

Equations

• NavierStokes.ActualMeanStageData.initialStreamData B N0 N qbig hq = NavierStokes.ActualMeanStageData.actualAngularData (NavierStokes.ActualMeanPhysicalData.initialStreamFamily B N0 N) ⋯ qbig hq

@[simp]

theorem NavierStokes.ActualMeanStageData.initialAngularData_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (initialAngularData B N0 N qbig hq).scalar = (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.initialTemporalData_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (initialTemporalData B N0 N qbig hq).scalar = (ActualMeanPhysicalData.initialTemporalFamily B N0 N).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.initialRankData_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (initialRankData B N0 N qbig hq).scalar = (ActualMeanPhysicalData.initialRankFamily B N0 N).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.initialStreamData_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (initialStreamData B N0 N qbig hq).scalar = (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField

noncomputable def NavierStokes.ActualMeanStageData.initialAngularSupport (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial angular support, given by actualAngularSupport (initialAngularFamily B N0 N) (initial_mean_moving B N0).angular qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.initialTemporalSupport (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial temporal support, given by actualAngularSupport (initialTemporalFamily B N0 N) (initialTemporal_moving B N0) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.initialRankSupport (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial rank support, given by actualAngularSupport (initialRankFamily B N0 N) (initialRank_moving B N0) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.initialStreamSupport (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Initial stream support, given by actualAngularSupport (initialStreamFamily B N0 N) (initialStream_moving B N0) qbig hq.

Equations

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

@[simp]

theorem NavierStokes.ActualMeanStageData.initialAngularSupport_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (initialAngularSupport B N0 N qbig hq).field = (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.initialTemporalSupport_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (initialTemporalSupport B N0 N qbig hq).field = (ActualMeanPhysicalData.initialTemporalFamily B N0 N).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.initialRankSupport_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (initialRankSupport B N0 N qbig hq).field = (ActualMeanPhysicalData.initialRankFamily B N0 N).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.initialStreamSupport_field (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (initialStreamSupport B N0 N qbig hq).field = (ActualMeanPhysicalData.initialStreamFamily B N0 N).angularField

theorem NavierStokes.ActualMeanStageData.initial_shrinkingSupport (B N0 N : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (initialAngularSupport B N0 N qbig hq).field ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (initialTemporalSupport B N0 N qbig hq).field ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (initialRankSupport B N0 N qbig hq).field ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (initialStreamSupport B N0 N qbig hq).field

The literal iterated mean stages

noncomputable def NavierStokes.ActualMeanStageData.cycleAngularData {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle angular data, given by actualAngularData ((initialCycleData H).angularIncrementFamily k) ((initialCycleData H).angularIncrement_moving k) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.cycleTemporalData {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle temporal data, given by actualAngularData ((initialCycleData H).temporalFamily k) ((initialCycleData H).temporal_moving k) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.cycleRankData {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle rank data, given by actualAngularData ((initialCycleData H).rankFamily k) ((initialCycleData H).rank_moving k) qbig hq.

Equations

• NavierStokes.ActualMeanStageData.cycleRankData H k qbig hq = NavierStokes.ActualMeanStageData.actualAngularData ((NavierStokes.ActualMeanPhysicalData.initialCycleData H).rankFamily k) ⋯ qbig hq

noncomputable def NavierStokes.ActualMeanStageData.cycleStreamData {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle stream data, given by actualAngularData ((initialCycleData H).streamFamily k) ((initialCycleData H).stream_moving k) qbig hq.

Equations

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

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleAngularData_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (cycleAngularData H k qbig hq).scalar = ((ActualMeanPhysicalData.initialCycleData H).angularIncrementFamily k).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleTemporalData_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (cycleTemporalData H k qbig hq).scalar = ((ActualMeanPhysicalData.initialCycleData H).temporalFamily k).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleRankData_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (cycleRankData H k qbig hq).scalar = ((ActualMeanPhysicalData.initialCycleData H).rankFamily k).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleStreamData_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : DirectAngularDiagonal.angularField (cycleStreamData H k qbig hq).scalar = ((ActualMeanPhysicalData.initialCycleData H).streamFamily k).angularField

noncomputable def NavierStokes.ActualMeanStageData.cycleAngularSupport {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle angular support, given by actualAngularSupport ((initialCycleData H).angularIncrementFamily k) ((initialCycleData H).angularIncrement_moving k) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.cycleTemporalSupport {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle temporal support, given by actualAngularSupport ((initialCycleData H).temporalFamily k) ((initialCycleData H).temporal_moving k) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.cycleRankSupport {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle rank support, given by actualAngularSupport ((initialCycleData H).rankFamily k) ((initialCycleData H).rank_moving k) qbig hq.

Equations

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

noncomputable def NavierStokes.ActualMeanStageData.cycleStreamSupport {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedAxisPreservation.AngularSupport (MixedAxisPreservation.localDomain CorrectionInitialization.ActualPrimary.h qbig)

Cycle stream support, given by actualAngularSupport ((initialCycleData H).streamFamily k) ((initialCycleData H).stream_moving k) qbig hq.

Equations

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

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleAngularSupport_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (cycleAngularSupport H k qbig hq).field = ((ActualMeanPhysicalData.initialCycleData H).angularIncrementFamily k).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleTemporalSupport_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (cycleTemporalSupport H k qbig hq).field = ((ActualMeanPhysicalData.initialCycleData H).temporalFamily k).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleRankSupport_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (cycleRankSupport H k qbig hq).field = ((ActualMeanPhysicalData.initialCycleData H).rankFamily k).angularField

@[simp]

theorem NavierStokes.ActualMeanStageData.cycleStreamSupport_field {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : (cycleStreamSupport H k qbig hq).field = ((ActualMeanPhysicalData.initialCycleData H).streamFamily k).angularField

theorem NavierStokes.ActualMeanStageData.cycle_shrinkingSupport {B N0 N : ℕ} {p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)} (H : ActualMeanPhysicalData.InitialCycleInput B N0 N p) (k : ℕ) (qbig : ℝ) (hq : qbig ≤ ChartScales.Q N) : MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (cycleAngularSupport H k qbig hq).field ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (cycleTemporalSupport H k qbig hq).field ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (cycleRankSupport H k qbig hq).field ∧ MixedDiagonalExtensions.SublevelShrinkingSupport CorrectionInitialization.ActualPrimary.h PhysicalStageSupport.actualOuterConstant qbig (cycleStreamSupport H k qbig hq).field