The actual angular mean equation along the correction cycle #
The analytic input is on the primitive harmonic coefficients and the actual stream reconstructions. Incompressibility and the angular mean identity are conclusions for the literal stored states.
structure
NavierStokes.CycleMeanEquation.BlockData
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(V : Set D)
(b : CorrectionState.HarmonicBlock D)
:
Local regularity of the actual finite harmonic coefficients.
- phase (n : ℕ) : ContDiffOn ℝ (↑⊤) (b.phase n) V
- pressure (n : ℕ) : HarmonicResidual.SmoothCoefficients V (b.pressure n)
Instances For
theorem
NavierStokes.CycleMeanEquation.BlockData.oscillation
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{V : Set D}
{b : CorrectionState.HarmonicBlock D}
(H : BlockData V b)
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤) (fun (x : D × ℝ) => b.oscillation n x i) (LiftedMeanResidual.cylinder V)
theorem
NavierStokes.CycleMeanEquation.BlockData.oscillatoryPressure
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{V : Set D}
{b : CorrectionState.HarmonicBlock D}
(H : BlockData V b)
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) (b.oscillatoryPressure n) (LiftedMeanResidual.cylinder V)
theorem
NavierStokes.CycleMeanEquation.block_oscillation_periodic
{D : Type}
(V : Set D)
(b : CorrectionState.HarmonicBlock D)
(n : ℕ)
(i : Fin 3)
:
LiftedMeanResidual.PeriodicOn V fun (x : D × ℝ) => b.oscillation n x i
theorem
NavierStokes.CycleMeanEquation.block_pressure_periodic
{D : Type}
(V : Set D)
(b : CorrectionState.HarmonicBlock D)
(n : ℕ)
:
theorem
NavierStokes.CycleMeanEquation.block_pressure_continuous
{D : Type}
(b : CorrectionState.HarmonicBlock D)
(n : ℕ)
(x : D)
:
Continuous fun (θ : ℝ) => b.oscillatoryPressure n (x, θ)
theorem
NavierStokes.CycleMeanEquation.block_pressure_mean_zero
{D : Type}
(b : CorrectionState.HarmonicBlock D)
(hz : ∀ (n : ℕ), (b.pressure n).coeff 0 = 0)
(hk : ∀ (n : ℕ), b.angularFrequency n ≠ 0)
(n : ℕ)
(x : D)
:
theorem
NavierStokes.CycleMeanEquation.ofReal_realDivergence
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
(R : D × ℝ → ℝ)
(Vr Vθ Vz : D × ℝ → D × ℝ)
{v : D × ℝ → Fin 3 → ℝ}
{x : D × ℝ}
(hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => v y i) x)
:
↑(LiftedMeanResidual.realDivergence R Vr Vθ Vz v x) = HarmonicCalculus.cylindricalDivergence R Vr Vθ Vz (fun (y : D × ℝ) (i : Fin 3) => ↑(v y i)) x
The real and complex cylindrical divergence operators agree on the actual real-valued components, including their Fréchet derivatives.
theorem
NavierStokes.CycleMeanEquation.singleMode_zero
{D : Type}
{b : CorrectionState.HarmonicBlock D}
(hz : HarmonicWaveInteraction.ZeroMode b)
(n : ℕ)
:
A zero velocity harmonic also removes its derivative contribution.
theorem
NavierStokes.CycleMeanEquation.block_divergence_zero
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
{b : CorrectionState.HarmonicBlock D}
(H : BlockData s.domain b)
(hz : HarmonicWaveInteraction.ZeroMode b)
(hk : ∀ (n : ℕ), b.angularFrequency n ≠ 0)
(hs : HarmonicWaveInteraction.ModeSolenoidal s c b)
(n : ℕ)
{x : D × ℝ}
(hx : x ∈ LiftedMeanResidual.cylinder s.domain)
:
Per-mode solenoidality implies divergence zero for the actual finite harmonic field. The zero harmonic is controlled explicitly.
theorem
NavierStokes.CycleMeanEquation.realDivergence_sum
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type}
(J : Finset ι)
(R : D × ℝ → ℝ)
(Vr Vθ Vz : D × ℝ → D × ℝ)
(v : ι → D × ℝ → Fin 3 → ℝ)
{x : D × ℝ}
(hv : ∀ j ∈ J, ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : D × ℝ) => v j y i) x)
:
LiftedMeanResidual.realDivergence R Vr Vθ Vz (fun (y : D × ℝ) (i : Fin 3) => ∑ j ∈ J, v j y i) x = ∑ j ∈ J, LiftedMeanResidual.realDivergence R Vr Vθ Vz (v j) x
theorem
NavierStokes.CycleMeanEquation.fieldSum_divergence_zero
{D : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
{ι : Type}
{s : WeightedClasses.StripData D}
{c : CorrectionState.Context D}
(labels : ℕ → Finset ι)
(b : ι → CorrectionState.HarmonicBlock D)
(H : ∀ (l : ι), BlockData s.domain (b l))
(hz : ∀ (l : ι), HarmonicWaveInteraction.ZeroMode (b l))
(hk : ∀ (l : ι) (n : ℕ), (b l).angularFrequency n ≠ 0)
(hs : ∀ (l : ι), HarmonicWaveInteraction.ModeSolenoidal s c (b l))
(n : ℕ)
{x : D × ℝ}
(hx : x ∈ LiftedMeanResidual.cylinder s.domain)
:
LiftedMeanResidual.realDivergence (LiftedMeanResidual.liftScalar c.operators.radius)
(LiftedMeanResidual.radialDirection c n) LiftedMeanResidual.angularDirection (LiftedMeanResidual.axialDirection c n)
(LabelSumBounds.fieldSum labels (fun (l : ι) => (b l).oscillation) n) x = 0
theorem
NavierStokes.CycleMeanEquation.pressureSum_mean_zero
{D ι : Type}
(labels : ℕ → Finset ι)
(b : ι → CorrectionState.HarmonicBlock D)
(hz : ∀ (l : ι) (n : ℕ), ((b l).pressure n).coeff 0 = 0)
(hk : ∀ (l : ι) (n : ℕ), (b l).angularFrequency n ≠ 0)
(n : ℕ)
(x : D)
:
CorrectionState.angularAverage (fun (n : ℕ) (y : D × ℝ) => ∑ l ∈ labels n, (b l).oscillatoryPressure n y) n x = 0
@[reducible, inline]
Point: an abbreviation for CyclePoint.
Instances For
structure
NavierStokes.CycleMeanEquation.StepData
{ι : Type}
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
Inputs on the existing state, the two actual waves, and the primitive stream construction. No outgoing divergence or mean equation is a field.
- domain : p.strip.domain ⊆ LocalRankDefect.positiveDomain U.carrier
- particular_covariance (i j : Fin 3) : GaugeMomentBalances.MovingField U p.gauge.radial.inner p.gauge.radial.outer (SignedMeanGain.covarianceIncrement u.oscillation (p.particularVelocity v c u) i j)
- signed_covariance (i j : Fin 3) : GaugeMomentBalances.MovingField U p.gauge.radial.inner p.gauge.radial.outer (SignedMeanGain.covarianceIncrement (p.afterParticular v c u).oscillation (p.signedVelocity v c u) i j)
- rank : LocalRankDefect.RankGeometry p.gauge p.rank U.carrier c u
- particular_regular (l : ι) : BlockData p.strip.domain (p.particularBlock v c u l)
- signed_regular (l : ι) : BlockData p.strip.domain (p.signedBlock v c u l)
- particular_solenoidal (l : ι) : HarmonicWaveInteraction.ModeSolenoidal p.strip c (p.particularBlock v c u l)
- signed_solenoidal (l : ι) : HarmonicWaveInteraction.ModeSolenoidal p.strip c (p.signedBlock v c u l)
- signed_carrier (l : ι) : CorrectionStep.SameCarrier (v.blocks l) (p.signedBlock v c u l)
Instances For
theorem
NavierStokes.CycleMeanEquation.particular_pressure_zero
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : ι)
(n : ℕ)
:
theorem
NavierStokes.CycleMeanEquation.signed_pressure_zero
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(l : ι)
(n : ℕ)
:
theorem
NavierStokes.CycleMeanEquation.gaugeWaveStage_divergence
(g : VariableGaugeMean.GaugeData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(w : CorrectionState.Oscillation Point)
(q : CorrectionState.OscillatoryScalar Point)
(e : CorrectionState.ExcludedErrors Point)
(n : ℕ)
(x : Point × ℝ)
(hu : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Point × ℝ) => u.totalVelocity c n y i) x)
(hw : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : Point × ℝ) => w n y i) x)
:
CorrectionStep.fullDivergence c (CorrectionStep.gaugeWaveStage g c u w q e) n x = CorrectionStep.fullDivergence c u n x + LiftedMeanResidual.realDivergence (LiftedMeanResidual.liftScalar c.operators.radius)
(LiftedMeanResidual.radialDirection c n) LiftedMeanResidual.angularDirection
(LiftedMeanResidual.axialDirection c n) (w n) x
theorem
NavierStokes.CycleMeanEquation.next_errors_total
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
:
theorem
NavierStokes.CycleMeanEquation.StepData.particular_angular
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(l : ι)
(n : ℕ)
:
theorem
NavierStokes.CycleMeanEquation.StepData.signed_angular
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(l : ι)
(n : ℕ)
:
theorem
NavierStokes.CycleMeanEquation.StepData.particular_smooth
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤) (fun (x : CorrectionStep.CyclePoint × ℝ) => p.particularVelocity v c u n x i)
(LiftedMeanResidual.cylinder p.strip.domain)
theorem
NavierStokes.CycleMeanEquation.StepData.signed_smooth
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤) (fun (x : CorrectionStep.CyclePoint × ℝ) => p.signedVelocity v c u n x i)
(LiftedMeanResidual.cylinder p.strip.domain)
theorem
NavierStokes.CycleMeanEquation.StepData.particular_divergence
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(n : ℕ)
{x : Point × ℝ}
(hx : x ∈ LiftedMeanResidual.cylinder p.strip.domain)
:
theorem
NavierStokes.CycleMeanEquation.StepData.signed_divergence
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(n : ℕ)
{x : Point × ℝ}
(hx : x ∈ LiftedMeanResidual.cylinder p.strip.domain)
:
theorem
NavierStokes.CycleMeanEquation.StepData.next_oscillation_smooth
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(hu :
∀ (n : ℕ) (i : Fin 3),
ContDiffOn ℝ (↑⊤) (fun (x : Point × ℝ) => u.oscillation n x i) (LiftedMeanResidual.cylinder p.strip.domain))
(n : ℕ)
(i : Fin 3)
:
ContDiffOn ℝ (↑⊤) (fun (x : CorrectionStep.CyclePoint × ℝ) => (p.next v c u).oscillation n x i)
(LiftedMeanResidual.cylinder p.strip.domain)
theorem
NavierStokes.CycleMeanEquation.StepData.next_pressure_smooth
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(hu : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.oscillatoryPressure n) (LiftedMeanResidual.cylinder p.strip.domain))
(n : ℕ)
:
ContDiffOn ℝ (↑⊤) ((p.next v c u).oscillatoryPressure n) (LiftedMeanResidual.cylinder p.strip.domain)
theorem
NavierStokes.CycleMeanEquation.StepData.next_oscillation_periodic
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(hu :
∀ (n : ℕ) (i : Fin 3),
LiftedMeanResidual.PeriodicOn p.strip.domain fun (x : CorrectionStep.CyclePoint × ℝ) => u.oscillation n x i)
(n : ℕ)
(i : Fin 3)
:
LiftedMeanResidual.PeriodicOn p.strip.domain fun (x : CorrectionStep.CyclePoint × ℝ) => (p.next v c u).oscillation n x i
theorem
NavierStokes.CycleMeanEquation.StepData.next_pressure_periodic
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(hu : ∀ (n : ℕ), LiftedMeanResidual.PeriodicOn p.strip.domain (u.oscillatoryPressure n))
(n : ℕ)
:
LiftedMeanResidual.PeriodicOn p.strip.domain ((p.next v c u).oscillatoryPressure n)
theorem
NavierStokes.CycleMeanEquation.StepData.next_oscillation_mean_zero
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(hu :
∀ (n : ℕ) (i : Fin 3),
ContDiffOn ℝ (↑⊤) (fun (x : Point × ℝ) => u.oscillation n x i) (LiftedMeanResidual.cylinder p.strip.domain))
(hz :
∀ (n : ℕ),
∀ x ∈ p.strip.domain,
∀ (i : Fin 3), CorrectionState.angularAverage (fun (k : ℕ) (y : Point × ℝ) => u.oscillation k y i) n x = 0)
(n : ℕ)
{x : Point}
(hx : x ∈ p.strip.domain)
(i : Fin 3)
:
CorrectionState.angularAverage (fun (k : ℕ) (y : CorrectionStep.CyclePoint × ℝ) => (p.next v c u).oscillation k y i) n
x = 0
theorem
NavierStokes.CycleMeanEquation.StepData.next_pressure_mean_zero
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(hu : ∀ (n : ℕ), ContDiffOn ℝ (↑⊤) (u.oscillatoryPressure n) (LiftedMeanResidual.cylinder p.strip.domain))
(hz : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, CorrectionState.angularAverage u.oscillatoryPressure n x = 0)
(n : ℕ)
{x : Point}
(hx : x ∈ p.strip.domain)
:
theorem
NavierStokes.CycleMeanEquation.StepData.next_excluded_continuous
{ι : Type}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(hu : ∀ (n : ℕ), ∀ x ∈ p.strip.domain, ∀ (i : Fin 3), Continuous fun (θ : ℝ) => u.errors.total n (x, θ) i)
(n : ℕ)
{x : Point}
(hx : x ∈ p.strip.domain)
(i : Fin 3)
:
theorem
NavierStokes.CycleMeanEquation.meanHypotheses_angularData
{V : Set Point}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : LiftedMeanResidual.MeanHypotheses V c u)
:
theorem
NavierStokes.CycleMeanEquation.StepData.next_angularData
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(HA : ActualInitialMeanEquation.AngularData p.strip.domain u)
:
ActualInitialMeanEquation.AngularData p.strip.domain (p.next v c u)
theorem
NavierStokes.CycleMeanEquation.StepData.next_fullDivergence
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(hu :
∀ (n : ℕ) (i : Fin 3),
ContDiffOn ℝ (↑⊤) (fun (x : Point × ℝ) => u.oscillation n x i) (LiftedMeanResidual.cylinder p.strip.domain))
(n : ℕ)
{x : Point × ℝ}
(hx : x ∈ LiftedMeanResidual.cylinder p.strip.domain)
:
Each wave contributes zero actual divergence; both subsequent mean increments are the genuine divergence-free stream reconstructions.
theorem
NavierStokes.CycleMeanEquation.StepData.next_meanHypotheses
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(HM : LiftedMeanResidual.MeanHypotheses p.strip.domain c u)
:
LiftedMeanResidual.MeanHypotheses p.strip.domain c (p.next v c u)
The complete primitive mean-PDE hypotheses are preserved by the actual four updates, including pressure reconstruction and error refresh.
theorem
NavierStokes.CycleMeanEquation.StepData.next_angularMean_fullGoodResidual
{ι : Type}
{coord : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : StepData U p v c u)
(HM : LiftedMeanResidual.MeanHypotheses p.strip.domain c u)
(n : ℕ)
{x : Point}
(hx : x ∈ p.strip.domain)
(i : Fin 3)
:
CorrectionStep.angularMeanVector (CorrectionStep.fullGoodResidual c (p.next v c u)) n x i = (p.next v c u).meanGoodResidual c n x i
theorem
NavierStokes.CycleMeanEquation.iterate_meanHypotheses
{ι : Type}
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(V : Set Point)
(hV : ∀ (j : ℕ), (p j).strip.domain = V)
(H₀ : LiftedMeanResidual.MeanHypotheses V c seed.state)
(H :
∀ (j : ℕ),
StepData U (p j) (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state)
(j : ℕ)
:
LiftedMeanResidual.MeanHypotheses V c (CorrectionStep.CycleState.iterate p c seed j).state
A fixed local domain is used throughout the actual stored iteration. The step inputs are on its constructed waves and streams, not mean identities.
theorem
NavierStokes.CycleMeanEquation.iterate_divergence_zero
{ι : Type}
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(V : Set Point)
(hV : ∀ (j : ℕ), (p j).strip.domain = V)
(H₀ : LiftedMeanResidual.MeanHypotheses V c seed.state)
(H :
∀ (j : ℕ),
StepData U (p j) (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state)
(j n : ℕ)
{x : Point × ℝ}
(hx : x ∈ LiftedMeanResidual.cylinder V)
:
theorem
NavierStokes.CycleMeanEquation.iterate_angularMean_fullGoodResidual
{ι : Type}
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(V : Set Point)
(hV : ∀ (j : ℕ), (p j).strip.domain = V)
(H₀ : LiftedMeanResidual.MeanHypotheses V c seed.state)
(H :
∀ (j : ℕ),
StepData U (p j) (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state)
(j n : ℕ)
{x : Point}
(hx : x ∈ V)
(i : Fin 3)
:
CorrectionStep.angularMeanVector
(CorrectionStep.fullGoodResidual c (CorrectionStep.CycleState.iterate p c seed j).state) n x i = (CorrectionStep.CycleState.iterate p c seed j).state.meanGoodResidual c n x i
theorem
NavierStokes.CycleMeanEquation.iterate_meanHypotheses_of_initialized
{ι : Type}
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(B N0 : ℕ)
(p : ℕ → CorrectionStep.CycleParameters ι)
(seed : CorrectionStep.CycleState ι)
(hseed : seed.state = ActualInitialCoherence.initialized B N0)
(hV : ∀ (j : ℕ), (p j).strip.domain = ActualInitialMeanEquation.strip.domain)
(H :
∀ (j : ℕ),
StepData U (p j)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) seed j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) seed j).state)
(j : ℕ)
:
Specialization to the literal initializer: its mean-PDE hypotheses come from the proved initialization theorem, not an additional premise.
theorem
NavierStokes.CycleMeanEquation.iterate_angularMean_fullGoodResidual_of_initialized
{ι : Type}
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(B N0 : ℕ)
(p : ℕ → CorrectionStep.CycleParameters ι)
(seed : CorrectionStep.CycleState ι)
(hseed : seed.state = ActualInitialCoherence.initialized B N0)
(hV : ∀ (j : ℕ), (p j).strip.domain = ActualInitialMeanEquation.strip.domain)
(H :
∀ (j : ℕ),
StepData U (p j)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) seed j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) seed j).state)
(j n : ℕ)
{x : Point}
(hx : x ∈ ActualInitialMeanEquation.strip.domain)
(i : Fin 3)
:
CorrectionStep.angularMeanVector
(CorrectionStep.fullGoodResidual (CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) seed j).state)
n x i = (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) seed
j).state.meanGoodResidual
(CorrectionInitialization.ActualPrimary.commonContext B) n x i