The curl of the actual current signed potential

The native equation is proved from the actual signed tangency and cutoff construction. The weighted amplitude bound supplies its smooth extension across the radial edges. All physical statements use the current band.

@[reducible, inline]

abbrev NavierStokes.CurrentSignedCurl.Point : Type

Point: an abbreviation for ActualSignedCoherence.Point.

Equations

• NavierStokes.CurrentSignedCurl.Point = NavierStokes.ActualSignedCoherence.Point

@[reducible, inline]

abbrev NavierStokes.CurrentSignedCurl.FullPoint : Type

Full point: an abbreviation for ActualSignedCoherence.FullPoint.

Equations

• NavierStokes.CurrentSignedCurl.FullPoint = NavierStokes.ActualSignedCoherence.FullPoint

@[reducible, inline]

abbrev NavierStokes.CurrentSignedCurl.AmplitudeBound {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (α : ℝ) : Prop

The actual weighted raw-amplitude estimate; no curl equation is included.

Equations

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

theorem NavierStokes.CurrentSignedCurl.amplitudeBound_of_mean {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (α : ℝ) (H : MeanStateRegularity.PrimitiveData ActualInitialization.geometry.region ActualInitialization.geometry.patch.a ActualInitialization.geometry.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) u) (hfixed : VariableGaugeMean.reconstructState ActualInitialization.geometry.gauge (CorrectionInitialization.ActualPrimary.commonContext B) u = u) (hθ : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))) (hz : WeightedClasses.MeanClass ActualInitialization.geometry.strip α (u.axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))) : AmplitudeBound l u (α - 1 / 2)

Primitive state regularity and actual mean residual bounds supply the amplitude hypothesis used below, for the same current request and label.

theorem NavierStokes.CurrentSignedCurl.common_tangent {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) {x : FullPoint} (hx : x ∈ ActualWaveRegularityData.positiveDomain) : HarmonicCalculus.normalDot ((ActualSignedStageControls.parameters l).base.normal ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B) n x) ((ActualSignedCoherence.copies l u).common.amplitude n x) = 0

Actual tangency extends to the entire positive native domain: outside the strict active annulus the common raw amplitude is exactly zero.

theorem NavierStokes.CurrentSignedCurl.potential_smooth {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (ha : AmplitudeBound l u α) (n : ℕ) : ContDiffOn ℝ (↑⊤) (ActualSignedPotentialCoherence.potential l u n) ActualWaveRegularityData.positiveDomain

Smoothness of the literal current potential on positive native radii.

theorem NavierStokes.CurrentSignedCurl.native_curl {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (ha : AmplitudeBound l u α) (n : ℕ) {x : FullPoint} (hx : x ∈ ActualWaveRegularityData.positiveDomain) : CurlClassBounds.cylindricalCurl ((ActualSignedStageControls.parameters l).base.radius n) ((ActualSignedStageControls.directions B).radialField n) (fun (x : ActualSignedStageControls.Point × ℝ) => (ActualSignedStageControls.directions B).angular) ((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n) (ActualSignedPotentialCoherence.potential l u n) x = HarmonicCalculus.vectorMode ((ActualSignedStageControls.parameters l).base.frequency n) ((ActualSignedStageControls.parameters l).base.phase n) (((ActualSignedCoherence.copies l u).commonCorrected ActualSignedStageControls.fullStrip (ActualSignedStageControls.directions B)).amplitude n) x

The real current cylindrical curl is the stored exact signed block.

noncomputable def NavierStokes.CurrentSignedCurl.currentPotential {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (a : ℝ) (i : PolarCharts.Index) : ProblemStatement.VelocityField

The actual current potential expressed in the selected Cartesian polar chart.

Equations

• NavierStokes.CurrentSignedCurl.currentPotential l u n a i = NavierStokes.PhysicalCurlCovariance.cartesianPotential a i (NavierStokes.ActualSignedPotentialCoherence.cylindricalPotential l u n)

theorem NavierStokes.CurrentSignedCurl.nativePoint_mem (n : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.source n) : ActualSignedPotentialCoherence.nativePoint n z ∈ ActualWaveRegularityData.positiveDomain

theorem NavierStokes.CurrentSignedCurl.cylindricalPotential_smoothAt {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (ha : AmplitudeBound l u α) (n : ℕ) {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.source n) : ContDiffAt ℝ (↑⊤) (ActualSignedPotentialCoherence.cylindricalPotential l u n) z

theorem NavierStokes.CurrentSignedCurl.currentPotential_smoothAt {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (hamp : AmplitudeBound l u α) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {qbig : ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : ContDiffAt ℝ (↑⊤) (currentPotential l u n a i) z

theorem NavierStokes.CurrentSignedCurl.reindexed_curl {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (y : FullPoint) : CurlClassBounds.cylindricalCurl PhysicalResidualBridge.ScaledGraph.radius (ActualCycleResidualBounds.actualBandGraph n).radial PhysicalResidualBridge.ScaledGraph.angular (ActualCycleResidualBounds.actualBandGraph n).axial (fun (x : PhysicalResidualBridge.Cylinder) => ActualSignedPotentialCoherence.potential l u n (PhysicalResidualTZ.swapCylinder x)) y = CurlClassBounds.cylindricalCurl ((ActualSignedStageControls.parameters l).base.radius n) ((ActualSignedStageControls.directions B).radialField n) (fun (x : ActualSignedStageControls.Point × ℝ) => (ActualSignedStageControls.directions B).angular) ((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n) (ActualSignedPotentialCoherence.potential l u n) (PhysicalResidualTZ.swapCylinder y)

Swapping slow coordinates changes the input order, not the vector components.

theorem NavierStokes.CurrentSignedCurl.native_curl_real {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (ha : AmplitudeBound l u α) (n : ℕ) {x : FullPoint} (hx : x ∈ ActualWaveRegularityData.positiveDomain) (j : Fin 3) : (CurlClassBounds.cylindricalCurl ((ActualSignedStageControls.parameters l).base.radius n) ((ActualSignedStageControls.directions B).radialField n) (fun (x : ActualSignedStageControls.Point × ℝ) => (ActualSignedStageControls.directions B).angular) ((ActualSignedStageControls.directions B).axialField ActualSignedStageControls.fullStrip n) (ActualSignedPotentialCoherence.potential l u n) x j).re = ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n x j

theorem NavierStokes.CurrentSignedCurl.currentPotential_curl_forward {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (hamp : AmplitudeBound l u α) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hc : z ∈ PhysicalCurlCovariance.validCylindrical a i) (hz : z ∈ ActualPhysicalPrefixFields.source n) : SpatialCurl.spatialCurl (currentPotential l u n a i) (z.1, CylindricalResidual.chart z.2) = (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) (((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n)) (z.1, CylindricalResidual.chart z.2)

At a valid current cylindrical chart, the constructed Cartesian potential has exactly the physical signed velocity as its curl.

theorem NavierStokes.CurrentSignedCurl.currentPotential_curl {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) {α : ℝ} (hamp : AmplitudeBound l u α) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {qbig : ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : SpatialCurl.spatialCurl (currentPotential l u n a i) z = (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) (((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n)) z

The current-band curl identity on the actual Cartesian chart domain.

theorem NavierStokes.CurrentSignedCurl.currentPotential_sum_curl {B N0 : ℕ} (s : Finset (ActualSignedCoherence.SignedLabel B N0)) (u : CorrectionState.State Point) {α : ℝ} (hamp : ∀ l ∈ s, AmplitudeBound l u α) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {qbig : ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : SpatialCurl.spatialCurl (fun (w : ProblemStatement.SpaceTime) => ∑ l ∈ s, currentPotential l u n a i w) z = ∑ l ∈ s, (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) (((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n)) z

Finite label sums use actual differentiable potentials before taking curl.

theorem NavierStokes.CurrentSignedCurl.currentPotential_sum_curl_map {B N0 : ℕ} (s : Finset (ActualSignedCoherence.SignedLabel B N0)) (u : CorrectionState.State Point) {α : ℝ} (hamp : ∀ l ∈ s, AmplitudeBound l u α) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {qbig : ℝ} {z : ProblemStatement.SpaceTime} (hz : z ∈ ActualPhysicalPrefixFields.cartesianChartDomain qbig n a i) : SpatialCurl.spatialCurl (fun (w : ProblemStatement.SpaceTime) => ∑ l ∈ s, currentPotential l u n a i w) z = (CyclePhysicalPrefixes.polarVelocityMap a i) ((CyclePhysicalPrefixes.velocityMap (ActualCycleResidualBounds.actualBandGraph n)) (∑ l ∈ s, ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillation n)) z

Integer angular periodicity and independence of the inverse chart

theorem NavierStokes.CurrentSignedCurl.potential_periodic {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (x : Point) : Function.Periodic (fun (θ : ℝ) => ActualSignedPotentialCoherence.potential l u n (x, θ)) (2 * Real.pi)

theorem NavierStokes.CurrentSignedCurl.nativePoint_angle (n : ℕ) (t r θ z : ℝ) : ActualSignedPotentialCoherence.nativePoint n (t, AxisymmetricResidual.pack r θ z) = ((ActualSignedPotentialCoherence.nativePoint n (t, AxisymmetricResidual.pack r 0 z)).1, θ)

theorem NavierStokes.CurrentSignedCurl.cylindricalPotential_periodic {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (t r z : ℝ) : Function.Periodic (fun (θ : ℝ) => ActualSignedPotentialCoherence.cylindricalPotential l u n (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)

theorem NavierStokes.CurrentSignedCurl.cartesianPotential_overlap_radius {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (i j : PolarCharts.Index) (F : ProblemStatement.SpaceTime → HarmonicCalculus.ComplexVector) (hF : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => F (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {z : ProblemStatement.SpaceTime} (hi : z ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hj : z ∈ ActualMeanPotentialRealization.cartesianDomain b j) : PhysicalCurlCovariance.cartesianPotential a i F z = PhysicalCurlCovariance.cartesianPotential b j F z

A periodic cylindrical field agrees in inverse charts with independently chosen positive smoothing radii.

theorem NavierStokes.CurrentSignedCurl.currentPotential_overlap {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (i j : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hi : z ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hj : z ∈ ActualMeanPotentialRealization.cartesianDomain b j) : currentPotential l u n a i z = currentPotential l u n b j z

theorem NavierStokes.CurrentSignedCurl.currentPotential_overlap_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (i j : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hi : z ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hj : z ∈ ActualMeanPotentialRealization.cartesianDomain b j) : currentPotential l u n a i =ᶠ[nhds z] currentPotential l u n b j

The actual pressure mode

theorem NavierStokes.CurrentSignedCurl.pressureMode_eq_exact {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (x : FullPoint) : (ActualSignedPotentialCoherence.pressureMode l u n x).re = ((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillatoryPressure n x

noncomputable def NavierStokes.CurrentSignedCurl.currentPressure {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (a : ℝ) (i : PolarCharts.Index) : ProblemStatement.PressureField

Current pressure, defined pointwise by (cylindricalPressureMode l u n (PhysicalCurlCovariance.polarCoordinates a i z)).re.

Equations

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

theorem NavierStokes.CurrentSignedCurl.currentPressure_eq {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (a : ℝ) (i : PolarCharts.Index) : currentPressure l u n a i = (CyclePhysicalPrefixes.polarPressureMap a i) ((CyclePhysicalPrefixes.pressureMap (ActualCycleResidualBounds.actualBandGraph n)) (((ActualSignedStageControls.parameters l).exactBlock ActualInitialization.geometry.strip (ActualSignedCoherence.request B u)).oscillatoryPressure n))

theorem NavierStokes.CurrentSignedCurl.realPressureMode_periodic {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (x : Point) : Function.Periodic (fun (θ : ℝ) => (ActualSignedPotentialCoherence.pressureMode l u n (x, θ)).re) (2 * Real.pi)

theorem NavierStokes.CurrentSignedCurl.realCylindricalPressure_periodic {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) (t r z : ℝ) : Function.Periodic (fun (θ : ℝ) => (ActualSignedPotentialCoherence.cylindricalPressureMode l u n (t, AxisymmetricResidual.pack r θ z)).re) (2 * Real.pi)

theorem NavierStokes.CurrentSignedCurl.polarScalar_overlap_radius {E : Type u_1} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (i j : PolarCharts.Index) (F : ProblemStatement.SpaceTime → E) (hF : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => F (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {z : ProblemStatement.SpaceTime} (hi : z ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hj : z ∈ ActualMeanPotentialRealization.cartesianDomain b j) : F (PhysicalCurlCovariance.polarCoordinates a i z) = F (PhysicalCurlCovariance.polarCoordinates b j z)

theorem NavierStokes.CurrentSignedCurl.currentPressure_overlap {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (i j : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hi : z ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hj : z ∈ ActualMeanPotentialRealization.cartesianDomain b j) : currentPressure l u n a i z = currentPressure l u n b j z

theorem NavierStokes.CurrentSignedCurl.currentPressure_overlap_germ {B N0 : ℕ} (l : ActualSignedCoherence.SignedLabel B N0) (u : CorrectionState.State Point) (n : ℕ) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (i j : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hi : z ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hj : z ∈ ActualMeanPotentialRealization.cartesianDomain b j) : currentPressure l u n a i =ᶠ[nhds z] currentPressure l u n b j