Physical fields of the actual current-band particular solve

The copy solve in this file is evaluated at the current band. The choice of a polar angle depends only on the Cartesian point and is independent of the band. No regularity of a fixed-reference continuation is used.

@[reducible, inline]

abbrev NavierStokes.ActualCurrentParticularPhysical.Label (B N0 : ℕ) : Type

Label: an abbreviation for ActualParticularStageControls.Label B N0.

Equations

• NavierStokes.ActualCurrentParticularPhysical.Label B N0 = NavierStokes.ActualParticularStageControls.Label B N0

@[reducible, inline]

abbrev NavierStokes.ActualCurrentParticularPhysical.Native : Type

Native: an abbreviation for PhysicalParticularWave.WaveSpace.

Equations

• NavierStokes.ActualCurrentParticularPhysical.Native = NavierStokes.PhysicalParticularWave.WaveSpace

noncomputable def NavierStokes.ActualCurrentParticularPhysical.copyData {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) : PeriodizedWaveBounds.CopyData ((ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) TorusInverse.Frequency

The literal current solve, with the canonical geometry already fixed.

Equations

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

theorem NavierStokes.ActualCurrentParticularPhysical.copyData_eq_actual {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) : copyData x l j = ActualParticularCoherence.copyData x l j

noncomputable def NavierStokes.ActualCurrentParticularPhysical.nativePotential {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : Native → HarmonicCalculus.ComplexVector

The current common coefficient includes every localized copy cutoff.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.nativePressure {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : Native → ℂ

Native pressure, given by mode ((copyData x l j).background.frequency n) ((copyData x l j).background.phase n) ((copyData x l j).common.pressure n).

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.angle (w : ProblemStatement.SpaceTime) : ℝ

A pointwise polar angle choice. Its apparent cuts disappear from periodic physical fields by the chart-agreement theorem below.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.cylinderPoint (w : ProblemStatement.SpaceTime) : ProblemStatement.SpaceTime

Cylinder point, given by (w.1, AxisymmetricResidual.pack (PolarCharts.radius (PhysicalGraphBounds.radialProjection w)) (angle w) (w.2 2)).

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.nativePoint (n : ℕ) (w : ProblemStatement.SpaceTime) : Native

This is a current-band map; it does not use the reference band of a label.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.cylindricalPotential {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (z : ProblemStatement.SpaceTime) : HarmonicCalculus.ComplexVector

Cylindrical potential as an element of ComplexVector.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.cylindricalPressure {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (z : ProblemStatement.SpaceTime) : ℝ

Cylindrical pressure as an element of ℝ.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.localPotentialMode {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (w : ProblemStatement.SpaceTime) : ProblemStatement.Space

A single actual harmonic, in Cartesian coordinates.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.localPressureMode {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (w : ProblemStatement.SpaceTime) : ℝ

Local pressure mode, given by cylindricalPressure x l j n (cylinderPoint w).

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.localPotential {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (n : ℕ) : ProblemStatement.VelocityField

The actual finite active-label and nonzero-harmonic sum at band n.

Equations

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

noncomputable def NavierStokes.ActualCurrentParticularPhysical.localPressure {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (n : ℕ) : ProblemStatement.PressureField

Local pressure, defined pointwise by ∑ l ∈ x.coefficients.labels n, ∑ j ∈ ParticularWaveAssembly.modes x.coefficients.residualBand, localPressureMode x l j n w.

Equations

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

theorem NavierStokes.ActualCurrentParticularPhysical.nativePotential_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : nativePotential x l j n = CurlClassBounds.vectorPotential ((copyData x l j).background.frequency n) ((copyData x l j).background.radius n) (ActualParticularStageControls.directions.radialField n) (fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => ActualParticularStageControls.directions.angular) (ActualParticularStageControls.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n) ((copyData x l j).background.phase n) ((copyData x l j).common.amplitude n)

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_eq {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (w : ProblemStatement.SpaceTime) : localPotentialMode x l j n w = ChartScales.Q n ^ (-CorrectionInitialization.ActualPrimary.h) • PhysicalCurlCovariance.realVector ((CartesianCopySource.rotationMap (PhysicalGraphBounds.radialProjection w)) (nativePotential x l j n (nativePoint n w)))

The polar angle is only a coordinate choice

theorem NavierStokes.ActualCurrentParticularPhysical.chosenChart_valid {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : PhysicalGraphBounds.radialProjection w ∈ PolarCharts.chartDomain ‖PhysicalGraphBounds.radialProjection w‖ (PhysicalWaveSum.chooseChart ‖PhysicalGraphBounds.radialProjection w‖ (PhysicalGraphBounds.radialProjection w))

theorem NavierStokes.ActualCurrentParticularPhysical.polar_angle {w : ProblemStatement.SpaceTime} (hw : PhysicalGraphBounds.radialProjection w ≠ 0) : PolarCharts.polar (PolarCharts.radius (PhysicalGraphBounds.radialProjection w), angle w) = PhysicalGraphBounds.radialProjection w

theorem NavierStokes.ActualCurrentParticularPhysical.angle_chart_cos_sin {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : Real.cos (angle w) = Real.cos (PhysicalCurlCovariance.polarInput a i w).2 ∧ Real.sin (angle w) = Real.sin (PhysicalCurlCovariance.polarInput a i w).2

theorem NavierStokes.ActualCurrentParticularPhysical.periodic_eq_of_cos_sin {E : Type u_1} {f : ℝ → E} (hf : Function.Periodic f (2 * Real.pi)) {a b : ℝ} (hc : Real.cos a = Real.cos b) (hs : Real.sin a = Real.sin b) : f a = f b

theorem NavierStokes.ActualCurrentParticularPhysical.periodic_cylinderPoint_eq_chart {E : Type u_1} {f : ProblemStatement.SpaceTime → E} (hf : ∀ (t r z : ℝ), Function.Periodic (fun (θ : ℝ) => f (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : f (cylinderPoint w) = f (PhysicalCurlCovariance.polarCoordinates a i w)

theorem NavierStokes.ActualCurrentParticularPhysical.rotation_realVector_eq_frame {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (v : HarmonicCalculus.ComplexVector) : PhysicalCurlCovariance.realVector ((CartesianCopySource.rotationMap (PhysicalGraphBounds.radialProjection w)) v) = (CylindricalResidual.frame (PhysicalCurlCovariance.polarInput a i w).2) (PhysicalCurlCovariance.realVector v)

The actual current coefficients have integer angular frequency

theorem NavierStokes.ActualCurrentParticularPhysical.nativePotential_fullTurn {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) (z : Native) : nativePotential x l j n (z + (2 * Real.pi) • ActualParticularStageControls.directions.angular) = nativePotential x l j n z

theorem NavierStokes.ActualCurrentParticularPhysical.nativePressure_fullTurn {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) (z : Native) : nativePressure x l j n (z + (2 * Real.pi) • ActualParticularStageControls.directions.angular) = nativePressure x l j n z

theorem NavierStokes.ActualCurrentParticularPhysical.cylindricalPotential_periodic {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) (t r z : ℝ) : Function.Periodic (fun (θ : ℝ) => cylindricalPotential x l j n (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)

theorem NavierStokes.ActualCurrentParticularPhysical.cylindricalPressure_periodic {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) (t r z : ℝ) : Function.Periodic (fun (θ : ℝ) => cylindricalPressure x l j n (t, AxisymmetricResidual.pack r θ z)) (2 * Real.pi)

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_eq_chart {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : localPotentialMode x l j n w = PhysicalCurlCovariance.cartesianPotential a i (cylindricalPotential x l j n) w

theorem NavierStokes.ActualCurrentParticularPhysical.localPressureMode_eq_chart {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : localPressureMode x l j n w = cylindricalPressure x l j n (PhysicalCurlCovariance.polarCoordinates a i w)

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_germ_chart {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : localPotentialMode x l j n =ᶠ[nhds w] PhysicalCurlCovariance.cartesianPotential a i (cylindricalPotential x l j n)

theorem NavierStokes.ActualCurrentParticularPhysical.localPressureMode_germ_chart {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) : localPressureMode x l j n =ᶠ[nhds w] fun (v : ProblemStatement.SpaceTime) => cylindricalPressure x l j n (PhysicalCurlCovariance.polarCoordinates a i v)

Native smoothness and its exact physical transport

noncomputable def NavierStokes.ActualCurrentParticularPhysical.nativeDomain : Set Native

Native domain, given by ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion.

Equations

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

theorem NavierStokes.ActualCurrentParticularPhysical.nativeDomain_open : IsOpen nativeDomain

def NavierStokes.ActualCurrentParticularPhysical.RawBoundaryZero {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) : Prop

The endpoint condition concerns actual Volterra output values. The source-continuity and path lemmas provide it for the constructed cycle.

Equations

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

theorem NavierStokes.ActualCurrentParticularPhysical.nativePotential_contDiffOn {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hphase : (copyData x l j).background.phase = (ActualParticularStageControls.background l).phase) {α : ℝ} (ha : WeightedClasses.MemClass ActualWaveRegularityData.particularFullStrip (fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(ActualWaveRegularityData.particularFullStrip.zeta z)) α (copyData x l j).common.amplitude) (hz : RawBoundaryZero x l j) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePotential x l j n) nativeDomain

theorem NavierStokes.ActualCurrentParticularPhysical.nativePressure_re_contDiffOn {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hphase : (copyData x l j).background.phase = (ActualParticularStageControls.background l).phase) {β : ℝ} (hp : WeightedClasses.MemClass ActualWaveRegularityData.particularFullStrip (fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(ActualWaveRegularityData.particularFullStrip.zeta z)) β (copyData x l j).common.pressure) (hz : RawBoundaryZero x l j) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : Native) => (nativePressure x l j n z).re) nativeDomain

theorem NavierStokes.ActualCurrentParticularPhysical.nativeMap_contDiffAt (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) : ContDiffAt ℝ (↑⊤) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)) z

theorem NavierStokes.ActualCurrentParticularPhysical.cylindricalPotential_contDiffAt_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hP : ContDiffAt ℝ (↑⊤) (nativePotential x l j n) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z)) : ContDiffAt ℝ (↑⊤) (cylindricalPotential x l j n) z

theorem NavierStokes.ActualCurrentParticularPhysical.cylindricalPressure_contDiffAt_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hP : ContDiffAt ℝ (↑⊤) (fun (v : Native) => (nativePressure x l j n v).re) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z)) : ContDiffAt ℝ (↑⊤) (cylindricalPressure x l j n) z

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_contDiffAt_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hP : ContDiffAt ℝ (↑⊤) (nativePotential x l j n) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (PhysicalCurlCovariance.polarCoordinates a i w))) : ContDiffAt ℝ (↑⊤) (localPotentialMode x l j n) w

theorem NavierStokes.ActualCurrentParticularPhysical.localPressureMode_contDiffAt_of_native {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hP : ContDiffAt ℝ (↑⊤) (fun (v : Native) => (nativePressure x l j n v).re) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (PhysicalCurlCovariance.polarCoordinates a i w))) : ContDiffAt ℝ (↑⊤) (localPressureMode x l j n) w

theorem NavierStokes.ActualCurrentParticularPhysical.copyData_phase {B N0 : ℕ} {x : CorrectionStep.CycleState (Label B N0)} (hx : ActualParticularStageControls.PreservesCarriers x) (l : Label B N0) (j : ℤ) : (copyData x l j).background.phase = (ActualParticularStageControls.background l).phase

theorem NavierStokes.ActualCurrentParticularPhysical.native_smooth_of_current_source {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : Label B N0) (hz : RawBoundaryZero x l j) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePotential x l j n) nativeDomain ∧ ContDiffOn ℝ (↑⊤) (fun (z : Native) => (nativePressure x l j n z).re) nativeDomain

The native smoothness hypotheses are consequences of the actual source class and support theorem; no physical jet estimate is assumed.

theorem NavierStokes.ActualCurrentParticularPhysical.nativeMap_polar_mem_iff (n : ℕ) (a : ℝ) (i : PolarCharts.Index) (w : ProblemStatement.SpaceTime) : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) (PhysicalCurlCovariance.polarCoordinates a i w) ∈ nativeDomain ↔ nativePoint n w ∈ nativeDomain

theorem NavierStokes.ActualCurrentParticularPhysical.localModes_contDiffAt_of_current_source {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : Label B N0) (hz : RawBoundaryZero x l j) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hm : nativePoint n w ∈ nativeDomain) : ContDiffAt ℝ (↑⊤) (localPotentialMode x l j n) w ∧ ContDiffAt ℝ (↑⊤) (localPressureMode x l j n) w

The literal cycle input discharges the raw endpoint condition.

theorem NavierStokes.ActualCurrentParticularPhysical.copyData_particularState {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualInitialization.Index B N0)) (l : ActualInitialization.Index B N0) (j : ℤ) : copyData (ActualCycleParameters.particularState x) (l.2, l.1) j = ActualParticularCycleData.nativeData x l j

theorem NavierStokes.ActualCurrentParticularPhysical.rawBoundaryZero_of_invariant {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (l : ActualInitialization.Index B N0) (j : ℤ) : RawBoundaryZero (ActualCycleParameters.particularState x) (l.2, l.1) j

theorem NavierStokes.ActualCurrentParticularPhysical.native_smooth_of_invariant {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : ActualInitialization.Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (nativePotential (ActualCycleParameters.particularState x) (l.2, l.1) j n) nativeDomain ∧ ContDiffOn ℝ (↑⊤) (fun (z : Native) => (nativePressure (ActualCycleParameters.particularState x) (l.2, l.1) j n z).re) nativeDomain

theorem NavierStokes.ActualCurrentParticularPhysical.localModes_contDiffAt_of_invariant {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : ActualInitialization.Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hm : nativePoint n w ∈ nativeDomain) : ContDiffAt ℝ (↑⊤) (localPotentialMode (ActualCycleParameters.particularState x) (l.2, l.1) j n) w ∧ ContDiffAt ℝ (↑⊤) (localPressureMode (ActualCycleParameters.particularState x) (l.2, l.1) j n) w

theorem NavierStokes.ActualCurrentParticularPhysical.localFields_contDiffAt_of_invariant {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {w : ProblemStatement.SpaceTime} (hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a i) (hm : nativePoint n w ∈ nativeDomain) : ContDiffAt ℝ (↑⊤) (localPotential (ActualCycleParameters.particularState x) n) w ∧ ContDiffAt ℝ (↑⊤) (localPressure (ActualCycleParameters.particularState x) n) w

The complete corrected coefficient is the actual native curl

noncomputable def NavierStokes.ActualCurrentParticularPhysical.nativeVelocity {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) : Native → HarmonicCalculus.ComplexVector

Native velocity, constructed using vectorMode.

Equations

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

theorem NavierStokes.ActualCurrentParticularPhysical.nativeStrip_mem {z : Native} (hz : z ∈ nativeDomain) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∈ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain

theorem NavierStokes.ActualCurrentParticularPhysical.common_tangent_on_strip {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (hx : ActualParticularStageControls.PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : Label B N0) (n : ℕ) {z : Native} (hz : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain) : HarmonicCalculus.normalDot ((copyData x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z) ((copyData x l j).common.amplitude n z) = 0

theorem NavierStokes.ActualCurrentParticularPhysical.native_normal_ne {B N0 : ℕ} {x : CorrectionStep.CycleState (Label B N0)} (hx : ActualParticularStageControls.PreservesCarriers x) (l : Label B N0) (j : ℤ) (n : ℕ) {z : Native} (hz : z ∈ ActualWaveRegularityData.particularPositive) : (copyData x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z ≠ 0

theorem NavierStokes.ActualCurrentParticularPhysical.nativePotential_curl_of_invariant {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : ActualInitialization.Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) {z : Native} (hz : z ∈ ActualWaveRegularityData.particularPositive) : CurlClassBounds.cylindricalCurl ((copyData (ActualCycleParameters.particularState x) (l.2, l.1) j).background.radius n) (ActualParticularStageControls.directions.radialField n) (fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => ActualParticularStageControls.directions.angular) (ActualParticularStageControls.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n) (nativePotential (ActualCycleParameters.particularState x) (l.2, l.1) j n) z = nativeVelocity (ActualCycleParameters.particularState x) (l.2, l.1) j n z

The actual native curl identity includes the radial faces: zero raw values there give tangency, while the weighted extension supplies the actual derivatives of the normal coefficient.

Curl in genuine Cartesian coordinates

theorem NavierStokes.ActualCurrentParticularPhysical.nativeCurl_reindex {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (n : ℕ) (z : PhysicalResidualBridge.Cylinder) : CurlClassBounds.cylindricalCurl PhysicalResidualBridge.ScaledGraph.radius (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).radial PhysicalResidualBridge.ScaledGraph.angular (PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)).axial (fun (y : PhysicalResidualBridge.Cylinder) => nativePotential x l j n (PhysicalParticularWave.waveEquiv y)) z = CurlClassBounds.cylindricalCurl ((copyData x l j).background.radius n) (ActualParticularStageControls.directions.radialField n) (fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => ActualParticularStageControls.directions.angular) (ActualParticularStageControls.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n) (nativePotential x l j n) (PhysicalParticularWave.waveEquiv z)

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_forward_germ {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a i) : (fun (w : ProblemStatement.SpaceTime) => localPotentialMode x l j n (w.1, CylindricalResidual.chart w.2)) =ᶠ[nhds z] fun (w : ProblemStatement.SpaceTime) => (CylindricalResidual.frame (w.2.ofLp 1)) (PhysicalCurlCovariance.realVector (cylindricalPotential x l j n w))

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_curl_transport {B N0 : ℕ} (x : CorrectionStep.CycleState (Label B N0)) (l : Label B N0) (j : ℤ) (hf : ∀ (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a i) (hP : ContDiffAt ℝ (↑⊤) (nativePotential x l j n) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z)) (k : Fin 3) : ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (localPotentialMode x l j n) (z.1, CylindricalResidual.chart z.2))).ofLp k = ChartScales.Q n ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * (CurlClassBounds.cylindricalCurl ((copyData x l j).background.radius n) (ActualParticularStageControls.directions.radialField n) (fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => ActualParticularStageControls.directions.angular) (ActualParticularStageControls.directions.axialField (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) n) (nativePotential x l j n) (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z) k).re

theorem NavierStokes.ActualCurrentParticularPhysical.nativeMap_mem_positive (n : ℕ) {z : ProblemStatement.SpaceTime} (hr : 0 < z.2.ofLp 0) (hz : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z ∈ nativeDomain) : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z ∈ ActualWaveRegularityData.particularPositive

theorem NavierStokes.ActualCurrentParticularPhysical.localPotentialMode_curl_of_invariant {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualInitialization.Index B N0)} {σ : ℝ} (H : ActualParticularCycleData.Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : ActualInitialization.Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) {a : ℝ} (ha : 0 < a) (i : PolarCharts.Index) {z : ProblemStatement.SpaceTime} (hz : z ∈ PhysicalCurlCovariance.validCylindrical a i) (hm : PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z ∈ nativeDomain) (k : Fin 3) : ((CylindricalResidual.frame (-z.2.ofLp 1)) (SpatialCurl.spatialCurl (localPotentialMode (ActualCycleParameters.particularState x) (l.2, l.1) j n) (z.1, CylindricalResidual.chart z.2))).ofLp k = ChartScales.Q n ^ (-CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) * (nativeVelocity (ActualCycleParameters.particularState x) (l.2, l.1) j n (PhysicalParticularWave.nativeMap CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n) z) k).re