Particular-wave data for the actual correction cycle

The record below names the particular half of the cycle's analytic data. Its producer uses the literal fixed-parameter solve and incoming invariant.

Exact dynamics of the actual particular correction

The current harmonic residual is solved on the common cover. Geometry and carrier identities are proved for the actual selected primary labels; quantitative controls are supplied by ActualParticularStageControls.

Actual harmonic divergence under a change of product association

The same complex single-mode field is pulled back along the cylinder isometry. Its genuine cylindrical divergence is preserved, including the transported radial and axial directions. No new divergence premise is needed for the associated particular-solver coordinates.

theorem NavierStokes.ModeSolenoidalReindex.amplitude_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock E) (j : ℤ) (n : ℕ) : HarmonicWaveInteraction.amplitude (StateReindex.block e b) j n = fun (x : D) => HarmonicWaveInteraction.amplitude b j n (e x)

theorem NavierStokes.ModeSolenoidalReindex.singleMode_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (b : CorrectionState.HarmonicBlock E) (j : ℤ) (n : ℕ) : HarmonicWaveInteraction.singleMode (StateReindex.block e b) j n = fun (x : D × ℝ) => HarmonicWaveInteraction.singleMode b j n ((StateReindex.cylinder e) x)

theorem NavierStokes.ModeSolenoidalReindex.liftDirection_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (V : E → E) : HarmonicResidual.liftDirection (StateReindex.vector e V) = StateReindex.vector (StateReindex.cylinder e) (HarmonicResidual.liftDirection V)

theorem NavierStokes.ModeSolenoidalReindex.angularDirection_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) : StateReindex.vector (StateReindex.cylinder e) HarmonicResidual.angularDirection = HarmonicResidual.angularDirection

theorem NavierStokes.ModeSolenoidalReindex.cylindricalDivergence_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (R : E → ℝ) (Vr Vθ Vz : E → E) (a : E → HarmonicCalculus.ComplexVector) (x : D) : HarmonicCalculus.cylindricalDivergence (fun (y : D) => R (e y)) (StateReindex.vector e Vr) (StateReindex.vector e Vθ) (StateReindex.vector e Vz) (fun (y : D) => a (e y)) x = HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz a (e x)

theorem NavierStokes.ModeSolenoidalReindex.singleMode_divergence_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (b : CorrectionState.HarmonicBlock E) (j : ℤ) (n : ℕ) (p : D × ℝ) : HarmonicCalculus.cylindricalDivergence (fun (q : D × ℝ) => (StateReindex.context e c).operators.radius q.1) (HarmonicResidual.liftDirection (HarmonicResidual.contextFrame (StateReindex.context e c) n).radial) HarmonicResidual.angularDirection (HarmonicResidual.liftDirection (HarmonicResidual.contextFrame (StateReindex.context e c) n).axial) (HarmonicWaveInteraction.singleMode (StateReindex.block e b) j n) p = HarmonicCalculus.cylindricalDivergence (fun (q : E × ℝ) => c.operators.radius q.1) (HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).radial) HarmonicResidual.angularDirection (HarmonicResidual.liftDirection (HarmonicResidual.contextFrame c n).axial) (HarmonicWaveInteraction.singleMode b j n) ((StateReindex.cylinder e) p)

theorem NavierStokes.ModeSolenoidalReindex.modeSolenoidal_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) {s : WeightedClasses.StripData E} {c : CorrectionState.Context E} {b : CorrectionState.HarmonicBlock E} (hb : HarmonicWaveInteraction.ModeSolenoidal s c b) : HarmonicWaveInteraction.ModeSolenoidal (ParticularWaveBounds.reindexStrip e s) (StateReindex.context e c) (StateReindex.block e b)

noncomputable def NavierStokes.ActualParticularDynamics.primaryCarrier {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Primary carrier as an element of HarmonicBlock CyclePoint.

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualParticularDynamics.PreservesCarriers {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) : Prop

Preserves carriers: an abbreviation for ∀ l, SameCarrier (x.coefficients.blocks l) (primaryCarrier l).

Equations

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

theorem NavierStokes.ActualParticularDynamics.carrier_frequency {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (n : ℕ) : (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

@[simp]

theorem NavierStokes.ActualParticularDynamics.nativeToFull_apply (z : ActualParticularStageControls.Native) : ActualParticularStageControls.nativeToFull z = ((z.1.1.1, z.1.1.2, z.2), z.1.2)

noncomputable def NavierStokes.ActualParticularDynamics.referencePoint {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (z : ActualParticularStageControls.Native) : ActualSignedGeometry.Native

Reference point as an element of ActualSignedGeometry.Native.

Equations

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

theorem NavierStokes.ActualParticularDynamics.referencePoint_eq_copy {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (z : ActualParticularStageControls.Native) : referencePoint l n k z = ActualPrimaryDynamics.copyPoint l.1 l.2 n k (ActualParticularStageControls.nativeToFull z)

theorem NavierStokes.ActualParticularDynamics.normalWeight_eq {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (j : ℤ) (hj : j ≠ 0) : PhysicalParticularWave.normalWeight (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2)) (↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2))) = ActualPrimaryDynamics.normalScale l.2 n

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

Data used in actual particular dynamics.

Equations

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

theorem NavierStokes.ActualParticularDynamics.data_phase {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : (data x l j).background.phase = (ActualParticularStageControls.background l).phase

theorem NavierStokes.ActualParticularDynamics.data_frequency {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : (data x l j).background.frequency n = ↑j * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)

theorem NavierStokes.ActualParticularDynamics.native_strip_eq : CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip = ParticularWaveBounds.reindexStrip ActualParticularStageControls.nativeToFull (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion))

theorem NavierStokes.ActualParticularDynamics.background_normal {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) {z : ActualParticularStageControls.Native} (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) : (ActualParticularStageControls.background l).normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z = (CorrectionInitialization.ActualPrimary.chartCoefficients l.1 l.2).normal (HarmonicWaveInteraction.productStrip (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion)) (PrimaryResidualClass.directions (CorrectionInitialization.ActualPrimary.commonContext B)) n (ActualParticularStageControls.nativeToFull z)

theorem NavierStokes.ActualParticularDynamics.data_normal {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (z : ActualParticularStageControls.Native) : (data x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z = (ActualParticularStageControls.background l).normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z

theorem NavierStokes.ActualParticularDynamics.tangent_normal {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (hfrequency : ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) (k : TorusInverse.Frequency) (z : ActualParticularStageControls.Native) : ((ActualParticularStageControls.parameters x l).nativeTangent j n).normal (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k z) = ActualPrimaryDynamics.normalScale l.2 n • ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).frame l.2).normal ((referencePoint l n k z).1, (referencePoint l n k z).2.2)

theorem NavierStokes.ActualParticularDynamics.native_normal_match {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (hp : (referencePoint l n k z).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2) (ht : (referencePoint l n k z).2.2 ∈ Set.Icc 0 ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).L l.2)) (hc : (referencePoint l n k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : (data x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z = ((ActualParticularStageControls.parameters x l).nativeTangent j n).normal (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k z)

theorem NavierStokes.ActualParticularDynamics.transported_coordinates {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (z : ActualParticularStageControls.Native) : CopySolveCompatibility.nativeTimeMap 0 (PhysicalParticularWave.clockWeight CorrectionInitialization.ActualPrimary.h (ChartScales.Q n) (ChartScales.Q (BaseChartJets.cellBand l.2))) (((ActualParticularStageControls.parameters x l).geometry n).coordinates k z.2) = (referencePoint l n k z).2

theorem NavierStokes.ActualParticularDynamics.tangent_action {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) (z : ActualParticularStageControls.Native) : ((ActualParticularStageControls.parameters x l).nativeTangent j n).action (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k z) = ActualPrimaryDynamics.clockScale l.2 n • PrimaryCopyBridge.baseOperator ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).phase.F l.2 (referencePoint l n k z).1) ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).phase.shear l.2 ((referencePoint l n k z).1, (referencePoint l n k z).2.2))

theorem NavierStokes.ActualParticularDynamics.tangent_damping {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) (z : ActualParticularStageControls.Native) : ((ActualParticularStageControls.parameters x l).nativeTangent j n).damping (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k z) = ActualPrimaryDynamics.clockScale l.2 n * (↑j ^ 2 * (ChartScales.epsilon CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) * ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) ^ 2 * ‖(CorrectionInitialization.ActualPrimary.phases B N0 l.1).phase.normal l.2 ((referencePoint l n k z).1, (referencePoint l n k z).2.2)‖ ^ 2))

theorem NavierStokes.ActualParticularDynamics.native_damping_match {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (hc : (referencePoint l n k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : ((ActualParticularStageControls.parameters x l).nativeTangent j n).damping (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k z) = (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).epsilon n * (data x l j).background.frequency n ^ 2 * ‖(data x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z‖ ^ 2

theorem NavierStokes.ActualParticularDynamics.reference_slotDirection {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) : ParticularWaveBounds.slotDirection (ActualParticularStageControls.reference l).geometry = ChartScales.timeCoefficient CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2) • CorrectionInitialization.ActualPrimary.temporalVector

theorem NavierStokes.ActualParticularDynamics.native_fast {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) : ActualParticularStageControls.directions.fastScale n • ActualParticularStageControls.directions.fast = (0, ParticularWaveBounds.slotDirection ((ActualParticularStageControls.parameters x l).geometry n))

theorem NavierStokes.ActualParticularDynamics.native_action_match {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (v : ProblemStatement.Space) : CurlClassBounds.complexify ((((ActualParticularStageControls.parameters x l).nativeTangent j n).action (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k z)) v) = LinearWaveResidual.shear ((data x l j).background.radius n) ((data x l j).background.frequencyBase n) ((data x l j).background.axialBase n) (ActualParticularStageControls.directions.radialField n) (fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => CurlClassBounds.complexify v) z

theorem NavierStokes.ActualParticularDynamics.referencePoint_contDiff {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) : ContDiff ℝ (↑⊤) (referencePoint l n k)

theorem NavierStokes.ActualParticularDynamics.native_normal_germ {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (hp : (referencePoint l n k z).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2) (ht : (referencePoint l n k z).2.2 ∈ Set.Ioo 0 ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).L l.2)) (hc : (referencePoint l n k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : (data x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n =ᶠ[nhds z] fun (y : ActualParticularStageControls.Native) => ((ActualParticularStageControls.parameters x l).nativeTangent j n).normal (ParticularWaveBounds.nativePoint ((ActualParticularStageControls.parameters x l).geometry n) k y)

The copied normal equality is a true germ, including on the closed transverse core boundary. Only slot time and the slow carrier are open.

theorem NavierStokes.ActualParticularDynamics.complexCopy_tangent_germ {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {s : WeightedClasses.StripData (P × TorusInverse.Plane)} {α : ℝ} {ds : LinearWaveBounds.GraphDirections (P × TorusInverse.Plane)} {frame : ℕ → PrimaryODE.FrameData (P × ℝ)} {t : ℕ → CommonCoverSolve.TangentData P ProblemStatement.Space} {source : ℕ → P × TorusInverse.Plane → HarmonicCalculus.ComplexVector} {j : ℤ} {g : ℕ → CommonCoverSolve.Geometry} {len : ℕ → ℝ} {envelope : ℕ → ℝ → ℝ} {C : ℕ → TorusInverse.Frequency → Set (P × TorusInverse.Plane)} (a : LinearWaveBounds.WaveCoefficients (P × TorusInverse.Plane)) (hL : ∀ (n : ℕ), 0 < len n) (hr : ParticularCopyBounds.ModalControl s α frame (fun (n : ℕ) => ParticularWaveBounds.realData (t n) (source n)) j g len envelope C) (hi : ParticularCopyBounds.ModalControl s α frame (fun (n : ℕ) => ParticularWaveBounds.imagData (t n) (source n)) j g len envelope C) (n : ℕ) (k : TorusInverse.Frequency) {z : P × TorusInverse.Plane} (hz : z ∈ s.domain) (hC : z ∈ C n k) (hN : a.normal s ds n =ᶠ[nhds z] fun (y : P × TorusInverse.Plane) => (t n).normal (ParticularWaveBounds.nativePoint (g n) k y)) : (fun (y : P × TorusInverse.Plane) => HarmonicCalculus.normalDot (a.normal s ds n y) ((ParticularWaveBounds.complexCopyCoefficients a t source g (fun (x : ℕ) => k) len hL).amplitude n y)) =ᶠ[nhds z] fun (x : P × TorusInverse.Plane) => 0

The actual modal reconstruction is tangent throughout a neighborhood of a closed-cell point. The normal match is a primitive geometric germ; the tangency of both solved components follows from the modal bridges.

theorem NavierStokes.ActualParticularDynamics.reindex_vector_derivative {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {V : F → F} {z : E} (hV : DifferentiableAt ℝ V (e z)) (w : F) : (fderiv ℝ (ParticularWaveBounds.reindexVector e V) z) (e.symm w) = e.symm ((fderiv ℝ V (e z)) w)

theorem NavierStokes.ActualParticularDynamics.geometryAt_reindex {E F : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (e : E ≃ₗᵢ[ℝ] F) {R : F → ℝ} {Vr Vθ Vz : F → F} {z : E} (G : ClosedNativeWaveIdentities.GeometryAt R Vr Vθ Vz (e z)) : ClosedNativeWaveIdentities.GeometryAt (fun (y : E) => R (e y)) (ParticularWaveBounds.reindexVector e Vr) (ParticularWaveBounds.reindexVector e Vθ) (ParticularWaveBounds.reindexVector e Vz) z

theorem NavierStokes.ActualParticularDynamics.geometryAt_of_cylindrical {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : Set F} {R : F → ℝ} {Vr Vθ Vz : F → F} {z : F} (G : CurlClassBounds.CylindricalGeometry Ω R Vr Vθ Vz) (hz : z ∈ Ω) : ClosedNativeWaveIdentities.GeometryAt R Vr Vθ Vz z

theorem NavierStokes.ActualParticularDynamics.native_geometry {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) : ClosedNativeWaveIdentities.GeometryAt ((data 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) z

theorem NavierStokes.ActualParticularDynamics.invariant_native {B : ℕ} {E : Type} {f : CorrectionInitialization.ActualPrimary.FullPoint → E} (hf : CopyAngularInvariance.Invariant (0, 1) f) : CopyAngularInvariance.Invariant ActualParticularStageControls.directions.angular fun (z : ActualParticularStageControls.Native) => f (ActualParticularStageControls.nativeToFull z)

theorem NavierStokes.ActualParticularDynamics.native_angular {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) : ClosedNativeWaveIdentities.AngularData ((data x l j).raw k) (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions (fun (m : ℕ) => (data x l j).cutoff m k) n

theorem NavierStokes.ActualParticularDynamics.associated_frame_match {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) : CorrectionStep.WaveFrameMatch ActualParticularStageControls.associatedContext (HarmonicWaveInteraction.productStrip ActualParticularStageControls.associatedStrip) (ParticularWaveBounds.reindexDirections ParticularWaveAssembly.angleShuffle ActualParticularStageControls.directions) (ParticularWaveBounds.reindexCoefficients ParticularWaveAssembly.angleShuffle (ActualParticularStageControls.background l))

theorem NavierStokes.ActualParticularDynamics.native_radialProfile_smoothAt {B : ℕ} {z : ActualParticularStageControls.Native} (hR : 0 < z.1.1.1) : ContDiffAt ℝ (↑⊤) ActualParticularStageControls.directions.radialProfile z

theorem NavierStokes.ActualParticularDynamics.native_base_smoothAt {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) : ContDiffAt ℝ (↑⊤) ((data x l j).background.radialBase n) z ∧ ContDiffAt ℝ (↑⊤) ((data x l j).background.frequencyBase n) z ∧ ContDiffAt ℝ (↑⊤) ((data x l j).background.axialBase n) z

theorem NavierStokes.ActualParticularDynamics.data_phase_smoothAt {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) : ContDiffAt ℝ (↑⊤) ((data x l j).background.phase n) z

theorem NavierStokes.ActualParticularDynamics.native_cutoff_smooth {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) : ContDiff ℝ (↑⊤) ((data x l j).cutoff n k)

theorem NavierStokes.ActualParticularDynamics.native_normal_ne {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (hp : (referencePoint l n k z).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2) (ht : (referencePoint l n k z).2.2 ∈ Set.Icc 0 ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).L l.2)) (hc : (referencePoint l n k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) : (data x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z ≠ 0

theorem NavierStokes.ActualParticularDynamics.rawJets_at {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (H : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hi : CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n ≤ ChartScales.nativeIndex CorrectionInitialization.ActualPrimary.h (BaseChartJets.cellBand l.2)) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (hp : (referencePoint l n k z).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2) (ht : (referencePoint l n k z).2.2 ∈ Set.Icc 0 ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).L l.2)) (hc : (referencePoint l n k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core) (ha : ContDiffAt ℝ (↑⊤) ((data x l j).amplitude n k) z) (hpres : ContDiffAt ℝ (↑⊤) ((data x l j).pressure n k) z) : ClosedNativeWaveIdentities.RawJetsAt ((data x l j).raw k) (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions (fun (m : ℕ) => (data x l j).cutoff m k) n z

theorem NavierStokes.ActualParticularDynamics.localized_zero_of_cutoff_germ {D I : Type} [NormedAddCommGroup D] (a : PeriodizedWaveBounds.CopyData D I) {n : ℕ} {i : I} {z : D} (h : a.cutoff n i =ᶠ[nhds z] fun (x : D) => 0) : ((a.localized i).amplitude n =ᶠ[nhds z] fun (x : D) => 0) ∧ (a.localized i).pressure n =ᶠ[nhds z] fun (x : D) => 0

theorem NavierStokes.ActualParticularDynamics.gaussian_eq_source_of_cutoff_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {z : D} (h : a.cutoff n i =ᶠ[nhds z] fun (x : D) => 0) : a.localGaussian d n i =ᶠ[nhds z] a.source n

theorem NavierStokes.ActualParticularDynamics.cancellation_of_cutoff_germ {D I : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] (a : PeriodizedWaveBounds.CopyData D I) (s : WeightedClasses.StripData D) (d : LinearWaveBounds.GraphDirections D) {n : ℕ} {i : I} {z : D} (h : a.cutoff n i =ᶠ[nhds z] fun (x : D) => 0) : ((a.corrected s d i).harmonicResidual s d n z + fun (q : Fin 3) => a.source n z q * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) z) = fun (q : Fin 3) => (a.localGood s d n i z q + a.localGaussian d n i z q) * HarmonicCalculus.carrier (a.background.frequency n) (a.background.phase n) z

noncomputable def NavierStokes.ActualParticularDynamics.selectedDirections {B N0 : ℕ} (e : ℕ → ActualParticularStageControls.ActivePair B N0) : LinearWaveBounds.GraphDirections ActualParticularStageControls.Native

Selected directions as an element of LinearWaveBounds.GraphDirections Native.

Equations

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

noncomputable def NavierStokes.ActualParticularDynamics.modalStrip {B N0 : ℕ} (e : ℕ → ActualParticularStageControls.ActivePair B N0) : WeightedClasses.StripData ((ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane)

Modal strip, constructed using UniformPrimaryWeights.reindexedStrip.

Equations

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

theorem NavierStokes.ActualParticularDynamics.selected_principal {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (e : ℕ → ActualParticularStageControls.ActivePair B N0) (q : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ (modalStrip e).domain) (hcell : z ∈ ActualParticularStageControls.selectedPatch e () q k) (hR : 0 < z.1.1.1) (hT : 0 < z.1.1.2.1) (hp : (referencePoint (ActualParticularStageControls.selectedLabel e q) (ActualParticularStageControls.selectedBand e q) k z).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier (ActualParticularStageControls.selectedLabel e q).2) (ht : (referencePoint (ActualParticularStageControls.selectedLabel e q) (ActualParticularStageControls.selectedBand e q) k z).2.2 ∈ Set.Icc 0 ((CorrectionInitialization.ActualPrimary.phases B N0 (ActualParticularStageControls.selectedLabel e q).1).L (ActualParticularStageControls.selectedLabel e q).2)) (hc : (referencePoint (ActualParticularStageControls.selectedLabel e q) (ActualParticularStageControls.selectedBand e q) k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow (ActualParticularStageControls.selectedLabel e q).2).core) : ((data x (ActualParticularStageControls.selectedLabel e q) j).raw k).principal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions (ActualParticularStageControls.selectedBand e q) z = -(data x (ActualParticularStageControls.selectedLabel e q) j).source (ActualParticularStageControls.selectedBand e q) z

theorem NavierStokes.ActualParticularDynamics.controlPatch_geometry {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : 0 < z.1.1.1 ∧ 0 < z.1.1.2.1 ∧ (referencePoint l n k z).1 ∈ (PrimaryGeometryAssembly.domain CorrectionInitialization.ActualPrimary.nominal (CorrectionInitialization.ActualPrimary.choice B N0).prepared.N).carrier l.2 ∧ (referencePoint l n k z).2.2 ∈ Set.Ioo 0 ((CorrectionInitialization.ActualPrimary.phases B N0 l.1).L l.2) ∧ (referencePoint l n k z).2 ∈ (CorrectionInitialization.ActualPrimary.clockWindow l.2).core

theorem NavierStokes.ActualParticularDynamics.native_principal {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : ((data x l j).raw k).principal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z = -(data x l j).source n z

theorem NavierStokes.ActualParticularDynamics.native_tangency_germ {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : (fun (y : ActualParticularStageControls.Native) => HarmonicCalculus.normalDot ((data x l j).background.normal (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n y) ((data x l j).amplitude n k y)) =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0

theorem NavierStokes.ActualParticularDynamics.native_rawJets {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : ClosedNativeWaveIdentities.RawJetsAt ((data x l j).raw k) (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions (fun (m : ℕ) => (data x l j).cutoff m k) n z

theorem NavierStokes.ActualParticularDynamics.frequency_ne {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : (data x l j).background.frequency n ≠ 0

theorem NavierStokes.ActualParticularDynamics.native_cancellation {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : (((data x l j).corrected (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions k).harmonicResidual (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z + fun (i : Fin 3) => (data x l j).source n z i * HarmonicCalculus.carrier ((data x l j).background.frequency n) ((data x l j).background.phase n) z) = fun (i : Fin 3) => ((data x l j).localGood (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n k z i + (data x l j).localGaussian ActualParticularStageControls.directions n k z i) * HarmonicCalculus.carrier ((data x l j).background.frequency n) ((data x l j).background.phase n) z

The literal common-cover inverse solves the current source at every closed transverse cell point. No open-cell or final equation hypothesis is used.

theorem NavierStokes.ActualParticularDynamics.native_realizes_curl {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : CurlClassBounds.cylindricalCurl ((data 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) (((data x l j).localized k).curlPotential (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n) z = HarmonicCalculus.vectorMode ((data x l j).background.frequency n) ((data x l j).background.phase n) (((data x l j).corrected (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions k).amplitude n) z

theorem NavierStokes.ActualParticularDynamics.native_divergence_zero {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : HarmonicCalculus.cylindricalDivergence ((data 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) (HarmonicCalculus.vectorMode ((data x l j).background.frequency n) ((data x l j).background.phase n) (((data x l j).corrected (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions k).amplitude n)) z = 0

structure NavierStokes.ActualParticularDynamics.SupportData {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : Type

The support information supplied by the actual incoming source and the common-cover cutoff. The last alternative is proved by zero source on the whole native solve path. It contains no differential equation.

• cells : PeriodizedWaveBounds.Cells ActualParticularStageControls.Native TorusInverse.Frequency

  Cells of SupportData, of type PeriodizedWaveBounds.Cells Native Frequency.

• cutoff_support (n : ℕ) (k : TorusInverse.Frequency) : Function.support ((data x l j).cutoff n k) ⊆ self.cells.carrier n k
• cover (n : ℕ) (k : TorusInverse.Frequency) (z : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain → z ∈ self.cells.carrier n k → z ∈ ActualParticularStageControls.controlPatch l n k ∨ ((data x l j).cutoff n k =ᶠ[nhds z] fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => 0) ∨ ((data x l j).amplitude n k =ᶠ[nhds z] fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => 0) ∧ ((data x l j).pressure n k =ᶠ[nhds z] fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => 0) ∧ (data x l j).source n =ᶠ[nhds z] fun (x : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => 0

theorem NavierStokes.ActualParticularDynamics.localized_zero_of_fields {D I : Type} [NormedAddCommGroup D] (a : PeriodizedWaveBounds.CopyData D I) {n : ℕ} {k : I} {z : D} (ha : a.amplitude n k =ᶠ[nhds z] fun (x : D) => 0) (hp : a.pressure n k =ᶠ[nhds z] fun (x : D) => 0) : ((a.localized k).amplitude n =ᶠ[nhds z] fun (x : D) => 0) ∧ (a.localized k).pressure n =ᶠ[nhds z] fun (x : D) => 0

theorem NavierStokes.ActualParticularDynamics.SupportData.localized_alternative {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} {l : ActualParticularStageControls.Label B N0} {j : ℤ} (S : SupportData x l j) {n : ℕ} {k : TorusInverse.Frequency} {z : ActualParticularStageControls.Native} (hz : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain) (hk : z ∈ S.cells.carrier n k) : z ∈ ActualParticularStageControls.controlPatch l n k ∨ (((data x l j).localized k).amplitude n =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0) ∧ ((data x l j).localized k).pressure n =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0

noncomputable def NavierStokes.ActualParticularDynamics.actualWave {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : LinearWaveBounds.WaveCoefficients ((ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane)

Actual wave used in actual particular dynamics.

Equations

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

theorem NavierStokes.ActualParticularDynamics.common_cancellation {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain) : ((actualWave x l j).harmonicResidual (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z + fun (i : Fin 3) => (data x l j).source n z i * HarmonicCalculus.carrier ((data x l j).background.frequency n) ((data x l j).background.phase n) z) = fun (i : Fin 3) => ((data x l j).globalGood (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n z i + (data x l j).globalGaussian ActualParticularStageControls.directions n z i) * HarmonicCalculus.carrier ((data x l j).background.frequency n) ((data x l j).background.phase n) z

theorem NavierStokes.ActualParticularDynamics.common_realizes_curl {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain) : CurlClassBounds.cylindricalCurl ((data 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) ((data x l j).common.curlPotential (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n) z = HarmonicCalculus.vectorMode ((actualWave x l j).frequency n) ((actualWave x l j).phase n) ((actualWave x l j).amplitude n) z

theorem NavierStokes.ActualParticularDynamics.common_divergence_zero {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain) : HarmonicCalculus.cylindricalDivergence ((data 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) (HarmonicCalculus.vectorMode ((actualWave x l j).frequency n) ((actualWave x l j).phase n) ((actualWave x l j).amplitude n)) z = 0

theorem NavierStokes.ActualParticularDynamics.common_smooth {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((actualWave x l j).amplitude n) (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain ∧ ContDiffOn ℝ (↑⊤) ((actualWave x l j).pressure n) (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain

theorem NavierStokes.ActualParticularDynamics.common_amplitude_invariant {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : CopyAngularInvariance.Invariant ActualParticularStageControls.directions.angular ((actualWave x l j).amplitude n)

theorem NavierStokes.ActualParticularDynamics.common_pressure_invariant {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : CopyAngularInvariance.Invariant ActualParticularStageControls.directions.angular ((actualWave x l j).pressure n)

theorem NavierStokes.ActualParticularDynamics.common_good_invariant {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : CopyAngularInvariance.Invariant ActualParticularStageControls.directions.angular ((data x l j).globalGood (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n)

theorem NavierStokes.ActualParticularDynamics.common_gaussian_invariant {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : CopyAngularInvariance.Invariant ActualParticularStageControls.directions.angular ((data x l j).globalGaussian ActualParticularStageControls.directions n)

theorem NavierStokes.ActualParticularDynamics.source_frequency_ne {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (n : ℕ) : (ActualParticularStageControls.assembly x l).carrierBlock.frequency n ≠ 0

noncomputable def NavierStokes.ActualParticularDynamics.actualUpdate {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (N : ℕ) : CorrectionState.HarmonicBlock (ActualParticularStageControls.Parameter × TorusInverse.Plane)

Actual update used in actual particular dynamics.

Equations

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

noncomputable def NavierStokes.ActualParticularDynamics.actualGood {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (N : ℕ) : CorrectionState.HarmonicBlock (ActualParticularStageControls.Parameter × TorusInverse.Plane)

Actual good used in actual particular dynamics.

Equations

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

noncomputable def NavierStokes.ActualParticularDynamics.actualGaussian {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (N : ℕ) : CorrectionState.HarmonicBlock (ActualParticularStageControls.Parameter × TorusInverse.Plane)

Actual gaussian used in actual particular dynamics.

Equations

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

theorem NavierStokes.ActualParticularDynamics.update_represents {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (N : ℕ) : ((actualUpdate x l N).oscillation = fun (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (i : Fin 3) => ∑ j ∈ ParticularWaveAssembly.modes N, (HarmonicCalculus.vectorMode ((actualWave x l j).frequency n) ((actualWave x l j).phase n) ((actualWave x l j).amplitude n) (ParticularWaveAssembly.angleShuffle z) i).re) ∧ (actualUpdate x l N).oscillatoryPressure = fun (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) => ∑ j ∈ ParticularWaveAssembly.modes N, (HarmonicCalculus.mode ((actualWave x l j).frequency n) ((actualWave x l j).phase n) ((actualWave x l j).pressure n) (ParticularWaveAssembly.angleShuffle z)).re

theorem NavierStokes.ActualParticularDynamics.native_phase_smooth {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((data x l j).background.phase n) (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip).domain

theorem NavierStokes.ActualParticularDynamics.wave_smooth {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) (i : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) => HarmonicCalculus.vectorMode ((actualWave x l j).frequency n) ((actualWave x l j).phase n) ((actualWave x l j).amplitude n) (ParticularWaveAssembly.angleShuffle z) i) (HarmonicResidual.liftDomain ActualParticularStageControls.associatedStrip.domain)

theorem NavierStokes.ActualParticularDynamics.pressure_smooth {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) : ContDiffOn ℝ (↑⊤) (fun (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) => HarmonicCalculus.mode ((actualWave x l j).frequency n) ((actualWave x l j).phase n) ((actualWave x l j).pressure n) (ParticularWaveAssembly.angleShuffle z)) (HarmonicResidual.liftDomain ActualParticularStageControls.associatedStrip.domain)

noncomputable def NavierStokes.ActualParticularDynamics.supportData {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : ActualParticularStageControls.Label B N0) (j : ℤ) : SupportData x l j

Support data, bundling cells, cutoff_support, cover.

Equations

• NavierStokes.ActualParticularDynamics.supportData x hs hN l j = { cells := NavierStokes.ActualParticularStageControls.carrierCells l, cutoff_support := ⋯, cover := ⋯ }

theorem NavierStokes.ActualParticularDynamics.source_phase_smooth {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((ActualParticularStageControls.assembly x l).carrierBlock.phase n) ActualParticularStageControls.associatedStrip.domain

theorem NavierStokes.ActualParticularDynamics.source_angular_ne {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (n : ℕ) : (ActualParticularStageControls.assembly x l).carrierBlock.angularFrequency n ≠ 0

theorem NavierStokes.ActualParticularDynamics.associated_base_smooth {B : ℕ} : MeanIncrementBounds.SmoothTriple ActualParticularStageControls.associatedStrip.domain ActualParticularStageControls.associatedContext.base

theorem NavierStokes.ActualParticularDynamics.associated_radial_smooth {B : ℕ} (n : ℕ) : ContDiffOn ℝ (↑⊤) (HarmonicResidual.contextFrame ActualParticularStageControls.associatedContext n).radial ActualParticularStageControls.associatedStrip.domain

theorem NavierStokes.ActualParticularDynamics.pair_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) (j : ℤ) : HarmonicResidual.SmoothCoefficients U (ErrorHarmonics.conjugatePair j f)

theorem NavierStokes.ActualParticularDynamics.update_smooth {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (N : ℕ) (Hs : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : (j : ℤ) → j ∈ ParticularWaveAssembly.modes N → SupportData x l j) (n : ℕ) : (∀ (i : Fin 3), HarmonicResidual.SmoothCoefficients ActualParticularStageControls.associatedStrip.domain ((actualUpdate x l N).velocity n i)) ∧ HarmonicResidual.SmoothCoefficients ActualParticularStageControls.associatedStrip.domain ((actualUpdate x l N).pressure n)

@[reducible, inline]

abbrev NavierStokes.ActualParticularDynamics.SourceClasses {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (N : ℕ) (α : ℝ) : Prop

Source classes type used in actual particular dynamics.

Equations

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

theorem NavierStokes.ActualParticularDynamics.section_equation {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (Hs : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (l : ActualParticularStageControls.Label B N0) (S : SupportData x l j) (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (hz : z.1 ∈ ActualParticularStageControls.associatedStrip.domain) (i : Fin 3) : (actualWave x l j).harmonicResidual (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n (ParticularWaveAssembly.angleShuffle z) i + ParticularWaveAssembly.residualSource (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput j n z.1 i * HarmonicFields.character j ((ActualParticularStageControls.assembly x l).carrierBlock.frequency n * (ActualParticularStageControls.assembly x l).carrierBlock.phase n z.1 + ↑((ActualParticularStageControls.assembly x l).carrierBlock.angularFrequency n) * z.2) = ((data x l j).globalGood (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n (ParticularWaveAssembly.angleShuffle (z.1, 0)) i + (data x l j).globalGaussian ActualParticularStageControls.directions n (ParticularWaveAssembly.angleShuffle (z.1, 0)) i) * HarmonicFields.character j ((ActualParticularStageControls.assembly x l).carrierBlock.frequency n * (ActualParticularStageControls.assembly x l).carrierBlock.phase n z.1 + ↑((ActualParticularStageControls.assembly x l).carrierBlock.angularFrequency n) * z.2)

theorem NavierStokes.ActualParticularDynamics.cancellation_sum {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (S : (j : ℤ) → j ∈ ParticularWaveAssembly.modes N → SupportData x l j) (hBand : (HarmonicResidual.residualBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput).BandLimited N) (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (hz : z.1 ∈ ActualParticularStageControls.associatedStrip.domain) : (fun (i : Fin 3) => ∑ j ∈ ParticularWaveAssembly.modes N, ((actualWave x l j).harmonicResidual (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n (ParticularWaveAssembly.angleShuffle z) i).re) + (HarmonicResidual.residualBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput).oscillation n z = (actualGood x l N).oscillation n z + (actualGaussian x l N).oscillation n z

theorem NavierStokes.ActualParticularDynamics.context_linear_sum {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (S : (j : ℤ) → j ∈ ParticularWaveAssembly.modes N → SupportData x l j) (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (hz : z.1 ∈ ActualParticularStageControls.associatedStrip.domain) : CorrectionStep.linearBlockField (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).carrierBlock (actualUpdate x l N) n z = fun (i : Fin 3) => ∑ j ∈ ParticularWaveAssembly.modes N, ((actualWave x l j).harmonicResidual (CorrectionStep.ParticularParameters.nativeStrip ActualParticularStageControls.associatedStrip) ActualParticularStageControls.directions n (ParticularWaveAssembly.angleShuffle z) i).re

theorem NavierStokes.ActualParticularDynamics.context_linear_cancellation_of_support {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (S : (j : ℤ) → j ∈ ParticularWaveAssembly.modes N → SupportData x l j) (hBand : (HarmonicResidual.residualBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput).BandLimited N) (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (hz : z.1 ∈ ActualParticularStageControls.associatedStrip.domain) : CorrectionStep.linearBlockField (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).carrierBlock (actualUpdate x l N) n z + (HarmonicResidual.residualBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput).oscillation n z = (actualGood x l N).oscillation n z + (actualGaussian x l N).oscillation n z

theorem NavierStokes.ActualParticularDynamics.full_divergence_zero {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (S : (j : ℤ) → j ∈ ParticularWaveAssembly.modes N → SupportData x l j) (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (hz : z.1 ∈ ActualParticularStageControls.associatedStrip.domain) : HarmonicCalculus.cylindricalDivergence (fun (y : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) => (ActualParticularStageControls.assembly x l).context.operators.radius y.1) (CorrectionStep.radialDirection (ActualParticularStageControls.assembly x l).context n) CorrectionStep.angularDirection (CorrectionStep.axialDirection (ActualParticularStageControls.assembly x l).context n) (fun (y : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (i : Fin 3) => ↑((actualUpdate x l N).oscillation n y i)) z = 0

theorem NavierStokes.ActualParticularDynamics.modeSolenoidal_of_support {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (S : (j : ℤ) → j ∈ ParticularWaveAssembly.modes N → SupportData x l j) : HarmonicWaveInteraction.ModeSolenoidal ActualParticularStageControls.associatedStrip (ActualParticularStageControls.assembly x l).context (actualUpdate x l N)

theorem NavierStokes.ActualParticularDynamics.modeSolenoidal {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) : HarmonicWaveInteraction.ModeSolenoidal ActualParticularStageControls.associatedStrip (ActualParticularStageControls.assembly x l).context (actualUpdate x l N)

Actual incoming support and source classes imply solenoidality of the finite particular correction.

theorem NavierStokes.ActualParticularDynamics.context_linear_cancellation {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (hBand : (HarmonicResidual.residualBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput).BandLimited N) (n : ℕ) (z : (ActualParticularStageControls.Parameter × TorusInverse.Plane) × ℝ) (hz : z.1 ∈ ActualParticularStageControls.associatedStrip.domain) : CorrectionStep.linearBlockField (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).carrierBlock (actualUpdate x l N) n z + (HarmonicResidual.residualBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput).oscillation n z = (actualGood x l N).oscillation n z + (actualGaussian x l N).oscillation n z

The actual current residual is cancelled by the finite common-cover solve, with the computed retained and Gaussian terms on the right.

noncomputable def NavierStokes.ActualParticularDynamics.cycleUpdate {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (N : ℕ) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Cycle update, given by StateReindex.block cycleAssoc (actualUpdate x l N).

Equations

• NavierStokes.ActualParticularDynamics.cycleUpdate x l N = NavierStokes.StateReindex.block NavierStokes.CorrectionStep.cycleAssoc (NavierStokes.ActualParticularDynamics.actualUpdate x l N)

theorem NavierStokes.ActualParticularDynamics.cycle_modeSolenoidal {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) : HarmonicWaveInteraction.ModeSolenoidal (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) (CorrectionInitialization.ActualPrimary.commonContext B) (cycleUpdate x l N)

theorem NavierStokes.ActualParticularDynamics.actualUpdate_eq_canonical {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (l : ActualParticularStageControls.Label B N0) (N : ℕ) : actualUpdate x l N = (ActualParticularStageControls.canonicalParameters l).updateBlock ActualParticularStageControls.associatedStrip (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput N

theorem NavierStokes.ActualParticularDynamics.linearBlockField_pull {D E : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup E] [NormedSpace ℝ E] (e : D ≃ₗᵢ[ℝ] E) (c : CorrectionState.Context E) (a b : CorrectionState.HarmonicBlock E) (n : ℕ) (z : D × ℝ) : CorrectionStep.linearBlockField (StateReindex.context e c) (StateReindex.block e a) (StateReindex.block e b) n z = CorrectionStep.linearBlockField c a b n ((StateReindex.cylinder e) z)

theorem NavierStokes.ActualParticularDynamics.cycle_context_linear_cancellation {B N0 : ℕ} {x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)} (Hc : PreservesCarriers x) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (N : ℕ) (Hs : SourceClasses x N α) (l : ActualParticularStageControls.Label B N0) (hBand : (HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)).BandLimited N) (n : ℕ) (z : CorrectionStep.CyclePoint × ℝ) (hz : z.1 ∈ (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion).domain) : CorrectionStep.linearBlockField (CorrectionInitialization.ActualPrimary.commonContext B) (x.coefficients.blocks l) (cycleUpdate x l N) n z + (HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)).oscillation n z = (StateReindex.block CorrectionStep.cycleAssoc (actualGood x l N)).oscillation n z + (StateReindex.block CorrectionStep.cycleAssoc (actualGaussian x l N)).oscillation n z

The weighted Gaussian error of the actual particular update

The native estimates are those of the selected actual Volterra solves, already transferred back to the original label and band in raw_jets. Gaussian decay is applied at that original band. The square-root moving-edge weight is kept through the entire estimate, including the uncovered source term.

noncomputable def NavierStokes.ActualParticularGaussian.nativeStrip : WeightedClasses.StripData ActualParticularStageControls.Native

Native strip, given by CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip slowStrip).

Equations

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

noncomputable def NavierStokes.ActualParticularGaussian.bandScales : GaussianTailFlat.BandScaleControl nativeStrip

Band scales, bundling power, epsilon_eq, boundConstant, constant_one_le and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualParticularGaussian.fast_bound {B : ℕ} : WeightedClasses.BandBound nativeStrip 0 ActualParticularStageControls.directions.fastScale

The clock bounds are imposed only on active pairs.

noncomputable def NavierStokes.ActualParticularGaussian.clockUpper : ℝ

Clock upper, given by `ActualSignedGeometry.powerBound (CoordinateAlgebra.A ActualPrimary.h

• 1 / 2)`.

Equations

• NavierStokes.ActualParticularGaussian.clockUpper = NavierStokes.ActualSignedGeometry.powerBound (NavierStokes.CoordinateAlgebra.A NavierStokes.CorrectionInitialization.ActualPrimary.h + 1 / 2)

theorem NavierStokes.ActualParticularGaussian.clockUpper_pos : 0 < clockUpper

theorem NavierStokes.ActualParticularGaussian.clock_bounds {B N0 : ℕ} {l : ActualParticularStageControls.Label B N0} {n : ℕ} (ha : ActualParticularStageControls.Active l n) : 1 / clockUpper ≤ ActualCarrierTransportBase.clock (ActualParticularStageControls.supportLabel l) n ∧ ActualCarrierTransportBase.clock (ActualParticularStageControls.supportLabel l) n ≤ clockUpper

noncomputable def NavierStokes.ActualParticularGaussian.transportedLength {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) : ℝ

Transported length, given by ActualCarrierTransportBase.referenceLength (supportLabel l) / ActualCarrierTransportBase.clock (supportLabel l) n.

Equations

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

theorem NavierStokes.ActualParticularGaussian.transportedLength_pos {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) : 0 < transportedLength l n

noncomputable def NavierStokes.ActualParticularGaussian.lengthLower : ℝ

Length lower, given by ActualInitialExcluded.gaussianLengthLower / clockUpper.

Equations

• NavierStokes.ActualParticularGaussian.lengthLower = NavierStokes.ActualInitialExcluded.gaussianLengthLower / NavierStokes.ActualParticularGaussian.clockUpper

theorem NavierStokes.ActualParticularGaussian.lengthLower_pos : 0 < lengthLower

theorem NavierStokes.ActualParticularGaussian.transportedLength_lower {B N0 : ℕ} {l : ActualParticularStageControls.Label B N0} {n : ℕ} (ha : ActualParticularStageControls.Active l n) : lengthLower * ChartScales.S n ≤ transportedLength l n

noncomputable def NavierStokes.ActualParticularGaussian.gaussianLength {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) : ℝ

The auxiliary length agrees with the actual transported slot wherever the analytic patch is used. It only totalizes the Gaussian bookkeeping on inactive label-band pairs.

Equations

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

theorem NavierStokes.ActualParticularGaussian.gaussianLength_pos {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) : 0 < gaussianLength l n

theorem NavierStokes.ActualParticularGaussian.gaussianLength_lower {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) : lengthLower * ChartScales.S n ≤ gaussianLength l n

theorem NavierStokes.ActualParticularGaussian.gaussianLength_eq {B N0 : ℕ} {l : ActualParticularStageControls.Label B N0} {n : ℕ} (ha : ActualParticularStageControls.Active l n) : gaussianLength l n = transportedLength l n

noncomputable def NavierStokes.ActualParticularGaussian.theta {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) (z : ActualParticularStageControls.Native) : ℝ

Theta, given by ((ActualCarrierTransportBase.geometry (supportLabel l) n).coordinates k z.2).2 / transportedLength l n.

Equations

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

noncomputable def NavierStokes.ActualParticularGaussian.gaussianRate (B N0 : ℕ) : ℝ

Gaussian rate, given by ActualGaussianCoverage.gaussianRate (ActualPrimary.choice B N0).prepared.M⁻¹ (ActualPrimary.choice B N0).prepared.u / clockUpper.

Equations

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

theorem NavierStokes.ActualParticularGaussian.gaussianRate_pos (B N0 : ℕ) : 0 < gaussianRate B N0

Exact envelope and cutoff readouts on the actual analytic patch.

theorem NavierStokes.ActualParticularGaussian.envelope_gaussian {B N0 : ℕ} (l : ActualParticularStageControls.Label B N0) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) : ActualParticularStageControls.nativeEnvelope l n z ≤ Real.exp (-gaussianRate B N0 * (theta l n k z - 1 / 2) ^ 2 * gaussianLength l n)

theorem NavierStokes.ActualParticularGaussian.cutoff_central {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualParticularStageControls.controlPatch l n k) (hm : |theta l n k z - 1 / 2| < 1 / 5) : (ActualParticularStageControls.data x l j).cutoff n k =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 1

The uncovered source is zero; it is not estimated without its edge weight.

theorem NavierStokes.ActualParticularGaussian.outside_alternative {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : ActualParticularStageControls.Label B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ nativeStrip.domain) (hk : z ∈ (ActualParticularStageControls.carrierCells l).carrier n k) (hn : z ∉ ActualParticularStageControls.controlPatch l n k) : (((ActualParticularStageControls.data x l j).cutoff n k =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0) ∧ (ActualParticularStageControls.data x l j).source n =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0) ∨ ((ActualParticularStageControls.data x l j).amplitude n k =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0) ∧ (ActualParticularStageControls.data x l j).source n =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0

theorem NavierStokes.ActualParticularGaussian.source_complement {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℤ) (β : ℝ) : LocalizedGaussianBounds.UniformComplementJets nativeStrip (fun (x : ActualParticularStageControls.Label B N0) (x_1 : ℕ) (z : ActualParticularStageControls.Native) => √(nativeStrip.zeta z)) β (fun (l : ActualParticularStageControls.Label B N0) => (ActualParticularStageControls.carrierCells l).carrier) fun (l : ActualParticularStageControls.Label B N0) => (ActualParticularStageControls.data x l j).source

theorem NavierStokes.ActualParticularGaussian.globalGaussian_all_gains {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (hfrequency : ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (j : ℤ) (hj : j ≠ 0) (H : LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (β : ℝ) : LabelSumBounds.UniformClass nativeStrip (fun (x : ActualParticularStageControls.Label B N0) (x_1 : ℕ) (z : ActualParticularStageControls.Native) => √(nativeStrip.zeta z)) β fun (l : ActualParticularStageControls.Label B N0) => (ActualParticularStageControls.data x l j).globalGaussian ActualParticularStageControls.directions

Every power gain for the literal particular Gaussian error, with constants chosen before the original spatial label and band. The hypotheses concern the incoming source and its actual support, never the solved error.

theorem NavierStokes.ActualParticularGaussian.gaussianBlock_all_gains {B N0 : ℕ} (x : CorrectionStep.CycleState (ActualParticularStageControls.Label B N0)) (hfrequency : ∀ (l : ActualParticularStageControls.Label B N0) (n : ℕ), (x.coefficients.blocks l).frequency n = ↑(ChartScales.carrier CorrectionInitialization.ActualPrimary.h n)) (hs : ActualParticularStageControls.InputSupport x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) {α : ℝ} (N : ℕ) (H : ∀ j ∈ ParticularWaveAssembly.modes N, LabelSumBounds.UniformWaveClass nativeStrip ActualParticularStageControls.nativeEnvelope α (ActualParticularStageControls.currentSource x j)) (β : ℝ) (i : Fin 3) (m : ℤ) : LabelSumBounds.UniformClass ActualParticularStageControls.associatedStrip (fun (x : ActualParticularStageControls.Label B N0) (x_1 : ℕ) (z : ActualParticularStageControls.Parameter × ActualParticularStageControls.Plane) => √(ActualParticularStageControls.associatedStrip.zeta z)) β fun (l : ActualParticularStageControls.Label B N0) (n : ℕ) (z : ActualParticularStageControls.Parameter × ActualParticularStageControls.Plane) => (((ActualParticularStageControls.parameters x l).gaussianBlock (ActualParticularStageControls.assembly x l).context (ActualParticularStageControls.assembly x l).state (ActualParticularStageControls.assembly x l).carrierBlock (ActualParticularStageControls.assembly x l).gaussianInput (ActualParticularStageControls.assembly x l).aliasInput N).velocity n i).coeff m z

The literal finite harmonic Gaussian block inherits the same weighted all-power estimate. Its finite modal sum changes the constant, not its uniformity in the original spatial label and band.

@[reducible, inline]

abbrev NavierStokes.ActualParticularCycleData.Point : Type

Point: an abbreviation for ActualInitialization.Point.

Equations

• NavierStokes.ActualParticularCycleData.Point = NavierStokes.ActualInitialization.Point

@[reducible, inline]

abbrev NavierStokes.ActualParticularCycleData.Index (B N0 : ℕ) : Type

Index: an abbreviation for ActualInitialization.Index B N0.

Equations

• NavierStokes.ActualParticularCycleData.Index B N0 = NavierStokes.ActualInitialization.Index B N0

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualParticularCycleData.parameters (B N0 : ℕ) : CorrectionStep.CycleParameters (ActualCycleParameters.Index B N0)

Parameters: an abbreviation for ActualCycleParameters.fixedParameters B N0.

Equations

• NavierStokes.ActualParticularCycleData.parameters B N0 = NavierStokes.ActualCycleParameters.fixedParameters B N0

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualParticularCycleData.block {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : ActualCycleParameters.Index B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Block: an abbreviation for (parameters B N0).particularBlock x.coefficients (ActualPrimary.commonContext B) x.state.

Equations

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

@[reducible, inline]

noncomputable abbrev NavierStokes.ActualParticularCycleData.gaussianBlock {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : ActualCycleParameters.Index B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Gaussian block: an abbreviation for (parameters B N0).particularGaussianBlock x.coefficients (ActualPrimary.commonContext B) x.state.

Equations

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

@[reducible, inline]

abbrev NavierStokes.ActualParticularCycleData.Invariant {B N0 : ℕ} (σ : ℝ) (x : CorrectionStep.CycleState (Index B N0)) : Prop

Invariant type used in actual particular cycle data.

Equations

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

structure NavierStokes.ActualParticularCycleData.Data {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (σ : ℝ) : Prop

The literal particular increment's analytic outputs. No signed-wave estimate is required to prepare its mean and the subsequent signed request.

• amplitude (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 / 2 + σ) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((block x l).velocity n i).coeff j z
• pressure (j : ℤ) : LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 + σ) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((block x l).pressure n).coeff j z
• coefficients (l : ActualCycleParameters.Index B N0) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients ActualInitialization.geometry.domain ((block x l).velocity n i)
• pressureCoefficients (l : ActualCycleParameters.Index B N0) (n : ℕ) : HarmonicResidual.SmoothCoefficients ActualInitialization.geometry.domain ((block x l).pressure n)
• gaussianCoefficients (l : ActualCycleParameters.Index B N0) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients ActualInitialization.geometry.domain ((gaussianBlock x l).velocity n i)
• solenoidal (l : ActualCycleParameters.Index B N0) : HarmonicWaveInteraction.ModeSolenoidal ActualInitialization.strip (CorrectionInitialization.ActualPrimary.commonContext B) (block x l)
• gaussian (β : ℝ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformClass ActualInitialization.strip (fun (x : ActualCycleParameters.Index B N0) (x_1 : ℕ) (z : ActualInitialization.Point) => √(ActualInitialization.strip.zeta z)) β fun (l : ActualCycleParameters.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((gaussianBlock x l).velocity n i).coeff j z
• field : WaveStateRegularity.AngularSmooth ActualInitialization.geometry.domain ((parameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)
• pressureField (n : ℕ) : ContDiffOn ℝ (↑⊤) ((parameters B N0).particularPressure x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n) (ActualInitialization.geometry.domain ×ˢ Set.univ)
• periodic : CorrectionStep.OscillationPeriodic CorrectionInitialization.ActualPrimary.standardRegion.carrier ((parameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)
• support : WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b ((parameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)
• linear (i : Fin 3) (j : ℤ) : j ≠ 0 → LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 + σ - 3 * ChartScales.kappa) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)).velocity n i).coeff j z + ((HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (x.coefficients.blocks l) (block x l) (gaussianBlock x l).velocity).velocity n i).coeff j z

theorem NavierStokes.ActualParticularCycleData.Data.inputs {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (d : Data x σ) (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : ActualParticularMeanGain.Inputs x σ

The actual geometric support supplies the remaining first-wave mean inputs; this does not use any signed increment.

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

Native data used in actual particular cycle data.

Equations

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

theorem NavierStokes.ActualParticularCycleData.preservesCarriers {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) : ActualParticularDynamics.PreservesCarriers (ActualCycleParameters.particularState x)

theorem NavierStokes.ActualParticularCycleData.native_inputSupport {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) : ActualParticularStageControls.InputSupport (ActualCycleParameters.particularState x)

theorem NavierStokes.ActualParticularCycleData.nativeData_eq_data {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) : nativeData x l j = ActualParticularStageControls.data (ActualCycleParameters.particularState x) (l.2, l.1) j

theorem NavierStokes.ActualParticularCycleData.native_phase {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) : (nativeData x l j).background.phase = (ActualParticularStageControls.background (l.2, l.1)).phase

theorem NavierStokes.ActualParticularCycleData.native_source_pull {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} (l : Index B N0) (j : ℤ) (n : ℕ) : (nativeData x l j).source n = fun (z : (ActualParticularStageControls.Parameter × ℝ) × TorusInverse.Plane) => ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n (ActualCarrierTransportBase.associatedPoint z.1.1 z.2)

theorem NavierStokes.ActualParticularCycleData.native_source_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((nativeData x l j).source n) (ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion)

theorem NavierStokes.ActualParticularCycleData.native_source_exterior {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∉ Set.Icc (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (nativeData x l j).source n z = 0

theorem NavierStokes.ActualParticularCycleData.native_inactive {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) (hn : ¬ActualWaveRegularityData.Ordered l n) (j : ℤ) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) : (nativeData x l j).common.amplitude n =ᶠ[nhds z] fun (x : ActualParticularStageControls.Native) => 0

theorem NavierStokes.ActualParticularCycleData.native_source_boundary {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (nativeData x l j).source n z = 0

theorem NavierStokes.ActualParticularCycleData.native_raw_boundary {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (nativeData x l j).amplitude n k z = 0

theorem NavierStokes.ActualParticularCycleData.native_pressure_boundary {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) (k : TorusInverse.Frequency) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (nativeData x l j).pressure n k z = 0

theorem NavierStokes.ActualParticularCycleData.native_common_boundary {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (nativeData x l j).common.amplitude n z = 0 ∧ (nativeData x l j).common.pressure n z = 0

theorem NavierStokes.ActualParticularCycleData.native_gaussian_boundary {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) (n : ℕ) {z : ActualParticularStageControls.Native} (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) (hr : ActualWaveRegularityData.radius (ActualWaveRegularity.particularChart.symm z) ∉ Set.Ioo (PrimaryTargetBounds.leftRadius CorrectionInitialization.ActualPrimary.nominal) (PrimaryTargetBounds.rightRadius CorrectionInitialization.ActualPrimary.nominal)) : (nativeData x l j).globalGaussian (ActualParticularStageControls.canonicalParameters (l.2, l.1)).directions n z = 0

theorem NavierStokes.ActualParticularCycleData.native_residual {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) : UniformHarmonicInteraction.UniformVelocity (BaseContextAssembly.nativeStrip CorrectionInitialization.ActualPrimary.nominal CorrectionInitialization.ActualPrimary.standardRegion) ActualParticularStageControls.meanEnvelope (1 / 2 + σ) fun (l : ActualParticularStageControls.Label B N0) => HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) (ActualCycleParameters.particularState x).state ((ActualCycleParameters.particularState x).coefficients.blocks l) ((ActualCycleParameters.particularState x).coefficients.gaussian l) ((ActualCycleParameters.particularState x).coefficients.aliasCoefficients l)

theorem NavierStokes.ActualParticularCycleData.native_source_class {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (j : ℤ) (hj : j ≠ 0) : LabelSumBounds.UniformWaveClass (CommonCoverClass.sourceStrip (ActualParticularControl.angleStrip ActualParticularStageControls.slowStrip)) ActualParticularStageControls.nativeEnvelope (1 / 2 + σ) (ActualParticularStageControls.currentSource (ActualCycleParameters.particularState x) j)

theorem NavierStokes.ActualParticularCycleData.native_envelope_le_one {B N0 : ℕ} (l : Index B N0) (n : ℕ) (z : ActualParticularStageControls.Native) : ActualParticularStageControls.nativeEnvelope (l.2, l.1) n z ≤ 1

theorem NavierStokes.ActualParticularCycleData.native_raw_class {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) : WeightedClasses.MemClass ActualWaveRegularityData.particularFullStrip (fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(ActualWaveRegularityData.particularFullStrip.zeta z)) (1 / 2 + σ) (nativeData x l j).common.amplitude

theorem NavierStokes.ActualParticularCycleData.native_pressure_class {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) : WeightedClasses.MemClass ActualWaveRegularityData.particularFullStrip (fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(ActualWaveRegularityData.particularFullStrip.zeta z)) (1 / 2 + σ + 1 / 2) (nativeData x l j).common.pressure

theorem NavierStokes.ActualParticularCycleData.native_gaussian_class {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) (β : ℝ) : WeightedClasses.MemClass ActualWaveRegularityData.particularFullStrip (fun (x : ℕ) (z : ActualWaveRegularity.ParticularSpace) => √(ActualWaveRegularityData.particularFullStrip.zeta z)) β ((nativeData x l j).globalGaussian (ActualParticularStageControls.canonicalParameters (l.2, l.1)).directions)

theorem NavierStokes.ActualParticularCycleData.native_raw_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((nativeData x l j).common.amplitude n) (ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion)

theorem NavierStokes.ActualParticularCycleData.native_pressure_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((nativeData x l j).common.pressure n) (ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion)

theorem NavierStokes.ActualParticularCycleData.native_gaussian_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((nativeData x l j).globalGaussian (ActualParticularStageControls.canonicalParameters (l.2, l.1)).directions n) (ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion)

theorem NavierStokes.ActualParticularCycleData.native_corrected_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) (n : ℕ) : ContDiffOn ℝ (↑⊤) (((nativeData x l j).commonCorrected ActualWaveRegularityData.particularFullStrip (ActualParticularStageControls.canonicalParameters (l.2, l.1)).directions).amplitude n) (ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion)

theorem NavierStokes.ActualParticularCycleData.source_inactive {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (n : ℕ) (hn : ¬ActualWaveRegularityData.Ordered l n) (j : ℤ) {z : Point} (hz : z ∈ ActualInitialization.geometry.domain) : ParticularWaveAssembly.residualSource (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) j n z = 0

theorem NavierStokes.ActualParticularCycleData.native_source_periodic {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (T : ActualCyclePeriodicity.Periodic x) (l : Index B N0) (j : ℤ) (n : ℕ) (z : ActualParticularStageControls.Native) (hz : z ∈ ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion) : CommonCoverSolve.PeriodicAt ((nativeData x l j).source n) z.1

noncomputable def NavierStokes.ActualParticularCycleData.nativeMode {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) (j : ℤ) : CorrectionState.Oscillation ActualWaveRegularity.Point

Native mode, constructed using ActualWaveRegularity.modeOscillation.

Equations

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

theorem NavierStokes.ActualParticularCycleData.native_mode_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) (hj : j ≠ 0) : WaveStateRegularity.AngularSmooth ActualInitialization.geometry.domain (nativeMode x l j)

theorem NavierStokes.ActualParticularCycleData.native_mode_support {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) (j : ℤ) : WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (nativeMode x l j)

theorem NavierStokes.ActualParticularCycleData.native_mode_periodic {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (T : ActualCyclePeriodicity.Periodic x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (j : ℤ) : CorrectionStep.OscillationPeriodic CorrectionInitialization.ActualPrimary.standardRegion.carrier (nativeMode x l j)

theorem NavierStokes.ActualParticularCycleData.block_eq_modes {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) : (block x l).oscillation = LabelSumBounds.fieldSum (fun (x_1 : ℕ) => ParticularWaveAssembly.modes x.coefficients.residualBand) (nativeMode x l)

theorem NavierStokes.ActualParticularCycleData.block_regular {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (T : ActualCyclePeriodicity.Periodic x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) : WaveStateRegularity.AngularSmooth ActualInitialization.geometry.domain (block x l).oscillation ∧ CorrectionStep.OscillationPeriodic CorrectionInitialization.ActualPrimary.standardRegion.carrier (block x l).oscillation ∧ WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (block x l).oscillation

theorem NavierStokes.ActualParticularCycleData.field_regular {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (T : ActualCyclePeriodicity.Periodic x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) : WaveStateRegularity.AngularSmooth ActualInitialization.geometry.domain ((parameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) ∧ CorrectionStep.OscillationPeriodic CorrectionInitialization.ActualPrimary.standardRegion.carrier ((parameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) ∧ WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b ((parameters B N0).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state)

theorem NavierStokes.ActualParticularCycleData.pair_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} {f : D → ℂ} (hf : ContDiffOn ℝ (↑⊤) f U) (j : ℤ) : HarmonicResidual.SmoothCoefficients U (ErrorHarmonics.conjugatePair j f)

theorem NavierStokes.ActualParticularCycleData.assembled_velocity_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) (hv : ∀ j ∈ ParticularWaveAssembly.modes N, ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (v j n) U) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients U ((ParticularWaveAssembly.assembledBlock N k Φ kp v p).velocity n i)

theorem NavierStokes.ActualParticularCycleData.assembled_pressure_smooth {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {U : Set D} (N : ℕ) (k : ℕ → ℝ) (Φ : ℕ → D → ℝ) (kp : ℕ → ℤ) (v : ℤ → ℕ → D → HarmonicCalculus.ComplexVector) (p : ℤ → ℕ → D → ℂ) (hp : ∀ j ∈ ParticularWaveAssembly.modes N, ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (p j n) U) (n : ℕ) : HarmonicResidual.SmoothCoefficients U ((ParticularWaveAssembly.assembledBlock N k Φ kp v p).pressure n)

noncomputable def NavierStokes.ActualParticularCycleData.associatedDomain : Set (CorrectionStep.CycleSlow × TorusInverse.Plane)

Associated domain, given by ActualCarrierTransport.parameterDomain ×ˢ Set.univ.

Equations

• NavierStokes.ActualParticularCycleData.associatedDomain = NavierStokes.ActualCarrierTransportBase.parameterDomain ×ˢ Set.univ

theorem NavierStokes.ActualParticularCycleData.native_slice_smooth {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ActualParticularStageControls.Native → E} (hf : ContDiffOn ℝ (↑⊤) f (ActualWaveRegularity.nativeDomain ActualWaveRegularity.particularChart CorrectionInitialization.ActualPrimary.standardRegion)) : ContDiffOn ℝ (↑⊤) (fun (z : ActualParticularStageControls.Parameter × TorusInverse.Plane) => f (ParticularWaveAssembly.angleShuffle (z, 0))) associatedDomain

theorem NavierStokes.ActualParticularCycleData.coefficients_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients ActualInitialization.geometry.domain ((block x l).velocity n i)

theorem NavierStokes.ActualParticularCycleData.pressure_coefficients_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) : HarmonicResidual.SmoothCoefficients ActualInitialization.geometry.domain ((block x l).pressure n)

theorem NavierStokes.ActualParticularCycleData.gaussian_coefficients_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients ActualInitialization.geometry.domain ((gaussianBlock x l).velocity n i)

theorem NavierStokes.ActualParticularCycleData.block_eq_output {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) : block x l = ActualParticularStageControls.outputBlock (ActualCycleParameters.particularState x) x.coefficients.residualBand (l.2, l.1)

noncomputable def NavierStokes.ActualParticularCycleData.goodBlock {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : CorrectionState.HarmonicBlock CorrectionStep.CyclePoint

Good block, given by ActualParticularStageControls.outputGood (ActualCycleParameters.particularState x) x.coefficients.residualBand (l.2,l.1).

Equations

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

theorem NavierStokes.ActualParticularCycleData.amplitude_bounds {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 / 2 + σ) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((block x l).velocity n i).coeff j z

theorem NavierStokes.ActualParticularCycleData.pressure_bounds {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (j : ℤ) : LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 + σ) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((block x l).pressure n).coeff j z

theorem NavierStokes.ActualParticularCycleData.good_bounds {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 + σ - 3 * ChartScales.kappa) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((goodBlock x l).velocity n i).coeff j z

theorem NavierStokes.ActualParticularCycleData.gaussian_bounds {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (β : ℝ) (i : Fin 3) (m : ℤ) : LabelSumBounds.UniformClass ActualInitialization.strip (fun (x : ActualCycleParameters.Index B N0) (x_1 : ℕ) (z : ActualInitialization.Point) => √(ActualInitialization.strip.zeta z)) β fun (l : ActualCycleParameters.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((gaussianBlock x l).velocity n i).coeff m z

theorem NavierStokes.ActualParticularCycleData.solenoidal {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) : HarmonicWaveInteraction.ModeSolenoidal ActualInitialization.strip (CorrectionInitialization.ActualPrimary.commonContext B) (block x l)

theorem NavierStokes.ActualParticularCycleData.good_carrier {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : CorrectionStep.SameCarrier (x.coefficients.blocks l) (goodBlock x l)

theorem NavierStokes.ActualParticularCycleData.good_real {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) (l : Index B N0) : ErrorHarmonics.RealBlock (goodBlock x l)

theorem NavierStokes.ActualParticularCycleData.gaussian_eq_cycle {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (l : Index B N0) : gaussianBlock x l = StateReindex.block CorrectionStep.cycleAssoc (ActualParticularDynamics.actualGaussian (ActualCycleParameters.particularState x) (l.2, l.1) x.coefficients.residualBand)

theorem NavierStokes.ActualParticularCycleData.field_cancellation {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (l : Index B N0) (n : ℕ) (z : Point × ℝ) (hz : z.1 ∈ ActualInitialization.strip.domain) : CorrectionStep.linearBlockField (CorrectionInitialization.ActualPrimary.commonContext B) (x.coefficients.blocks l) (block x l) n z + (HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)).oscillation n z = (goodBlock x l).oscillation n z + (gaussianBlock x l).oscillation n z

theorem NavierStokes.ActualParticularCycleData.linear_bounds {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (i : Fin 3) (j : ℤ) : j ≠ 0 → LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 + σ - 3 * ChartScales.kappa) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((HarmonicResidual.residualBlock (CorrectionInitialization.ActualPrimary.commonContext B) x.state (x.coefficients.blocks l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l)).velocity n i).coeff j z + ((HarmonicWaveInteraction.linearGoodBlock (CorrectionInitialization.ActualPrimary.commonContext B) (x.coefficients.blocks l) (block x l) (gaussianBlock x l).velocity).velocity n i).coeff j z

theorem NavierStokes.ActualParticularCycleData.particularBlock_pressure_eq_modes {ι : Type} (p : CorrectionStep.CycleParameters ι) (v : CorrectionStep.CycleCoefficients ι) (c : CorrectionState.Context Point) (u : CorrectionState.State Point) (l : ι) (hf : ∀ (n : ℕ), (v.blocks l).frequency n ≠ 0) : (p.particularBlock v c u l).oscillatoryPressure = fun (n : ℕ) (z : ActualWaveRegularity.Cylinder) => ∑ j ∈ ParticularWaveAssembly.modes v.residualBand, (HarmonicCalculus.mode ((ActualWaveRegularity.particularCopyData p v c u l j).background.frequency n) ((ActualWaveRegularity.particularCopyData p v c u l j).background.phase n) ((ActualWaveRegularity.particularCopyData p v c u l j).common.pressure n) (ActualWaveRegularity.particularChart z)).re

Pressure is assembled from the same actual modes as velocity.

theorem NavierStokes.ActualParticularCycleData.pressure_field_smooth {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (n : ℕ) : ContDiffOn ℝ (↑⊤) ((parameters B N0).particularPressure x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state n) (ActualInitialization.geometry.domain ×ˢ Set.univ)

theorem NavierStokes.ActualParticularCycleData.actual_data {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (T : ActualCyclePeriodicity.Periodic x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (_hσ : 1 / 5 ≤ σ) : Data x σ

Every field is derived for the literal particular construction from the incoming analytic invariant and its separately tracked periods.

theorem NavierStokes.ActualParticularCycleData.actual_inputs {B N0 : ℕ} {σ : ℝ} {x : CorrectionStep.CycleState (Index B N0)} (H : Invariant σ x) (T : ActualCyclePeriodicity.Periodic x) (hN : ActualCarrierGeometry.geometricThreshold ≤ N0) (hσ : 1 / 5 ≤ σ) : ActualParticularMeanGain.Inputs x σ