The actual post-particular mean data

Only the particular wave is needed to prepare the signed request. The common assembly below is independent of a signed family or any signed output estimate.

@[reducible, inline]

abbrev NavierStokes.ActualParticularMeanGain.Point : Type

Point: an abbreviation for ActualInitialization.Point.

Equations

• NavierStokes.ActualParticularMeanGain.Point = NavierStokes.ActualInitialization.Point

@[reducible, inline]

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

Index: an abbreviation for ActualInitialization.Index B N0.

Equations

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

@[reducible, inline]

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

Particular blocks: an abbreviation for (ActualCycleParameters.fixedParameters 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.ActualParticularMeanGain.particularVelocity {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CorrectionState.Oscillation CorrectionStep.CyclePoint

Particular velocity: an abbreviation for (ActualCycleParameters.fixedParameters B N0).particularVelocity 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.ActualParticularMeanGain.particularPressure {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CorrectionState.OscillatoryScalar CorrectionStep.CyclePoint

Particular pressure: an abbreviation for (ActualCycleParameters.fixedParameters B N0).particularPressure 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.ActualParticularMeanGain.particularGaussian {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CorrectionState.Oscillation CorrectionStep.CyclePoint

Particular gaussian: an abbreviation for (ActualCycleParameters.fixedParameters B N0).particularGaussian 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.ActualParticularMeanGain.postParticular {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : CorrectionState.State CorrectionStep.CyclePoint

Post particular: an abbreviation for (ActualCycleParameters.fixedParameters B N0).afterParticular 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.ActualParticularMeanGain.signedRequest {B N0 : ℕ} (x : CorrectionStep.CycleState (Index B N0)) : ℕ → CorrectionStep.CyclePoint × ℝ → SignedWaveUpdate.Vec2

Signed request: an abbreviation for (ActualCycleParameters.fixedParameters B N0).signedRequest 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.ActualParticularMeanGain.label {B N0 : ℕ} (_n : ℕ) (l : Index B N0) : SlotColoring.Label

Label: an abbreviation for ActualPrimaryCovariance.signedLabelOf l.

Equations

• NavierStokes.ActualParticularMeanGain.label _n l = NavierStokes.ActualPrimaryCovariance.signedLabelOf l

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

First-wave data only. These supports use the original selected slots and physical window, independently of the signed output.

• amplitude (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass ActualInitialization.strip ActualInitialization.envelope (1 / 2 + σ) fun (l : ActualInitialization.Index B N0) (n : ℕ) (z : ActualInitialization.Point) => ((particularBlocks x l).velocity n i).coeff j z
• smooth : WaveStateRegularity.AngularSmooth ActualInitialization.geometry.domain (particularVelocity x)
• periodic : CorrectionStep.OscillationPeriodic CorrectionInitialization.ActualPrimary.standardRegion.carrier (particularVelocity x)
• supported : WaveStateRegularity.WaveSupport CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (particularVelocity x)
• old_support : LabelSumBounds.SupportedOscillations CorrectionInitialization.ActualPrimary.slots label ActualPrimaryCovariance.physicalWindow ActualPrimaryCovariance.absoluteAuxiliary ActualInitialization.strip.domain fun (l : Index B N0) => (x.coefficients.blocks l).oscillation
• particular_support : LabelSumBounds.SupportedOscillations CorrectionInitialization.ActualPrimary.slots label ActualPrimaryCovariance.physicalWindow ActualPrimaryCovariance.absoluteAuxiliary ActualInitialization.strip.domain fun (l : Index B N0) => (particularBlocks x l).oscillation

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

All data needed before constructing the signed wave. The covariance and residual estimates are outputs of the actual first-wave update.

• covariance : SignedMeanGain.TensorClass ActualInitialization.strip (1 + σ) (SignedMeanGain.covarianceIncrement x.state.oscillation (particularVelocity x))
• covariance_moving (i j : Fin 3) : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (SignedMeanGain.covarianceIncrement x.state.oscillation (particularVelocity x) i j)
• primitive : MeanStateRegularity.PrimitiveData CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (CorrectionInitialization.ActualPrimary.commonContext B) (postParticular x)
• reconstructed : VariableGaugeMean.reconstructState CorrectionInitialization.ActualPrimary.commonGauge (CorrectionInitialization.ActualPrimary.commonContext B) (postParticular x) = postParticular x
• pressure : WeightedClasses.MeanClass ActualInitialization.strip (1 + σ - ChartScales.kappa) ((postParticular x).pressure - x.state.pressure)
• cumulative : CorrectionState.CumulativeBounds ActualInitialization.strip (postParticular x)
• theta : WeightedClasses.MeanClass ActualInitialization.strip (1 + σ - ChartScales.kappa) ((postParticular x).thetaResidual (CorrectionInitialization.ActualPrimary.commonContext B))
• axial : WeightedClasses.MeanClass ActualInitialization.strip (1 + σ - ChartScales.kappa) ((postParticular x).axialResidual (CorrectionInitialization.ActualPrimary.commonContext B))
• debt : CorrectionState.DefectBounds ActualInitialization.slowStrip (σ - ChartScales.kappa) (CorrectionInitialization.ActualPrimary.commonContext B) (postParticular x)
• request (i : Fin 2) : WeightedClasses.MeanClass (HarmonicWaveInteraction.productStrip ActualInitialization.strip) (σ - ChartScales.kappa) fun (n : ℕ) (z : ActualInitialization.Point × ℝ) => signedRequest x n z i

theorem NavierStokes.ActualParticularMeanGain.covariance_class {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} {σ : ℝ} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (d : Inputs x σ) (hσ : 1 / 5 ≤ σ) : SignedMeanGain.TensorClass ActualInitialization.strip (1 + σ) (SignedMeanGain.covarianceIncrement x.state.oscillation (particularVelocity x))

Quantitative covariance of the literal first update, with uniform constants obtained from the fixed slot assembly.

theorem NavierStokes.ActualParticularMeanGain.covariance_moving {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} {σ : ℝ} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (d : Inputs x σ) (i j : Fin 3) : GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion ActualInitialization.patch.a ActualInitialization.patch.b (SignedMeanGain.covarianceIncrement x.state.oscillation (particularVelocity x) i j)

theorem NavierStokes.ActualParticularMeanGain.postParticular_gain {B N0 : ℕ} {x : CorrectionStep.CycleState (Index B N0)} {σ : ℝ} {S : Index B N0 → ℕ → Set Point} (H : CorrectionStep.CycleAnalyticInvariant ActualInitialization.geometry (CorrectionInitialization.ActualPrimary.commonContext B) ActualInitialization.tangentBlock ActualInitialization.envelope S σ x) (d : Inputs x σ) (hσ : 1 / 5 ≤ σ) : Result x σ

Prepare the actual signed request without any signed-wave estimate or complete four-stage input record.