Analytic preservation for the literal correction cycle #
The wave inputs below are estimates and local identities for the two actual
constructed increments. The full residual, mean, debt, covariance, and
stored-error conclusions are derived for CycleState.step.
Mean composition with the actual signed cross covariance #
The cross covariance need not equal the requested stress on the finitely
many bands before the primary partition is complete. This file retains
its literal difference and its radial divergence. The composition below
has no SignedMeanGain.NativeData input.
@[reducible, inline]
Scalar field: an abbreviation for SignedMeanGain.ScalarField.
Equations
Instances For
noncomputable def
NavierStokes.CrossBasedMeanComposition.crossDefect
(G : SignedMeanGain.Geometry)
(e : ℕ)
(f X : ScalarField Point)
:
The actual averaged cross covariance minus the requested physical stress, before applying the radial divergence.
Equations
Instances For
theorem
NavierStokes.CrossBasedMeanComposition.meanBar_eq_sigma_add_defect
(G : SignedMeanGain.Geometry)
(e : ℕ)
(f X : ScalarField Point)
:
theorem
NavierStokes.CrossBasedMeanComposition.crossDefect_mem_of_cross
(G : SignedMeanGain.Geometry)
(e : ℕ)
(f X : ScalarField Point)
(α : ℝ)
(hcross : MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar X) (SignedMeanGain.physicalSigma G e f))
:
WeightedClasses.MeanClass G.strip α (crossDefect G e f X)
theorem
NavierStokes.CrossBasedMeanComposition.crossDefect_all_exponents_of_tail
(G : SignedMeanGain.Geometry)
(e : ℕ)
(f X : ScalarField Point)
{α : ℝ}
(hbase : WeightedClasses.MeanClass G.strip α (crossDefect G e f X))
(N : ℕ)
(htail :
∀ (n : ℕ), N ≤ n → ∀ x ∈ G.strip.domain, StateMomentBalances.meanBar X n x = SignedMeanGain.physicalSigma G e f n x)
(β : ℝ)
:
WeightedClasses.MeanClass G.strip β (crossDefect G e f X)
A baseline weighted estimate and actual tail agreement suffice for every exponent. The finitely many earlier bands are retained, not set to zero.
theorem
NavierStokes.CrossBasedMeanComposition.cross_cancels_with_defect
(G : SignedMeanGain.Geometry)
(e : ℕ)
(he : e = 2 ∨ e = 1)
{f X : ScalarField Point}
(hf : MeanIncrementBounds.SmoothOn G.domain f)
(hs : ∀ (n : ℕ), LocalSignedRequest.MovingSupport G.patch.a G.patch.b G.coord G.region.carrier (f n))
(hX : SignedMeanGain.MovingField G X)
(hD : MeanIncrementBounds.SmoothOn G.strip.domain (crossDefect G e f X))
(n : ℕ)
{x : Point}
(hx : x ∈ G.strip.domain)
:
StateMomentBalances.meanBar f n x + StateMomentBalances.meanBar (G.operators.radialDiv (↑e) X) n x = SignedMeanGain.removedBump G e f n x + G.operators.radialDiv (↑e) (crossDefect G e f X) n x
The physical cancellation keeps the radial divergence of the actual cross defect. No cancellation on the finite head is assumed.
theorem
NavierStokes.CrossBasedMeanComposition.averaged_residual_decomposition_with_defect
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(w : CorrectionState.Oscillation Point)
(q : CorrectionState.OscillatoryScalar Point)
(gaussian : CorrectionState.Oscillation Point)
(H : SignedMeanGain.LocalData G c u w q gaussian)
(S E : SignedMeanGain.Tensor Point)
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (S i j))
(hE : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (E i j))
(hX : SignedMeanGain.covarianceIncrement u.oscillation w = S + E)
(hDθ : MeanIncrementBounds.SmoothOn G.strip.domain (crossDefect G 2 (u.thetaResidual c) (S 0 1)))
(hDz : MeanIncrementBounds.SmoothOn G.strip.domain (crossDefect G 1 (u.axialResidual c) (S 0 2)))
:
MeanIncrementBounds.Agree G.strip.domain
(StateMomentBalances.meanBar ((SignedMeanGain.waveStage G.gauge c u w q gaussian).thetaResidual c))
(SignedMeanGain.removedBump G 2 (u.thetaResidual c) + StateMomentBalances.meanBar (SignedMeanGain.thetaRemainderField G S E) + G.operators.radialDiv 2 (crossDefect G 2 (u.thetaResidual c) (S 0 1))) ∧ MeanIncrementBounds.Agree G.strip.domain
(StateMomentBalances.meanBar ((SignedMeanGain.waveStage G.gauge c u w q gaussian).axialResidual c))
(SignedMeanGain.removedBump G 1 (u.axialResidual c) + StateMomentBalances.meanBar
(SignedMeanGain.axialRemainderField G S E (SignedMeanGain.pressureChange G.gauge c u w q gaussian)) + G.operators.radialDiv 1 (crossDefect G 1 (u.axialResidual c) (S 0 2)))
Averaging the literal updated residual produces the removed moment bump, the usual covariance/pressure remainder, and the cross defect.
theorem
NavierStokes.CrossBasedMeanComposition.signed_mean_gain_of_cross_defects
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{ι : Type}
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(hσ : 1 / 5 ≤ σ)
(hκ : 0 ≤ κ)
(hκsmall : κ ≤ 1 / 100000)
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(q : CorrectionState.OscillatoryScalar Point)
(gaussian : CorrectionState.Oscillation Point)
(hold : u.oscillation = SignedMeanGain.oldField f a)
(H : SignedMeanGain.LocalData G c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian)
(ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ)
(hX : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.incrementTensor f a i j))
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c))
(hd : CorrectionState.DefectBounds G.slowStrip (σ - κ) c u)
(hDθ :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 2 (u.thetaResidual c) (SignedMeanGain.crossTensor f a 0 1)))
(hDz :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 1 (u.axialResidual c) (SignedMeanGain.crossTensor f a 0 2)))
:
have v :=
SignedMeanGain.waveStage G.gauge c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian;
WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.axialResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (StateMomentBalances.meanBar (v.axialResidual c))
The same four mean gains as the exact-cross theorem, allowing the literal cross defects at the derivative-adjusted gain exponent.
theorem
NavierStokes.CrossBasedMeanComposition.bandSignedStage_mean_debt_of_cross_defects
{ι : Type}
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(hσ : 1 / 5 ≤ σ)
(hκ : 0 ≤ κ)
(hκsmall : κ ≤ 1 / 100000)
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(q : CorrectionState.OscillatoryScalar Point)
(gaussian : CorrectionState.Oscillation Point)
(hold : u.oscillation = SignedMeanGain.oldField f a)
(H : SignedMeanGain.LocalData G c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian)
(ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ)
(hu : CorrectionState.CumulativeBounds G.strip u)
(hbase : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain G.region.carrier) c.base)
(hm : GaugeDebtIncrement.RegularTriple G.region G.patch.a G.patch.b u.mean)
(hW : ∀ (i j : Fin 3), GaugeDebtIncrement.Regular G.region G.patch.a G.patch.b (u.covariance i j))
(hX : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.incrementTensor f a i j))
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c))
(hd : CorrectionState.DefectBounds G.slowStrip (σ - κ) c u)
(hDθ :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 2 (u.thetaResidual c) (SignedMeanGain.crossTensor f a 0 1)))
(hDz :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 1 (u.axialResidual c) (SignedMeanGain.crossTensor f a 0 2)))
:
have v :=
SignedMeanGain.waveStage G.gauge c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian;
WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.pressure - u.pressure) ∧ CorrectionState.CumulativeBounds G.strip v ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.axialResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (CorrectionStep.meanBar (v.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (CorrectionStep.meanBar (v.axialResidual c)) ∧ CorrectionState.DefectBounds G.slowStrip (σ - 2 * κ) c v
Pressure, cumulative, and measured-debt bounds for the actual signed stage. Only the actual cross defect enters, without a native-selection record.
theorem
NavierStokes.CrossBasedMeanComposition.bandSignedStage_mean_debt_of_cross
{ι : Type}
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(hσ : 1 / 5 ≤ σ)
(hκ : 0 ≤ κ)
(hκsmall : κ ≤ 1 / 100000)
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(q : CorrectionState.OscillatoryScalar Point)
(gaussian : CorrectionState.Oscillation Point)
(hold : u.oscillation = SignedMeanGain.oldField f a)
(H : SignedMeanGain.LocalData G c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian)
(ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ)
(hu : CorrectionState.CumulativeBounds G.strip u)
(hbase : MeanIncrementBounds.SmoothTriple (LocalRankDefect.positiveDomain G.region.carrier) c.base)
(hm : GaugeDebtIncrement.RegularTriple G.region G.patch.a G.patch.b u.mean)
(hW : ∀ (i j : Fin 3), GaugeDebtIncrement.Regular G.region G.patch.a G.patch.b (u.covariance i j))
(hX : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.incrementTensor f a i j))
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(hθ : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ - κ) (u.axialResidual c))
(hd : CorrectionState.DefectBounds G.slowStrip (σ - κ) c u)
(hcrossθ :
MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 1))
(SignedMeanGain.physicalSigma G 2 (u.thetaResidual c)))
(hcrossz :
MeanIncrementBounds.Agree G.strip.domain (StateMomentBalances.meanBar (SignedMeanGain.crossTensor f a 0 2))
(SignedMeanGain.physicalSigma G 1 (u.axialResidual c)))
:
have v :=
SignedMeanGain.waveStage G.gauge c u (SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q gaussian;
WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.pressure - u.pressure) ∧ CorrectionState.CumulativeBounds G.strip v ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.axialResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (CorrectionStep.meanBar (v.thetaResidual c)) ∧ WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100) (CorrectionStep.meanBar (v.axialResidual c)) ∧ CorrectionState.DefectBounds G.slowStrip (σ - 2 * κ) c v
Exact cross identities recover the original signed-stage conclusion without the normalized-domain native-selection assumption.
theorem
NavierStokes.CrossBasedMeanComposition.fourStage_mean_gain_of_cross_defects
{ι : Type}
(G : SignedMeanGain.Geometry)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(w₁ : CorrectionState.Oscillation Point)
(q₁ : CorrectionState.OscillatoryScalar Point)
(e₁ : CorrectionState.Oscillation Point)
{P : ι → ℕ → Point → ℝ}
{σ κ : ℝ}
(f : LabelSumBounds.SignedFamily G.strip P (1 / 2) (17 / 25) (1 / 2 + σ - κ) (1 + σ - 2 * κ))
(a : SignedMeanGain.Assembly f)
(q₂ : CorrectionState.OscillatoryScalar Point)
(e₂ : CorrectionState.Oscillation Point)
(hσ : 1 / 5 ≤ σ)
(hκ : 0 ≤ κ)
(hκsmall : κ ≤ 1 / 100000)
(H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u)
(hop : c.operators = G.operators)
(ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ)
(hb : MeanIncrementBounds.BaseBounds G.strip c.base)
(hu : CorrectionState.CumulativeBounds G.strip u)
(hfixed : (VariableGaugeMean.reconstructState G.gauge c u).pressure = u.pressure)
(hmθ : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 2 u.mean.angular n z = 0)
(hmz : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 1 u.mean.axial n z = 0)
(hθ : WeightedClasses.MeanClass G.strip (1 + σ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ) (u.axialResidual c))
(hd : CorrectionState.DefectBounds G.slowStrip σ c u)
(hX₁ :
∀ (i j : Fin 3),
GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b
(SignedMeanGain.covarianceIncrement u.oscillation w₁ i j))
(hX₁class : SignedMeanGain.TensorClass G.strip (1 + σ) (SignedMeanGain.covarianceIncrement u.oscillation w₁))
(hX₂ : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.incrementTensor f a i j))
(hS : ∀ (i j : Fin 3), SignedMeanGain.MovingField G (SignedMeanGain.crossTensor f a i j))
(hold : (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁).oscillation = SignedMeanGain.oldField f a)
(hDθ :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 2 ((SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁).thetaResidual c)
(SignedMeanGain.crossTensor f a 0 1)))
(hDz :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 1 ((SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁).axialResidual c)
(SignedMeanGain.crossTensor f a 0 2)))
(r : CorrectionState.RankData PressureStream.Plane)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(hh : 0 ≤ h)
(hscale : ∀ (n : ℕ), ChartScales.S n ≤ G.slow n)
(gap : ℕ)
(hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + gap)
(hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal))
(hfast : ∀ (n : ℕ), c.operators.fastCoefficient n = ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h))
(hV : LocalRankDefect.IsSlowOn G.region.carrier c.base.angular)
(hG : LocalRankDefect.IsSlowOn G.region.carrier c.base.axial)
(hg :
LocalRankDefect.RankGeometry G.gauge r G.region.carrier c
(VariableGaugeMean.temporalStageState G.gauge h index axial c
(SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂)))
{A₀ B₀ : ℝ}
(hparam : RankStateBounds.NormalizedParameters G.coord A₀ B₀ r G.region.carrier)
(hB : B₀ ≠ 0)
(hleft : G.patch.a < r.inner)
(hright : r.outer < G.patch.b)
:
have t :=
VariableGaugeMean.temporalStageState G.gauge h index axial c
(SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂);
have v := VariableGaugeMean.rankStageState G.gauge r axial c t;
WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
((SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂).thetaResidual
c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
((SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂).axialResidual
c) ∧ CorrectionState.CumulativeBounds G.strip
(SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂) ∧ MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ)
(VariableGaugeMean.temporalIncrementState G.gauge h index axial c
(SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂)) ∧ MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ)
(VariableGaugeMean.rankIncrementState G.gauge r axial c t) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (v.pressure - u.pressure) ∧ CorrectionState.CumulativeBounds G.strip v ∧ CorrectionState.DefectBounds G.slowStrip (σ + 1 / 10) c v ∧ WeightedClasses.MeanClass G.strip (1 + (σ + 1 / 10)) (v.thetaResidual c) ∧ WeightedClasses.MeanClass G.strip (1 + (σ + 1 / 10))
(v.axialResidual c - fun (n : ℕ) (x : PressureStream.Lift SignedMeanGain.Plane) =>
VariableGaugeMean.temporalAliasState G.gauge h index c
(SignedMeanGain.waveStage G.gauge c (SignedMeanGain.waveStage G.gauge c u w₁ q₁ e₁)
(SignedMeanGain.tangentField f a + SignedMeanGain.curlField f a) q₂ e₂)
n (x, 0) 2)
The two actual wave updates, temporal inverse, and rank solve form one mean/debt gain. All intermediate residual and flux regularity is derived from the original primitive fields and the actual covariance increments.
theorem
NavierStokes.CrossBasedMeanComposition.CycleParameters.mean_gain_from_waves_of_cross_defects
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context CorrectionStep.CyclePoint)
(u : CorrectionState.State CorrectionStep.CyclePoint)
(primary : ι → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint)
(P : ι → ℕ → CorrectionStep.CyclePoint → ℝ)
{σ κ : ℝ}
(hσ : 1 / 5 ≤ σ)
(N : ℕ)
(hprimary : ∀ (l : ι), (primary l).BandLimited N)
(hband : CorrectionStep.CoefficientBands v)
(hcp : ∀ (l : ι), CorrectionStep.SameCarrier (v.blocks l) (primary l))
(hcs :
∀ (l : ι),
CorrectionStep.SameCarrier (v.blocks l)
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedBlock v c u l))
(hold :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 / 2) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
((v.blocks l).velocity n i).coeff j x)
(hdiff :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (17 / 25) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
((v.blocks l).velocity n i).coeff j x - ((primary l).velocity n i).coeff j x)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 / 2 + σ) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock v c u
l).velocity
n i).coeff
j x)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 / 2 + σ - κ) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedTangent v c u l).velocity
n i).coeff
j x)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 + σ - 2 * κ) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedCurl v c u l).velocity n
i).coeff
j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ G.strip.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ G.strip.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (v.blocks l).angularFrequency n ≠ 0)
(a :
SignedMeanGain.Assembly
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ N
hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp))
(halabels : a.labels = v.labels)
{axis : CorrectionStep.AxisymmetricAlias}
(hrep : CorrectionStep.CycleRepresentation v u axis)
(hzero : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (v.blocks l))
(hpartzero :
∀ (l : ι),
HarmonicWaveInteraction.ZeroMode
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock v c u l))
(hsold :
LabelSumBounds.SupportedOscillations a.slots a.label a.window a.auxiliary G.strip.domain fun (l : ι) =>
(v.blocks l).oscillation)
(hspart :
LabelSumBounds.SupportedOscillations a.slots a.label a.window a.auxiliary G.strip.domain fun (l : ι) =>
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock v c u
l).oscillation)
(hκ : 0 ≤ κ)
(hκsmall : κ ≤ 1 / 100000)
(H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u)
(hop : c.operators = G.operators)
(ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ)
(hb : MeanIncrementBounds.BaseBounds G.strip c.base)
(hu : CorrectionState.CumulativeBounds G.strip u)
(hfixed : (VariableGaugeMean.reconstructState G.gauge c u).pressure = u.pressure)
(hmθ : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 2 u.mean.angular n z = 0)
(hmz : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 1 u.mean.axial n z = 0)
(hθ : WeightedClasses.MeanClass G.strip (1 + σ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ) (u.axialResidual c))
(hd : CorrectionState.DefectBounds G.slowStrip σ c u)
(hX₁ :
∀ (i j : Fin 3),
GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b
(SignedMeanGain.covarianceIncrement u.oscillation
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularVelocity v c u) i j))
(hX₂ :
∀ (i j : Fin 3),
SignedMeanGain.MovingField G
(SignedMeanGain.incrementTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a i j))
(hS :
∀ (i j : Fin 3),
SignedMeanGain.MovingField G
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a i j))
(hDθ :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 2
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular v c
u).thetaResidual
c)
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a 0 1)))
(hDz :
WeightedClasses.MeanClass G.strip (1 + σ + 17 / 100 + κ)
(crossDefect G 1
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular v c
u).axialResidual
c)
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a 0 2)))
(hh : 0 ≤ h)
(hscale : ∀ (n : ℕ), ChartScales.S n ≤ G.slow n)
(gap : ℕ)
(hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + gap)
(hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal))
(hfast : ∀ (n : ℕ), c.operators.fastCoefficient n = ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h))
(hV : LocalRankDefect.IsSlowOn G.region.carrier c.base.angular)
(hG : LocalRankDefect.IsSlowOn G.region.carrier c.base.axial)
(hg :
LocalRankDefect.RankGeometry G.gauge r G.region.carrier c
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterTemporal v c u))
{A₀ B₀ : ℝ}
(hparam : RankStateBounds.NormalizedParameters G.coord A₀ B₀ r G.region.carrier)
(hB : B₀ ≠ 0)
(hleft : G.patch.a < r.inner)
(hright : r.outer < G.patch.b)
:
WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c u).thetaResidual
c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c u).axialResidual
c) ∧ CorrectionState.CumulativeBounds G.strip
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c u) ∧ MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ)
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).temporalIncrement v c u) ∧ MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ)
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).rankIncrement v c u) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c u).pressure - u.pressure) ∧ CorrectionState.CumulativeBounds G.strip
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c u) ∧ CorrectionState.DefectBounds G.slowStrip (σ + 1 / 10) c
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c u) ∧ WeightedClasses.MeanClass G.strip (1 + (σ + 1 / 10))
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c
u).thetaResidual
c) ∧ WeightedClasses.MeanClass G.strip (1 + (σ + 1 / 10))
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c
u).axialResidual
c - fun (n : ℕ) (x : PressureStream.Lift SignedMeanGain.Plane) =>
VariableGaugeMean.temporalAliasState G.gauge h index c
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c
u)
n (x, 0) 2)
The complete measured-mean gain for next. The signed family is
computed from this cycle's actual particular, tangent, and curl blocks;
its first covariance estimate is derived from the same finite labels.
theorem
NavierStokes.CrossBasedMeanComposition.CycleParameters.mean_gain_from_waves_of_finite_head
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context CorrectionStep.CyclePoint)
(u : CorrectionState.State CorrectionStep.CyclePoint)
(primary : ι → CorrectionState.HarmonicBlock CorrectionStep.CyclePoint)
(P : ι → ℕ → CorrectionStep.CyclePoint → ℝ)
{σ κ : ℝ}
(hσ : 1 / 5 ≤ σ)
(N : ℕ)
(hprimary : ∀ (l : ι), (primary l).BandLimited N)
(hband : CorrectionStep.CoefficientBands v)
(hcp : ∀ (l : ι), CorrectionStep.SameCarrier (v.blocks l) (primary l))
(hcs :
∀ (l : ι),
CorrectionStep.SameCarrier (v.blocks l)
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedBlock v c u l))
(hold :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 / 2) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
((v.blocks l).velocity n i).coeff j x)
(hdiff :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (17 / 25) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
((v.blocks l).velocity n i).coeff j x - ((primary l).velocity n i).coeff j x)
(hpart :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 / 2 + σ) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock v c u
l).velocity
n i).coeff
j x)
(htangent :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 / 2 + σ - κ) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedTangent v c u l).velocity
n i).coeff
j x)
(hcurl :
∀ (i : Fin 3) (j : ℤ),
LabelSumBounds.UniformWaveClass G.strip P (1 + σ - 2 * κ) fun (l : ι) (n : ℕ) (x : SignedMeanGain.Point) =>
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedCurl v c u l).velocity n
i).coeff
j x)
(hP0 : ∀ (l : ι) (n : ℕ), ∀ x ∈ G.strip.domain, 0 ≤ P l n x)
(hP1 : ∀ (l : ι) (n : ℕ), ∀ x ∈ G.strip.domain, P l n x ≤ 1)
(hkp : ∀ (l : ι) (n : ℕ), (v.blocks l).angularFrequency n ≠ 0)
(a :
SignedMeanGain.Assembly
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ N
hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp))
(halabels : a.labels = v.labels)
{axis : CorrectionStep.AxisymmetricAlias}
(hrep : CorrectionStep.CycleRepresentation v u axis)
(hzero : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (v.blocks l))
(hpartzero :
∀ (l : ι),
HarmonicWaveInteraction.ZeroMode
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock v c u l))
(hsold :
LabelSumBounds.SupportedOscillations a.slots a.label a.window a.auxiliary G.strip.domain fun (l : ι) =>
(v.blocks l).oscillation)
(hspart :
LabelSumBounds.SupportedOscillations a.slots a.label a.window a.auxiliary G.strip.domain fun (l : ι) =>
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock v c u
l).oscillation)
(hκ : 0 ≤ κ)
(hκsmall : κ ≤ 1 / 100000)
(H : MeanStateRegularity.PrimitiveData G.region G.patch.a G.patch.b c u)
(hop : c.operators = G.operators)
(ho : MeanIncrementBounds.OperatorBounds G.strip G.operators κ)
(hb : MeanIncrementBounds.BaseBounds G.strip c.base)
(hu : CorrectionState.CumulativeBounds G.strip u)
(hfixed : (VariableGaugeMean.reconstructState G.gauge c u).pressure = u.pressure)
(hmθ : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 2 u.mean.angular n z = 0)
(hmz : ∀ (n : ℕ), ∀ z ∈ G.region.carrier, CorrectionState.radialMoment 1 u.mean.axial n z = 0)
(hθ : WeightedClasses.MeanClass G.strip (1 + σ) (u.thetaResidual c))
(hz : WeightedClasses.MeanClass G.strip (1 + σ) (u.axialResidual c))
(hd : CorrectionState.DefectBounds G.slowStrip σ c u)
(hX₁ :
∀ (i j : Fin 3),
GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b
(SignedMeanGain.covarianceIncrement u.oscillation
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularVelocity v c u) i j))
(hX₂ :
∀ (i j : Fin 3),
SignedMeanGain.MovingField G
(SignedMeanGain.incrementTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a i j))
(hS :
∀ (i j : Fin 3),
SignedMeanGain.MovingField G
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a i j))
{αθ αz : ℝ}
(hDθ :
WeightedClasses.MeanClass G.strip αθ
(crossDefect G 2
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular v c
u).thetaResidual
c)
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a 0 1)))
(hDz :
WeightedClasses.MeanClass G.strip αz
(crossDefect G 1
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular v c
u).axialResidual
c)
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u primary P hσ
N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a 0 2)))
(Ncross : ℕ)
(htailθ :
∀ (n : ℕ),
Ncross ≤ n →
∀ x ∈ G.strip.domain,
StateMomentBalances.meanBar
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u
primary P hσ N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a 0 1)
n x = SignedMeanGain.physicalSigma G 2
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular v c
u).thetaResidual
c)
n x)
(htailz :
∀ (n : ℕ),
Ncross ≤ n →
∀ x ∈ G.strip.domain,
StateMomentBalances.meanBar
(SignedMeanGain.crossTensor
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily v c u
primary P hσ N hprimary hband hcp hcs hold hdiff hpart htangent hcurl hP0 hP1 hkp)
a 0 2)
n x = SignedMeanGain.physicalSigma G 1
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular v c
u).axialResidual
c)
n x)
(hh : 0 ≤ h)
(hscale : ∀ (n : ℕ), ChartScales.S n ≤ G.slow n)
(gap : ℕ)
(hgap : ∀ (n : ℕ), ChartScales.nativeIndex h n ≤ index n + gap)
(hv : c.operators.vT = (0, 0, TorusInverse.vector TorusInverse.Direction.temporal))
(hfast : ∀ (n : ℕ), c.operators.fastCoefficient n = ChartScales.Tg ^ index n * ChartScales.Q n ^ (1 + h))
(hV : LocalRankDefect.IsSlowOn G.region.carrier c.base.angular)
(hG : LocalRankDefect.IsSlowOn G.region.carrier c.base.axial)
(hg :
LocalRankDefect.RankGeometry G.gauge r G.region.carrier c
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterTemporal v c u))
{A₀ B₀ : ℝ}
(hparam : RankStateBounds.NormalizedParameters G.coord A₀ B₀ r G.region.carrier)
(hB : B₀ ≠ 0)
(hleft : G.patch.a < r.inner)
(hright : r.outer < G.patch.b)
:
WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c u).thetaResidual
c) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c u).axialResidual
c) ∧ CorrectionState.CumulativeBounds G.strip
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c u) ∧ MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ)
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).temporalIncrement v c u) ∧ MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ)
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).rankIncrement v c u) ∧ WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ)
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c u).pressure - u.pressure) ∧ CorrectionState.CumulativeBounds G.strip
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c u) ∧ CorrectionState.DefectBounds G.slowStrip (σ + 1 / 10) c
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c u) ∧ WeightedClasses.MeanClass G.strip (1 + (σ + 1 / 10))
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c
u).thetaResidual
c) ∧ WeightedClasses.MeanClass G.strip (1 + (σ + 1 / 10))
(((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next v c
u).axialResidual
c - fun (n : ℕ) (x : PressureStream.Lift SignedMeanGain.Plane) =>
VariableGaugeMean.temporalAliasState G.gauge h index c
((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned v c
u)
n (x, 0) 2)
The complete cycle needs only one baseline class for each cross defect and actual agreement after a fixed band. Finite-head promotion retains its contribution and preserves the original mean/debt gain.
@[reducible, inline]
Point: an abbreviation for CorrectionStep.CyclePoint.
Instances For
structure
NavierStokes.CorrectionAnalyticStep.WaveData
{ι : Type}
(G : SignedMeanGain.Geometry)
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
(σ κ : ℝ)
:
Outputs of the two native constructions, on their literal current source and request. No complete updated residual or mean estimate is an input to this record.
- carrier (l : ι) : CorrectionStep.SameCarrier (v.blocks l) (p.signedBlock v c u l)
- particular (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass p.strip P (1 / 2 + σ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.particularBlock v c u l).velocity n i).coeff j z
- tangent (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass p.strip P (1 / 2 + σ - κ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.signedTangent v c u l).velocity n i).coeff j z
- curl (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass p.strip P (1 + σ - 2 * κ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.signedCurl v c u l).velocity n i).coeff j z
- particularPressure (j : ℤ) : LabelSumBounds.UniformWaveClass p.strip P (1 + σ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.particularBlock v c u l).pressure n).coeff j z
- signedPressure (j : ℤ) : LabelSumBounds.UniformWaveClass p.strip P (1 + σ - κ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.signedBlock v c u l).pressure n).coeff j z
- particularSmooth (l : ι) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients G.domain ((p.particularBlock v c u l).velocity n i)
- signedSmooth (l : ι) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients G.domain ((p.signedBlock v c u l).velocity n i)
- particularPressureSmooth (l : ι) (n : ℕ) : HarmonicResidual.SmoothCoefficients G.domain ((p.particularBlock v c u l).pressure n)
- signedPressureSmooth (l : ι) (n : ℕ) : HarmonicResidual.SmoothCoefficients G.domain ((p.signedBlock v c u l).pressure n)
- particularGaussianSmooth (l : ι) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients G.domain ((p.particularGaussianBlock v c u l).velocity n i)
- signedGaussianSmooth (l : ι) (n : ℕ) (i : Fin 3) : HarmonicResidual.SmoothCoefficients G.domain ((p.signedGaussianBlock v c u l).velocity n i)
- particularSolenoidal (l : ι) : HarmonicWaveInteraction.ModeSolenoidal p.strip c (p.particularBlock v c u l)
- signedSolenoidal (l : ι) : HarmonicWaveInteraction.ModeSolenoidal p.strip c (p.signedBlock v c u l)
- particularSupport (l : ι) : HarmonicSourceSupport.InputSupportOn G.domain (S l) (p.particularBlock v c u l) (p.particularGaussianBlock v c u l).velocity 0
- signedSupport (l : ι) : HarmonicSourceSupport.InputSupportOn G.domain (S l) (p.signedBlock v c u l) (p.signedGaussianBlock v c u l).velocity 0
- particularGaussian (β : ℝ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformClass p.strip (fun (x : ι) (x_1 : ℕ) (z : CorrectionStep.CyclePoint) => √(p.strip.zeta z)) β fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.particularGaussianBlock v c u l).velocity n i).coeff j z
- signedGaussian (β : ℝ) (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformClass p.strip (fun (x : ι) (x_1 : ℕ) (z : CorrectionStep.CyclePoint) => √(p.strip.zeta z)) β fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((p.signedGaussianBlock v c u l).velocity n i).coeff j z
- particularField : WaveStateRegularity.AngularSmooth G.domain (p.particularVelocity v c u)
- signedField : WaveStateRegularity.AngularSmooth G.domain (p.signedVelocity v c u)
- particularPressureField (n : ℕ) : ContDiffOn ℝ (↑⊤) (p.particularPressure v c u n) (G.domain ×ˢ Set.univ)
- signedPressureField (n : ℕ) : ContDiffOn ℝ (↑⊤) (p.signedPressure v c u n) (G.domain ×ˢ Set.univ)
- particularPeriodic : CorrectionStep.OscillationPeriodic G.region.carrier (p.particularVelocity v c u)
- signedPeriodic : CorrectionStep.OscillationPeriodic G.region.carrier (p.signedVelocity v c u)
- particularRadialSupport : WaveStateRegularity.WaveSupport G.region G.patch.a G.patch.b (p.particularVelocity v c u)
- signedRadialSupport : WaveStateRegularity.WaveSupport G.region G.patch.a G.patch.b (p.signedVelocity v c u)
- tangentField : WaveStateRegularity.AngularSmooth G.domain (LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.signedTangent v c u l).oscillation)
- tangentPeriodic : CorrectionStep.OscillationPeriodic G.region.carrier (LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.signedTangent v c u l).oscillation)
- tangentRadialSupport : WaveStateRegularity.WaveSupport G.region G.patch.a G.patch.b (LabelSumBounds.fieldSum v.labels fun (l : ι) => (p.signedTangent v c u l).oscillation)
- particularLinear (i : Fin 3) (j : ℤ) : j ≠ 0 → LabelSumBounds.UniformWaveClass p.strip P (1 + σ - 3 * κ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) => ((HarmonicResidual.residualBlock c u (v.blocks l) (v.gaussian l) (v.aliasCoefficients l)).velocity n i).coeff j z + ((HarmonicWaveInteraction.linearGoodBlock c (v.blocks l) (p.particularBlock v c u l) (p.particularGaussianBlock v c u l).velocity).velocity n i).coeff j z
- signedLinear : UniformHarmonicInteraction.UniformVelocity p.strip P (1 + σ - 4 * κ) fun (l : ι) => HarmonicWaveInteraction.linearGoodBlock c (p.beforeSignedBlock v c u l) (p.signedBlock v c u l) (p.signedGaussianBlock v c u l).velocity
Instances For
theorem
NavierStokes.CorrectionAnalyticStep.WaveData.signed
{ι : Type}
{G : SignedMeanGain.Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{P : ι → ℕ → Point → ℝ}
{S : ι → ℕ → Set Point}
{σ κ : ℝ}
(W : WaveData G p v c u P S σ κ)
(hκ : κ ≤ 1 / 2)
(i : Fin 3)
(j : ℤ)
:
LabelSumBounds.UniformWaveClass p.strip P (1 / 2 + σ - κ) fun (l : ι) (n : ℕ) (z : CorrectionStep.CyclePoint) =>
((p.signedBlock v c u l).velocity n i).coeff j z
The signed exact coefficient is its tangent coefficient plus the literal curl difference.
theorem
NavierStokes.CorrectionAnalyticStep.WaveData.particular_zero_germ
{ι : Type}
{G : SignedMeanGain.Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{P : ι → ℕ → Point → ℝ}
{S : ι → ℕ → Set Point}
{σ κ : ℝ}
(W : WaveData G p v c u P S σ κ)
(hS : ∀ (l : ι) (n : ℕ), IsClosed (S l n))
(l : ι)
(n : ℕ)
{z : Point}
(hz : z ∈ G.domain)
(hn : z ∉ S l n)
(i : Fin 3)
(j : ℤ)
(hj : j ≠ 0)
:
theorem
NavierStokes.CorrectionAnalyticStep.WaveData.signed_zero_germ
{ι : Type}
{G : SignedMeanGain.Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{P : ι → ℕ → Point → ℝ}
{S : ι → ℕ → Set Point}
{σ κ : ℝ}
(W : WaveData G p v c u P S σ κ)
(hS : ∀ (l : ι) (n : ℕ), IsClosed (S l n))
(l : ι)
(n : ℕ)
{z : Point}
(hz : z ∈ G.domain)
(hn : z ∉ S l n)
(i : Fin 3)
(j : ℤ)
(hj : j ≠ 0)
:
theorem
NavierStokes.CorrectionAnalyticStep.WaveData.covariance_moving
{ι : Type}
{G : SignedMeanGain.Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{P : ι → ℕ → Point → ℝ}
{S : ι → ℕ → Set Point}
{σ κ : ℝ}
(W : WaveData G p v c u P S σ κ)
(hu : WaveStateRegularity.AngularSmooth G.domain u.oscillation)
(hup : CorrectionStep.OscillationPeriodic G.region.carrier u.oscillation)
:
(∀ (i j : Fin 3),
GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b
(SignedMeanGain.covarianceIncrement u.oscillation (p.particularVelocity v c u) i j)) ∧ ∀ (i j : Fin 3),
GaugeMomentBalances.MovingField G.region G.patch.a G.patch.b
(SignedMeanGain.covarianceIncrement (p.afterParticular v c u).oscillation (p.signedVelocity v c u) i j)
The two tensor regularity inputs are consequences of the actual finite wave fields, their radial support and their torus periodicity.
structure
NavierStokes.CorrectionAnalyticStep.StaticData
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(κ : ℝ)
:
The fixed geometry and primitive operator data shared by every cycle. The similarity data are identified with the same region, strip and gauge used in the invariant, including the entire radial and free-torus fiber.
- aliasData : ActualCycleExcluded.SimilarityData
Alias data of
StaticData, of typeActualCycleExcluded.SimilarityData. - operators : MeanIncrementBounds.OperatorBounds G.strip c.operators κ
- base : MeanIncrementBounds.BaseBounds G.strip c.base
- angular_slow : LocalRankDefect.IsSlowOn G.region.carrier c.base.angular
- axial_slow : LocalRankDefect.IsSlowOn G.region.carrier c.base.axial
- rankExponent : ℝ
Rank exponent of
StaticData, of typeℝ. - rankCoefficient : ℝ
Rank coefficient of
StaticData, of typeℝ. - rankParameters : RankStateBounds.NormalizedParameters G.coord self.rankExponent self.rankCoefficient r G.region.carrier
Instances For
theorem
NavierStokes.CorrectionAnalyticStep.StaticData.radius_pos
{G : SignedMeanGain.Geometry}
{h : ℝ}
{index : ℕ → ℕ}
{axial : PressureStream.Plane × PressureStream.Plane}
{r : CorrectionState.RankData PressureStream.Plane}
{c : CorrectionState.Context Point}
{κ : ℝ}
(D : StaticData G h index axial r c κ)
{z : Point}
(hz : z ∈ G.strip.domain)
:
theorem
NavierStokes.CorrectionAnalyticStep.StaticData.graph
{G : SignedMeanGain.Geometry}
{h : ℝ}
{index : ℕ → ℕ}
{axial : PressureStream.Plane × PressureStream.Plane}
{r : CorrectionState.RankData PressureStream.Plane}
{c : CorrectionState.Context Point}
{κ : ℝ}
(D : StaticData G h index axial r c κ)
:
∃ (slowTime : PressureStream.Plane × PressureStream.Plane) (temporal : PressureStream.Plane),
c.operators = CorrectionState.graphOperators G.gauge.radial c.operators.epsilon c.operators.fastCoefficient axial slowTime
temporal
theorem
NavierStokes.CorrectionAnalyticStep.StaticData.time_nonneg
{G : SignedMeanGain.Geometry}
{h : ℝ}
{index : ℕ → ℕ}
{axial : PressureStream.Plane × PressureStream.Plane}
{r : CorrectionState.RankData PressureStream.Plane}
{c : CorrectionState.Context Point}
{κ : ℝ}
(D : StaticData G h index axial r c κ)
:
theorem
NavierStokes.CorrectionAnalyticStep.StaticData.slow_scale
{G : SignedMeanGain.Geometry}
{h : ℝ}
{index : ℕ → ℕ}
{axial : PressureStream.Plane × PressureStream.Plane}
{r : CorrectionState.RankData PressureStream.Plane}
{c : CorrectionState.Context Point}
{κ : ℝ}
(D : StaticData G h index axial r c κ)
(n : ℕ)
:
theorem
NavierStokes.CorrectionAnalyticStep.StaticData.index_lower
{G : SignedMeanGain.Geometry}
{h : ℝ}
{index : ℕ → ℕ}
{axial : PressureStream.Plane × PressureStream.Plane}
{r : CorrectionState.RankData PressureStream.Plane}
{c : CorrectionState.Context Point}
{κ : ℝ}
(D : StaticData G h index axial r c κ)
(n : ℕ)
:
theorem
NavierStokes.CorrectionAnalyticStep.StaticData.compatible
{G : SignedMeanGain.Geometry}
{h : ℝ}
{index : ℕ → ℕ}
{axial : PressureStream.Plane × PressureStream.Plane}
{r : CorrectionState.RankData PressureStream.Plane}
{c : CorrectionState.Context Point}
{κ : ℝ}
(D : StaticData G h index axial r c κ)
{ι : Type}
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
:
ActualCycleExcluded.Compatible D.aliasData
(CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c
structure
NavierStokes.CorrectionAnalyticStep.StepData
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(x : CorrectionStep.CycleState ι)
(primary : ι → CorrectionState.HarmonicBlock Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
{σ κ : ℝ}
(D : StaticData G h index axial r c κ)
(H : CorrectionStep.CycleAnalyticInvariant G c primary P S σ x)
(hσ : 1 / 5 ≤ σ)
:
The remaining inputs to one cycle are on its actual native waves and their fixed geometric assembly. The only leading-covariance identity is on a fixed tail; the finite head is retained by the proof.
- waves : WaveData G (CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) x.coefficients c x.state P S σ κ
- primaryBand : ℕ
Primary band of
StepData, of typeℕ. - primary_band (l : ι) : (primary l).BandLimited self.primaryBand
- normal (i : Fin 3) : LocalizedWaveBounds.LocalUnweighted G.strip self.cells 0 fun (n : ℕ) (l : ι) (z : SignedMeanGain.Point) => (HarmonicMeanInteraction.slowNormal c ⋯ ⋯ (x.coefficients.blocks l).phase n z).ofLp i
- frequency : LocalizedWaveBounds.LocalUnweighted G.strip self.cells (-(1 / 2)) fun (n : ℕ) (l : ι) (x_1 : SignedMeanGain.Point) => (x.coefficients.blocks l).frequency n
- angular : LocalizedWaveBounds.LocalUnweighted G.strip self.cells (-(1 / 2)) fun (n : ℕ) (l : ι) (x_1 : SignedMeanGain.Point) => ↑((x.coefficients.blocks l).angularFrequency n)
- assembly : SignedMeanGain.Assembly ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily x.coefficients c x.state primary P hσ self.primaryBand ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯)
Assembly supplied by
StepData. - old_support : LabelSumBounds.SupportedOscillations self.assembly.slots self.assembly.label self.assembly.window self.assembly.auxiliary G.strip.domain fun (l : ι) => (x.coefficients.blocks l).oscillation
- particular_support : LabelSumBounds.SupportedOscillations self.assembly.slots self.assembly.label self.assembly.window self.assembly.auxiliary G.strip.domain fun (l : ι) => ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).particularBlock x.coefficients c x.state l).oscillation
- primary_smooth : WaveStateRegularity.AngularSmooth G.domain (SignedMeanGain.primaryField ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily x.coefficients c x.state primary P hσ self.primaryBand ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯) self.assembly)
- primary_periodic : CorrectionStep.OscillationPeriodic G.region.carrier (SignedMeanGain.primaryField ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily x.coefficients c x.state primary P hσ self.primaryBand ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯) self.assembly)
- rank_geometry : LocalRankDefect.RankGeometry G.gauge r G.region.carrier c x.state
- tailStart : ℕ
Tail start of
StepData, of typeℕ. - cross_tail (n : ℕ) : self.tailStart ≤ n → ∀ z ∈ G.strip.domain, ∀ (i : Fin 2), StateMomentBalances.meanBar (SignedMeanGain.crossTensor ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).signedFamily x.coefficients c x.state primary P hσ self.primaryBand ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯) self.assembly 0 i.succ) n z = LocalSignedRequest.requestedStress G.patch G.coord c ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterParticular x.coefficients c x.state) n z i
Instances For
structure
NavierStokes.CorrectionAnalyticStep.StepResult
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(x : CorrectionStep.CycleState ι)
(primary : ι → CorrectionState.HarmonicBlock Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
{σ κ : ℝ}
:
In addition to preservation, keep the actual increments needed by the physical-stage estimates.
- invariant : CorrectionStep.CycleAnalyticInvariant G c primary P S (σ + 1 / 10) (CorrectionStep.CycleState.step (CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c x)
- temporal : MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ) ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).temporalIncrement x.coefficients c x.state)
- rank : MeanIncrementBounds.IncrementBounds G.strip (1 + σ - 2 * κ) ((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).rankIncrement x.coefficients c x.state)
- pressure : WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).next x.coefficients c x.state).pressure - x.state.pressure)
- velocityCoefficients (i : Fin 3) (j : ℤ) : LabelSumBounds.UniformWaveClass G.strip P (1 / 2 + σ - κ) fun (l : ι) (n : ℕ) (z : SignedMeanGain.Point) => (((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).finalBlock x.coefficients c x.state l).velocity n i).coeff j z - ((x.coefficients.blocks l).velocity n i).coeff j z
- pressureCoefficients (j : ℤ) : LabelSumBounds.UniformWaveClass G.strip P (1 + σ - κ) fun (l : ι) (n : ℕ) (z : SignedMeanGain.Point) => (((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).finalBlock x.coefficients c x.state l).pressure n).coeff j z - ((x.coefficients.blocks l).pressure n).coeff j z
- afterSignedTheta : WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned x.coefficients c x.state).thetaResidual c)
- afterSignedAxial : WeightedClasses.MeanClass G.strip (1 + σ - 2 * κ) (((CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r).afterSigned x.coefficients c x.state).axialResidual c)
Instances For
theorem
NavierStokes.CorrectionAnalyticStep.step
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(x : CorrectionStep.CycleState ι)
(primary : ι → CorrectionState.HarmonicBlock Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
{σ κ : ℝ}
(D : StaticData G h index axial r c κ)
(H : CorrectionStep.CycleAnalyticInvariant G c primary P S σ x)
(hσ : 1 / 5 ≤ σ)
(hκsmall : κ ≤ 1 / 100000)
(d : StepData G h index axial particular signed r c x primary P S D H hσ)
:
StepResult G h index axial particular signed r c x primary P S
The complete analytic step, with actual covariance estimates, finite-head cross defects, temporal/rank reconstruction, and all error bookkeeping derived in the proof.
theorem
NavierStokes.CorrectionAnalyticStep.step_preserves
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(x : CorrectionStep.CycleState ι)
(primary : ι → CorrectionState.HarmonicBlock Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
{σ κ : ℝ}
(D : StaticData G h index axial r c κ)
(H : CorrectionStep.CycleAnalyticInvariant G c primary P S σ x)
(hσ : 1 / 5 ≤ σ)
(hκsmall : κ ≤ 1 / 100000)
(d : StepData G h index axial particular signed r c x primary P S D H hσ)
:
CorrectionStep.CycleAnalyticInvariant G c primary P S (σ + 1 / 10)
(CorrectionStep.CycleState.step (CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c x)
Projection of the complete step estimate to the stored invariant.
theorem
NavierStokes.CorrectionAnalyticStep.iterate_invariant
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(primary : ι → CorrectionState.HarmonicBlock Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
{κ : ℝ}
(D : StaticData G h index axial r c κ)
(σ : ℕ → ℝ)
(hσ : ∀ (n : ℕ), 1 / 5 ≤ σ n)
(hσstep : ∀ (n : ℕ), σ (n + 1) = σ n + 1 / 10)
(hκsmall : κ ≤ 1 / 100000)
(hseed : CorrectionStep.CycleAnalyticInvariant G c primary P S (σ 0) seed)
(data :
(n : ℕ) →
(H :
CorrectionStep.CycleAnalyticInvariant G c primary P S (σ n)
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)) →
StepData G h index axial particular signed r c
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)
primary P S D H ⋯)
(n : ℕ)
:
CorrectionStep.CycleAnalyticInvariant G c primary P S (σ n)
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)
All stages use the same primitive parameters, strip, gauge, carriers, and comparison primary. The supplied data construct each actual wave; they do not assume preservation of the invariant.
theorem
NavierStokes.CorrectionAnalyticStep.iterate_results
{ι : Type}
(G : SignedMeanGain.Geometry)
(h : ℝ)
(index : ℕ → ℕ)
(axial : PressureStream.Plane × PressureStream.Plane)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters Point TorusInverse.Frequency)
(r : CorrectionState.RankData PressureStream.Plane)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(primary : ι → CorrectionState.HarmonicBlock Point)
(P : ι → ℕ → Point → ℝ)
(S : ι → ℕ → Set Point)
{κ : ℝ}
(D : StaticData G h index axial r c κ)
(σ : ℕ → ℝ)
(hσ : ∀ (n : ℕ), 1 / 5 ≤ σ n)
(hσstep : ∀ (n : ℕ), σ (n + 1) = σ n + 1 / 10)
(hκsmall : κ ≤ 1 / 100000)
(hseed : CorrectionStep.CycleAnalyticInvariant G c primary P S (σ 0) seed)
(data :
(n : ℕ) →
(H :
CorrectionStep.CycleAnalyticInvariant G c primary P S (σ n)
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)) →
StepData G h index axial particular signed r c
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)
primary P S D H ⋯)
:
(∀ (n : ℕ),
CorrectionStep.CycleAnalyticInvariant G c primary P S (σ n)
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)) ∧ ∀ (n : ℕ),
StepResult G h index axial particular signed r c
(CorrectionStep.CycleState.iterate
(fun (x : ℕ) => CorrectionStep.CycleParameters.ofGeometry G h index axial particular signed r) c seed n)
primary P S
The same induction also retains the actual increment estimates for each positive physical stage.