Actual Cartesian curls of the mean stream potentials

The azimuthal potential carries the scale velocity/radialScale. Its genuine Cartesian curl is the meridional stream pair in the same physical graph.

@[reducible, inline]

abbrev NavierStokes.ActualMeanPotentialRealization.Point : Type

Point: an abbreviation for PhysicalResidualTZ.Lift.

Equations

• NavierStokes.ActualMeanPotentialRealization.Point = NavierStokes.PhysicalResidualTZ.Lift

@[reducible, inline]

abbrev NavierStokes.ActualMeanPotentialRealization.Cylinder : Type

Cylinder: an abbreviation for PhysicalResidualTZ.Cylinder.

Equations

• NavierStokes.ActualMeanPotentialRealization.Cylinder = NavierStokes.PhysicalResidualTZ.Cylinder

@[reducible, inline]

abbrev NavierStokes.ActualMeanPotentialRealization.ScaledGraph : Type

Scaled graph: an abbreviation for PhysicalResidualBridge.ScaledGraph.

Equations

• NavierStokes.ActualMeanPotentialRealization.ScaledGraph = NavierStokes.PhysicalResidualBridge.ScaledGraph

noncomputable def NavierStokes.ActualMeanPotentialRealization.axial : (ℝ × ℝ) × ℝ × ℝ

Axial, given by ((0, 1), 0).

Equations

• NavierStokes.ActualMeanPotentialRealization.axial = ((0, 1), 0)

noncomputable def NavierStokes.ActualMeanPotentialRealization.chartPoint (G : ScaledGraph) (z : ProblemStatement.SpaceTime) : Point

Chart point, given by (PhysicalResidualTZ.graphMapTZ G z).1.

Equations

• NavierStokes.ActualMeanPotentialRealization.chartPoint G z = (NavierStokes.PhysicalResidualTZ.graphMapTZ G z).1

noncomputable def NavierStokes.ActualMeanPotentialRealization.meridional (G : ScaledGraph) (Ψ : Point → ℝ) (x : Cylinder) : Fin 3 → ℝ

Meridional as an element of Fin 3 → ℝ.

Equations

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

noncomputable def NavierStokes.ActualMeanPotentialRealization.componentPotential (G : ScaledGraph) (Ψ : Point → ℝ) (z : ProblemStatement.SpaceTime) : ProblemStatement.Space

Component potential, given by AxisymmetricResidual.pack 0 ((G.velocityScale / G.radialScale) * Ψ (chartPoint G z)) 0.

Equations

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

noncomputable def NavierStokes.ActualMeanPotentialRealization.cartesianPotential (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (Ψ : Point → ℝ) : ProblemStatement.VelocityField

The same local polar realization used by the physical cycle prefixes.

Equations

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

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_smoothAt (G : ScaledGraph) {z : ProblemStatement.SpaceTime} (hr : G.radialScale * z.2.ofLp 0 ≠ 0) : ContDiffAt ℝ (↑⊤) (chartPoint G) z

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_fderiv (G : ScaledGraph) {z : ProblemStatement.SpaceTime} (hr : G.radialScale * z.2.ofLp 0 ≠ 0) (w : ProblemStatement.SpaceTime) : (fderiv ℝ (chartPoint G) z) w = PhysicalResidualTZ.swapSlow ((fderiv ℝ (PhysicalResidualBridge.ScaledGraph.map G) z) w).1

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_radius (G : ScaledGraph) (z : ProblemStatement.SpaceTime) : (chartPoint G z).1 = G.radialScale * z.2.ofLp 0

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_radial (G : ScaledGraph) {z : ProblemStatement.SpaceTime} (hr : G.radialScale * z.2.ofLp 0 ≠ 0) : (fderiv ℝ (chartPoint G) z) (LinearWaveResidual.spaceDirection 0 z) = G.radialScale • PressureStream.radialVector (PressureStream.physicalSpeed G.exponent G.frequency) (0, G.radialVector) (chartPoint G z)

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_axial (G : ScaledGraph) {z : ProblemStatement.SpaceTime} (hr : G.radialScale * z.2.ofLp 0 ≠ 0) : (fderiv ℝ (chartPoint G) z) (LinearWaveResidual.spaceDirection 2 z) = G.radialScale • (0, G.epsilon • axial)

theorem NavierStokes.ActualMeanPotentialRealization.scalar_radial (G : ScaledGraph) (hl : 0 < G.radialScale) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) {Ψ : Point → ℝ} (hΨ : DifferentiableAt ℝ Ψ (chartPoint G z)) : HarmonicCalculus.along (LinearWaveResidual.spaceDirection 0) (fun (p : ProblemStatement.SpaceTime) => G.velocityScale / G.radialScale * Ψ (chartPoint G p)) z = G.velocityScale * PressureStream.graphDr (PressureStream.physicalSpeed G.exponent G.frequency) (0, G.radialVector) Ψ (chartPoint G z)

theorem NavierStokes.ActualMeanPotentialRealization.scalar_axial (G : ScaledGraph) (hl : 0 < G.radialScale) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) {Ψ : Point → ℝ} (hΨ : DifferentiableAt ℝ Ψ (chartPoint G z)) : HarmonicCalculus.along (LinearWaveResidual.spaceDirection 2) (fun (p : ProblemStatement.SpaceTime) => G.velocityScale / G.radialScale * Ψ (chartPoint G p)) z = G.velocityScale * PressureStream.graphDz (G.epsilon • axial) Ψ (chartPoint G z)

theorem NavierStokes.ActualMeanPotentialRealization.componentPotential_smoothAt (G : ScaledGraph) {z : ProblemStatement.SpaceTime} (hr : G.radialScale * z.2.ofLp 0 ≠ 0) {Ψ : Point → ℝ} (hΨ : ContDiffAt ℝ (↑⊤) Ψ (chartPoint G z)) : ContDiffAt ℝ (↑⊤) (componentPotential G Ψ) z

theorem NavierStokes.ActualMeanPotentialRealization.componentPotential_realCurl (G : ScaledGraph) (hl : 0 < G.radialScale) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) {Ψ : Point → ℝ} (hΨ : DifferentiableAt ℝ Ψ (chartPoint G z)) (i : Fin 3) : PhysicalCurlCovariance.realCurl LinearWaveResidual.coordinateRadius (LinearWaveResidual.spaceDirection 0) (LinearWaveResidual.spaceDirection 1) (LinearWaveResidual.spaceDirection 2) (fun (p : ProblemStatement.SpaceTime) (i : Fin 3) => (componentPotential G Ψ p).ofLp i) z i = G.velocityScale * meridional G Ψ (PhysicalResidualTZ.graphMapTZ G z) i

The connection term Ψ/R is retained in the actual cylindrical curl.

theorem NavierStokes.ActualMeanPotentialRealization.cartesianPotential_smoothAt {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) {Ψ : Point → ℝ} {w : ProblemStatement.SpaceTime} (hr : G.radialScale * (PhysicalCurlCovariance.polarCoordinates a j w).2.ofLp 0 ≠ 0) (hΨ : ContDiffAt ℝ (↑⊤) Ψ (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : ContDiffAt ℝ (↑⊤) (cartesianPotential a j G Ψ) w

theorem NavierStokes.ActualMeanPotentialRealization.polar_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (v : ProblemStatement.VelocityField) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) : (CyclePhysicalPrefixes.polarVelocityMap a j) v (z.1, CylindricalResidual.chart z.2) = (CylindricalResidual.frame (z.2.ofLp 1)) (v z)

theorem NavierStokes.ActualMeanPotentialRealization.cartesianPotential_forward_germ {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (Ψ : Point → ℝ) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) : (fun (p : ProblemStatement.SpaceTime) => cartesianPotential a j G Ψ (p.1, CylindricalResidual.chart p.2)) =ᶠ[nhds z] fun (p : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (p.2.ofLp 1)) (componentPotential G Ψ p)

theorem NavierStokes.ActualMeanPotentialRealization.cartesianPotential_curl_forward {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) {Ψ : Point → ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a j) (hΨ : ContDiffAt ℝ (↑⊤) Ψ (chartPoint G z)) : SpatialCurl.spatialCurl (cartesianPotential a j G Ψ) (z.1, CylindricalResidual.chart z.2) = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (meridional G Ψ)) (z.1, CylindricalResidual.chart z.2)

A value formula for the potential, differentiated by the real Cartesian curl theorem, yields the actual meridional velocity.

Ordinary Cartesian chart domains

noncomputable def NavierStokes.ActualMeanPotentialRealization.cartesianDomain (a : ℝ) (j : PolarCharts.Index) : Set ProblemStatement.SpaceTime

Cartesian domain, given by PhysicalGraphBounds.radialProjection ⁻¹' PolarCharts.chartDomain a j.

Equations

• NavierStokes.ActualMeanPotentialRealization.cartesianDomain a j = ⇑NavierStokes.PhysicalGraphBounds.radialProjection ⁻¹' NavierStokes.PolarCharts.chartDomain a j

theorem NavierStokes.ActualMeanPotentialRealization.cartesianDomain_open (a : ℝ) (j : PolarCharts.Index) : IsOpen (cartesianDomain a j)

theorem NavierStokes.ActualMeanPotentialRealization.polarCoordinates_valid {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) : PhysicalCurlCovariance.polarCoordinates a j w ∈ PhysicalCurlCovariance.validCylindrical a j

theorem NavierStokes.ActualMeanPotentialRealization.polarCoordinates_back {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) : ((PhysicalCurlCovariance.polarCoordinates a j w).1, CylindricalResidual.chart (PhysicalCurlCovariance.polarCoordinates a j w).2) = w

theorem NavierStokes.ActualMeanPotentialRealization.cartesianPotential_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) {Ψ : Point → ℝ} {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (hΨ : ContDiffAt ℝ (↑⊤) Ψ (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cartesianPotential a j G Ψ) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (meridional G Ψ)) w

The actual variable-gauge temporal and rank fields

structure NavierStokes.ActualMeanPotentialRealization.GaugeMatches (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (c : CorrectionState.Context Point) (G : ScaledGraph) (n : ℕ) : Prop

Only literal chart coefficients are matched here; no derivative or curl identity is part of this predicate.

• epsilon : c.operators.epsilon n = G.epsilon
• exponent : g.radial.exponent = G.exponent
• frequency : g.radial.frequency n = G.frequency
• radialVector : g.radial.radialDirection = G.radialVector

theorem NavierStokes.ActualMeanPotentialRealization.similarityGauge_matches (h a b : ℝ) (hab : a < b) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (n : ℕ) (hε : c.operators.epsilon n = ChartScales.Q n ^ h) : GaugeMatches (VariableGaugeMean.similarityGauge h (ChartScales.radialExponent h) a b 1 hab index) c (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (index n)) n

theorem NavierStokes.ActualMeanPotentialRealization.meridional_temporal (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (G : ScaledGraph) (n : ℕ) (H : GaugeMatches g c G n) : meridional G (VariableGaugeMean.temporalPotential g h index c u n) = CyclePhysicalPrefixes.meridionalComponents (VariableGaugeMean.temporalIncrementState g h index axial c u) n

theorem NavierStokes.ActualMeanPotentialRealization.meridional_rank (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (r : CorrectionState.RankData (ℝ × ℝ)) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (G : ScaledGraph) (n : ℕ) (H : GaugeMatches g c G n) : meridional G (VariableGaugeMean.rankPotential g r c u n) = CyclePhysicalPrefixes.meridionalComponents (VariableGaugeMean.rankIncrementState g r axial c u) n

theorem NavierStokes.ActualMeanPotentialRealization.temporalPotential_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (G : ScaledGraph) (hl : 0 < G.radialScale) (n : ℕ) (H : GaugeMatches g c G n) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (hΨ : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.temporalPotential g h index c u n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cartesianPotential a j G (VariableGaugeMean.temporalPotential g h index c u n)) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (CyclePhysicalPrefixes.meridionalComponents (VariableGaugeMean.temporalIncrementState g h index axial c u) n)) w

theorem NavierStokes.ActualMeanPotentialRealization.rankPotential_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (r : CorrectionState.RankData (ℝ × ℝ)) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (G : ScaledGraph) (hl : 0 < G.radialScale) (n : ℕ) (H : GaugeMatches g c G n) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (hΨ : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.rankPotential g r c u n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cartesianPotential a j G (VariableGaugeMean.rankPotential g r c u n)) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (CyclePhysicalPrefixes.meridionalComponents (VariableGaugeMean.rankIncrementState g r axial c u) n)) w

Identification with the coherent physical mean potential

theorem NavierStokes.ActualMeanPotentialRealization.projection_forward (z : ProblemStatement.SpaceTime) : PhysicalGraphBounds.radialProjection (z.1, CylindricalResidual.chart z.2) = PolarCharts.polar (z.2.ofLp 0, z.2.ofLp 1)

theorem NavierStokes.ActualMeanPotentialRealization.radius_forward {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : PhysicalClassBounds.cartesianRadius (PhysicalGraphBounds.radialProjection (z.1, CylindricalResidual.chart z.2)) = z.2.ofLp 0

theorem NavierStokes.ActualMeanPotentialRealization.physicalPoint_forward (h : ℝ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : PhysicalMeanJetBounds.physicalPoint h (z.1, CylindricalResidual.chart z.2) = PhysicalResidualTZ.absoluteLiftTZ h z

theorem NavierStokes.ActualMeanPotentialRealization.physicalToChartTZ_eq (h : ℝ) (n k : ℕ) : PhysicalResidualTZ.physicalToChartTZ h n k = VariableGaugeMean.physicalToChartTZ h n k

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_eq_graph_forward (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : chartPoint (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)) z = PhysicalMeanJetBounds.graph h n d (z.1, CylindricalResidual.chart z.2)

theorem NavierStokes.ActualMeanPotentialRealization.chartPoint_eq_graph {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) : chartPoint (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)) (PhysicalCurlCovariance.polarCoordinates a j w) = PhysicalMeanJetBounds.graph h n d w

theorem NavierStokes.ActualMeanPotentialRealization.angularVector_forward {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : PhysicalMeanJetBounds.angularVector (PhysicalGraphBounds.radialProjection (z.1, CylindricalResidual.chart z.2)) = (CylindricalResidual.frame (z.2.ofLp 1)) (ProblemStatement.coordinateVector 1)

theorem NavierStokes.ActualMeanPotentialRealization.common_potential_units (h : ℝ) (n k : ℕ) : ChartScales.Q n ^ (-(CoordinateAlgebra.A h - 1 / 2)) = (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h k).velocityScale / (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h k).radialScale

theorem NavierStokes.ActualMeanPotentialRealization.bandAngularField_forward (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) (Ψ : Point → ℝ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : PhysicalMeanJetBounds.bandAngularField h n d (CoordinateAlgebra.A h - 1 / 2) Ψ (z.1, CylindricalResidual.chart z.2) = (CylindricalResidual.frame (z.2.ofLp 1)) (componentPotential (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)) Ψ z)

theorem NavierStokes.ActualMeanPotentialRealization.bandAngularField_eq_cartesianPotential {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (h : ℝ) (n d : ℕ) (hd : d ≤ ChartScales.nativeIndex h n) (Ψ : Point → ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) : PhysicalMeanJetBounds.bandAngularField h n d (CoordinateAlgebra.A h - 1 / 2) Ψ w = cartesianPotential a j (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - d)) Ψ w

theorem NavierStokes.ActualMeanPotentialRealization.coherent_angularField_germ {a h : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {N Δ : ℕ} {U : Set (ℝ × ℝ)} (D : PhysicalMeanJetBounds.CoherentFamily h (CoordinateAlgebra.A h - 1 / 2) N Δ U ℝ) (hU : IsOpen U) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hu : (PhysicalMeanJetBounds.graph h n (D.gap n) w).2.1 ∈ U) (hw : w ∈ cartesianDomain a j) : D.angularField =ᶠ[nhds w] cartesianPotential a j (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - D.gap n)) (D.native n)

theorem NavierStokes.ActualMeanPotentialRealization.coherent_angularField_curl {a h : ℝ} (ha : 0 < a) (j : PolarCharts.Index) {N Δ : ℕ} {U : Set (ℝ × ℝ)} (D : PhysicalMeanJetBounds.CoherentFamily h (CoordinateAlgebra.A h - 1 / 2) N Δ U ℝ) (hU : IsOpen U) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hu : (PhysicalMeanJetBounds.graph h n (D.gap n) w).2.1 ∈ U) (hw : w ∈ cartesianDomain a j) (hΨ : ContDiffAt ℝ (↑⊤) (D.native n) (PhysicalMeanJetBounds.graph h n (D.gap n) w)) : SpatialCurl.spatialCurl D.angularField w = have G := PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - D.gap n); (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (meridional G (D.native n))) w

This is a curl identity for the coherent physical field itself, obtained from its proved value coherence and the actual Cartesian derivative.

theorem NavierStokes.ActualMeanPotentialRealization.reconstructStream_curl {a b h ρ : ℝ} (hρ : 0 < ρ) (j : PolarCharts.Index) (U : LocalSignedRequest.SlowRegion (2 * h)) {N Δ : ℕ} (D : PhysicalMeanJetBounds.CoherentFamily h (CoordinateAlgebra.A h) N Δ U.carrier ℝ) (hh : 0 < h) (hh1 : h < 1 / 2) (ha : 0 < a) (hab : a < b) (hf : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (D.native n) (PhysicalMeanDomain.slowDomain U.carrier)) (hs : PhysicalMeanJetBounds.NativeSupport h a b N U.carrier D.native) (n : ℕ) (hn : N ≤ n) {w : ProblemStatement.SpaceTime} (ht : w ∈ PhysicalWaveSum.preterminal) (hu : (PhysicalMeanJetBounds.graph h n (D.gap n) w).2.1 ∈ U.carrier) (hw : w ∈ cartesianDomain ρ j) : have R := D.reconstructStream hh hh1 ha hab ⋯ 1 ⋯ hf hs; SpatialCurl.spatialCurl R.angularField w = have G := PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (ChartScales.nativeIndex h n - D.gap n); (CyclePhysicalPrefixes.polarVelocityMap ρ j) ((CyclePhysicalPrefixes.velocityMap G) (meridional G (R.native n))) w

For the reconstructed mean stream, smoothness of the scalar potential is proved from the supported axial source. No curl identity or smoothness of the output is an input. The radial exponent and frequency are the physical ones.

Finite sums of the actual potentials

theorem NavierStokes.ActualMeanPotentialRealization.cartesianPotential_finset_curl {ι : Type} (S : Finset ι) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) (Ψ : ι → Point → ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (hΨ : ∀ i ∈ S, ContDiffAt ℝ (↑⊤) (Ψ i) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (fun (z : ProblemStatement.SpaceTime) => ∑ i ∈ S, cartesianPotential a j G (Ψ i) z) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (∑ i ∈ S, meridional G (Ψ i))) w

theorem NavierStokes.ActualMeanPotentialRealization.cartesianPotential_add_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) (Ψ Φ : Point → ℝ) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (hΨ : ContDiffAt ℝ (↑⊤) Ψ (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) (hΦ : ContDiffAt ℝ (↑⊤) Φ (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cartesianPotential a j G Ψ + cartesianPotential a j G Φ) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (meridional G Ψ + meridional G Φ)) w

theorem NavierStokes.ActualMeanPotentialRealization.meridionalComponents_updated (m t : MeanIncrementBounds.Triple Point) (n : ℕ) : CyclePhysicalPrefixes.meridionalComponents (MeanIncrementBounds.updated m t) n = CyclePhysicalPrefixes.meridionalComponents m n + CyclePhysicalPrefixes.meridionalComponents t n

theorem NavierStokes.ActualMeanPotentialRealization.temporal_rank_curl {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (r : CorrectionState.RankData (ℝ × ℝ)) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (ut ur : CorrectionState.State Point) (G : ScaledGraph) (hl : 0 < G.radialScale) (n : ℕ) (H : GaugeMatches g c G n) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (ht : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.temporalPotential g h index c ut n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) (hr : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.rankPotential g r c ur n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cartesianPotential a j G (VariableGaugeMean.temporalPotential g h index c ut n) + cartesianPotential a j G (VariableGaugeMean.rankPotential g r c ur n)) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (CyclePhysicalPrefixes.meridionalComponents (VariableGaugeMean.temporalIncrementState g h index axial c ut) n + CyclePhysicalPrefixes.meridionalComponents (VariableGaugeMean.rankIncrementState g r axial c ur) n)) w

The temporal and rank inputs may be successive actual states. Their potentials realize exactly the radial/axial parts of those literal increments.

noncomputable def NavierStokes.ActualMeanPotentialRealization.cycleMeanPotential {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : ProblemStatement.VelocityField

The two scalar streams are evaluated at the actual successive states of the four-stage cycle.

Equations

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

theorem NavierStokes.ActualMeanPotentialRealization.cycleMeanPotential_curl {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) (n : ℕ) (H : GaugeMatches p.gauge c G n) (hax : p.axial = axial) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (ht : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.temporalPotential p.gauge p.timeExponent p.commonIndex c (p.afterSigned v c u) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) (hr : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.rankPotential p.gauge p.rank c (p.afterTemporal v c u) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cycleMeanPotential p v c u a j G n) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (CyclePhysicalPrefixes.meridionalComponents (p.temporalIncrement v c u) n + CyclePhysicalPrefixes.meridionalComponents (p.rankIncrement v c u) n)) w

theorem NavierStokes.ActualMeanPotentialRealization.cycleMeanPotential_smoothAt {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) (n : ℕ) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (ht : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.temporalPotential p.gauge p.timeExponent p.commonIndex c (p.afterSigned v c u) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) (hr : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.rankPotential p.gauge p.rank c (p.afterTemporal v c u) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : ContDiffAt ℝ (↑⊤) (cycleMeanPotential p v c u a j G n) w

The actual initialized mean

noncomputable def NavierStokes.ActualMeanPotentialRealization.initializedMeanPotential {ι : Type} (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (r : CorrectionState.RankData (ℝ × ℝ)) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (labels : ℕ → Finset ι) (pieces : ι → CorrectionInitialization.PrimaryPiece (Point × ℝ)) (baseError : CorrectionState.Oscillation Point) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n : ℕ) : ProblemStatement.VelocityField

Initialized mean potential, constructed using cartesianPotential.

Equations

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

theorem NavierStokes.ActualMeanPotentialRealization.initializedBands_mean {ι : Type} (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (r : CorrectionState.RankData (ℝ × ℝ)) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (labels : ℕ → Finset ι) (pieces : ι → CorrectionInitialization.PrimaryPiece (Point × ℝ)) (baseError : CorrectionState.Oscillation Point) : (CorrectionInitialization.GaugeInitialization.initializedBands g r h index axial c labels pieces baseError).mean = MeanIncrementBounds.updated (VariableGaugeMean.temporalIncrementState g h index axial c (CorrectionInitialization.GaugeInitialization.primaryBands g c labels pieces baseError)) (VariableGaugeMean.rankIncrementState g r axial c (CorrectionInitialization.GaugeInitialization.temporalBands g h index axial c labels pieces baseError))

theorem NavierStokes.ActualMeanPotentialRealization.initializedMeanPotential_curl {ι : Type} (g : VariableGaugeMean.GaugeData (ℝ × ℝ)) (r : CorrectionState.RankData (ℝ × ℝ)) (h : ℝ) (index : ℕ → ℕ) (c : CorrectionState.Context Point) (labels : ℕ → Finset ι) (pieces : ι → CorrectionInitialization.PrimaryPiece (Point × ℝ)) (baseError : CorrectionState.Oscillation Point) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) (n : ℕ) (H : GaugeMatches g c G n) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (ht : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.temporalPotential g h index c (CorrectionInitialization.GaugeInitialization.primaryBands g c labels pieces baseError) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) (hr : ContDiffAt ℝ (↑⊤) (VariableGaugeMean.rankPotential g r c (CorrectionInitialization.GaugeInitialization.temporalBands g h index axial c labels pieces baseError) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (initializedMeanPotential g r h index c labels pieces baseError a j G n) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (CyclePhysicalPrefixes.meridionalComponents (CorrectionInitialization.GaugeInitialization.initializedBands g r h index axial c labels pieces baseError).mean n)) w

The initial mean potential is the sum of the two actual initialized streams. Its curl equals the initialized mean's meridional components.

Finite prefixes of the literal iteration

noncomputable def NavierStokes.ActualMeanPotentialRealization.meanIncrementComponents {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) : CyclePhysicalPrefixes.Components

Mean increment components, constructed using CyclePhysicalPrefixes.meridionalComponents.

Equations

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

theorem NavierStokes.ActualMeanPotentialRealization.meridionalComponents_next {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (n : ℕ) : CyclePhysicalPrefixes.meridionalComponents (p.next v c u).mean n = CyclePhysicalPrefixes.meridionalComponents u.mean n + meanIncrementComponents p v c u n

theorem NavierStokes.ActualMeanPotentialRealization.meridionalComponents_iterate {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context Point) (seed : CorrectionStep.CycleState ι) (n J : ℕ) : CyclePhysicalPrefixes.meridionalComponents (CorrectionStep.CycleState.iterate p c seed J).state.mean n = CyclePhysicalPrefixes.meridionalComponents seed.state.mean n + ∑ k ∈ Finset.range J, meanIncrementComponents (p k) (CorrectionStep.CycleState.iterate p c seed k).coefficients c (CorrectionStep.CycleState.iterate p c seed k).state n

noncomputable def NavierStokes.ActualMeanPotentialRealization.cycleMeanPrefix {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context Point) (seed : CorrectionStep.CycleState ι) (a : ℝ) (j : PolarCharts.Index) (G : ScaledGraph) (n J : ℕ) : ProblemStatement.VelocityField

The finite sum is evaluated on the actual successive cycle states.

Equations

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

theorem NavierStokes.ActualMeanPotentialRealization.cycleMeanPrefix_curl {ι : Type} (p : ℕ → CorrectionStep.CycleParameters ι) (c : CorrectionState.Context Point) (seed : CorrectionStep.CycleState ι) {a : ℝ} (ha : 0 < a) (j : PolarCharts.Index) (G : ScaledGraph) (hl : 0 < G.radialScale) (n J : ℕ) (H : ∀ k < J, GaugeMatches (p k).gauge c G n) (hax : ∀ k < J, (p k).axial = axial) {w : ProblemStatement.SpaceTime} (hw : w ∈ cartesianDomain a j) (ht : ∀ k < J, ContDiffAt ℝ (↑⊤) (VariableGaugeMean.temporalPotential (p k).gauge (p k).timeExponent (p k).commonIndex c ((p k).afterSigned (CorrectionStep.CycleState.iterate p c seed k).coefficients c (CorrectionStep.CycleState.iterate p c seed k).state) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) (hr : ∀ k < J, ContDiffAt ℝ (↑⊤) (VariableGaugeMean.rankPotential (p k).gauge (p k).rank c ((p k).afterTemporal (CorrectionStep.CycleState.iterate p c seed k).coefficients c (CorrectionStep.CycleState.iterate p c seed k).state) n) (chartPoint G (PhysicalCurlCovariance.polarCoordinates a j w))) : SpatialCurl.spatialCurl (cycleMeanPrefix p c seed a j G n J) w = (CyclePhysicalPrefixes.polarVelocityMap a j) ((CyclePhysicalPrefixes.velocityMap G) (CyclePhysicalPrefixes.meridionalComponents (CorrectionStep.CycleState.iterate p c seed J).state.mean n - CyclePhysicalPrefixes.meridionalComponents seed.state.mean n)) w