Physical mean fields glued from their actual valid bands #
Only overlapping valid slow strips are compared. The physical field is defined by a valid-band choice, and its value is proved independent of that choice. Native moving mean classes supply the physical derivative estimates.
Full-fiber coherence through the actual correction recurrence #
All comparisons below retain every radial, free auxiliary and angular
variable. Pressure reconstruction, the temporal inverse and the rank repair
are the literal operations in CorrectionStep.CycleState.step.
@[reducible, inline]
Point: an abbreviation for CorrectionStep.CyclePoint.
Instances For
Fixed physical geometry of the recurrence. The radial exponent, gauge and normalized rank coefficients are constructed from these parameters.
- h : ℝ
Step-size parameter of
Geometry, of typeℝ. - inner : ℝ
Inner of
Geometry, of typeℝ. - outer : ℝ
Outer of
Geometry, of typeℝ. - frequency : ℝ
Frequency of
Geometry, of typeℝ. - rankAmplitude : ℝ
Rank amplitude of
Geometry, of typeℝ. - rankShape : ℝ
Rank shape of
Geometry, of typeℝ. - rankInner : ℝ
Rank inner of
Geometry, of typeℝ. - rankOuter : ℝ
Rank outer of
Geometry, of typeℝ. - operatorInner : ℝ
Operator inner of
Geometry, of typeℝ. - operatorOuter : ℝ
Operator outer of
Geometry, of typeℝ. Index of
Geometry, of typeℕ → ℕ.
Instances For
Gauge, given by VariableGaugeMean.similarityGauge G.h (ChartScales.radialExponent G.h) G.inner G.outer G.frequency G.inner_lt_outer G.index.
Equations
Instances For
Rank, given by RankStateBounds.normalizedData (2 * G.h) (CoordinateAlgebra.A G.h) G.rankAmplitude G.rankShape G.rankInner G.rankOuter.
Equations
Instances For
Operators, given by CommonBaseContext.operators G.h G.index G.operatorInner G.operatorOuter G.operator_lt.
Equations
Instances For
structure
NavierStokes.CycleStateCoherence.Realizes
{ι : Type}
(G : Geometry)
(p : CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
:
Identifications of primitive data, not conclusions about a state.
Instances For
def
NavierStokes.CycleStateCoherence.StateBand
(G : Geometry)
(V : Set Plane)
(n m k : ℕ)
(u : CorrectionState.State Point)
:
State band, given by StateOn (PhysicalMeanDomain.slowDomain V) (bandChartEquiv G.h n m k) (bandVelocityScale G.h n m) (bandScale n m) u u n m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
NavierStokes.CycleStateCoherence.ContextBand
(G : Geometry)
(V : Set Plane)
(n m k : ℕ)
(c : CorrectionState.Context Point)
:
Context band, given by ContextOn (PhysicalMeanDomain.slowDomain V) (bandChartEquiv G.h n m k) (bandVelocityScale G.h n m) (bandScale n m) c c n m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
NavierStokes.CycleStateCoherence.AxisBand
(G : Geometry)
(V : Set Plane)
(n m k : ℕ)
(a : CorrectionStep.AxisymmetricAlias)
:
Axis band as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Finite label sums without equality of the two active sets #
structure
NavierStokes.CycleStateCoherence.WaveOn
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(U : Set D)
(e : D ≃L[ℝ] E)
(c l : ℝ)
(w : CorrectionState.Oscillation D)
(p : CorrectionState.OscillatoryScalar D)
(g : CorrectionState.Oscillation D)
(wr : CorrectionState.Oscillation E)
(pr : CorrectionState.OscillatoryScalar E)
(gr : CorrectionState.Oscillation E)
(n m : ℕ)
:
Primitive wave transport with the velocity, pressure and excluded Gaussian terms in their respective physical units.
Instances For
structure
NavierStokes.CycleStateCoherence.LabelWavesOn
{ι : Type}
(U : Set Point)
(e : Point ≃L[ℝ] Point)
(c l : ℝ)
(labels : ℕ → Finset ι)
(b g : ι → CorrectionState.HarmonicBlock Point)
(n m : ℕ)
:
The support hypotheses concern each omitted label, so different active sets in neighboring bands are permitted.
- wave (i : ι) : WaveOn U e c l (b i).oscillation (b i).oscillatoryPressure (g i).oscillation (b i).oscillation (b i).oscillatoryPressure (g i).oscillation n m
Instances For
theorem
NavierStokes.CycleStateCoherence.LabelWavesOn.sum
{ι : Type}
{U : Set Point}
{e : Point ≃L[ℝ] Point}
{c l : ℝ}
{labels : ℕ → Finset ι}
{b g : ι → CorrectionState.HarmonicBlock Point}
{n m : ℕ}
(H : LabelWavesOn U e c l labels b g n m)
:
WaveOn U e c l (LabelSumBounds.fieldSum labels fun (i : ι) => (b i).oscillation)
(fun (j : ℕ) (x : Point × ℝ) => ∑ i ∈ labels j, (b i).oscillatoryPressure j x)
(LabelSumBounds.fieldSum labels fun (i : ι) => (g i).oscillation)
(LabelSumBounds.fieldSum labels fun (i : ι) => (b i).oscillation)
(fun (j : ℕ) (x : Point × ℝ) => ∑ i ∈ labels j, (b i).oscillatoryPressure j x)
(LabelSumBounds.fieldSum labels fun (i : ι) => (g i).oscillation) n m
Algebraic state operations retain all old errors #
theorem
NavierStokes.CycleStateCoherence.add_wave_on
{D E : Type}
[NormedAddCommGroup D]
[NormedSpace ℝ D]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{U : Set D}
{e : D ≃L[ℝ] E}
{c l : ℝ}
{u : CorrectionState.State D}
{ur : CorrectionState.State E}
{n m : ℕ}
{w g : CorrectionState.Oscillation D}
{p : CorrectionState.OscillatoryScalar D}
{wr gr : CorrectionState.Oscillation E}
{pr : CorrectionState.OscillatoryScalar E}
(H : PhysicalResidualNaturality.StateOn U e c l u ur n m)
(W : WaveOn U e c l w p g wr pr gr n m)
:
PhysicalResidualNaturality.StateOn U e c l
(u.addIncrement CorrectionStep.zeroTriple 0 w p { base := 0, gaussian := g, aliasError := 0 })
(ur.addIncrement CorrectionStep.zeroTriple 0 wr pr { base := 0, gaussian := gr, aliasError := 0 }) n m
theorem
NavierStokes.CycleStateCoherence.refresh_pressure_alias_on
{S T : Type}
[NormedAddCommGroup S]
[NormedSpace ℝ S]
[NormedAddCommGroup T]
[NormedSpace ℝ T]
{U : Set (PressureStream.Lift S)}
{e : PressureStream.Lift S ≃L[ℝ] PressureStream.Lift T}
{c l : ℝ}
{g : VariableGaugeMean.GaugeData S}
{gr : VariableGaugeMean.GaugeData T}
{C : CorrectionState.Context (PressureStream.Lift S)}
{Cr : CorrectionState.Context (PressureStream.Lift T)}
{old current : CorrectionState.State (PressureStream.Lift S)}
{oldr currentr : CorrectionState.State (PressureStream.Lift T)}
{n m : ℕ}
(H : PhysicalResidualNaturality.StateOn U e c l current currentr n m)
(hnew :
∀ x ∈ U,
∀ (theta : ℝ) (i : Fin 3),
VariableGaugeMean.pressureAliasState g C current n (x, theta) i = c * c * l * VariableGaugeMean.pressureAliasState gr Cr currentr m (e x, theta) i)
(hold :
∀ x ∈ U,
∀ (theta : ℝ) (i : Fin 3),
VariableGaugeMean.pressureAliasState g C old n (x, theta) i = c * c * l * VariableGaugeMean.pressureAliasState gr Cr oldr m (e x, theta) i)
:
PhysicalResidualNaturality.StateOn U e c l (CorrectionStep.gaugeRefreshPressureAlias g C old current)
(CorrectionStep.gaugeRefreshPressureAlias gr Cr oldr currentr) n m
All analytic source data come from the incoming primitive fields #
theorem
NavierStokes.CycleStateCoherence.debtRegular_of_primitive
{coord a b : ℝ}
{U : LocalSignedRequest.SlowRegion coord}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(H : MeanStateRegularity.PrimitiveData U a b c u)
(ha : 0 < a)
(hab : a < b)
(n : ℕ)
:
theorem
NavierStokes.CycleStateCoherence.Realizes.inner_pos
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
:
theorem
NavierStokes.CycleStateCoherence.Realizes.exponent_pos
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
:
theorem
NavierStokes.CycleStateCoherence.Realizes.length
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
(n : ℕ)
:
theorem
NavierStokes.CycleStateCoherence.Realizes.gauge_on
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
{V : Set Plane}
(n m k : ℕ)
(hi : G.index n + k = G.index m)
(htime : ∀ s ∈ V, 0 < s.1)
:
GaugeStateCoherence.GaugeOn V (GaugeStateCoherence.bandScale n m) (↑(GaugeStateCoherence.bandSlowEquiv G.h n m)) k
p.gauge p.gauge n m
theorem
NavierStokes.CycleStateCoherence.Realizes.axial_on
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
(n m k : ℕ)
:
((↑(GaugeStateCoherence.bandSlowEquiv G.h n m)).prodMap (TemporalMeanUpdate.coverMap k))
(c.operators.epsilon n • p.axial) = GaugeStateCoherence.bandScale n m • c.operators.epsilon m • p.axial
theorem
NavierStokes.CycleStateCoherence.Realizes.clock_on
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
(n m k : ℕ)
(hi : G.index n + k = G.index m)
:
theorem
NavierStokes.CycleStateCoherence.Realizes.fast_on
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
(n m k : ℕ)
(hi : G.index n + k = G.index m)
:
(GaugeStateCoherence.bandChartEquiv G.h n m k) (c.operators.fastCoefficient n • c.operators.vT) = (GaugeStateCoherence.bandVelocityScale G.h n m * GaugeStateCoherence.bandScale n m) • c.operators.fastCoefficient m • c.operators.vT
theorem
NavierStokes.CycleStateCoherence.Realizes.rank_on
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
(R : Realizes G p c)
{V : Set Plane}
(n m : ℕ)
(htime : ∀ s ∈ V, 0 < s.1)
:
RankStateCoherence.RankOn V (⇑(GaugeStateCoherence.bandSlowEquiv G.h n m)) (GaugeStateCoherence.bandScale n m)
(GaugeStateCoherence.bandVelocityScale G.h n m) p.rank p.rank n m
structure
NavierStokes.CycleStateCoherence.StagePrimitives
{ι : Type}
(G : Geometry)
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(U : LocalSignedRequest.SlowRegion (2 * G.h))
:
Intermediate regularity is a proved consequence of the incoming primitive fields and the two actual covariance changes.
- particular : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c (p.afterParticular v c u)
- signed : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c (p.afterSigned v c u)
- temporal : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c (p.afterTemporal v c u)
- rankGeometry : LocalRankDefect.RankGeometry p.gauge p.rank U.carrier c (p.afterTemporal v c u)
Instances For
theorem
NavierStokes.CycleStateCoherence.stage_primitives
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(R : Realizes G p c)
(H : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c u)
(hX₁ :
∀ (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))
(hX₂ :
∀ (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))
(hg : LocalRankDefect.RankGeometry p.gauge p.rank U.carrier c u)
:
StagePrimitives G p v c u U
theorem
NavierStokes.CycleStateCoherence.reconstruction_and_alias_band
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(R : Realizes G p c)
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
{V : Set Plane}
(hV : IsOpen V)
(hsub : V ⊆ U.carrier)
(n m k : ℕ)
(hi : G.index n + k = G.index m)
(hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv G.h n m)) V U.carrier)
(HC : ContextBand G V n m k c)
(H : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c u)
(HS : StateBand G V n m k u)
:
StateBand G V n m k (VariableGaugeMean.reconstructState p.gauge c u) ∧ ∀ x ∈ PhysicalMeanDomain.slowDomain V,
∀ (theta : ℝ) (i : Fin 3),
VariableGaugeMean.pressureAliasState p.gauge c u n (x, theta) i = GaugeStateCoherence.bandVelocityScale G.h n m * GaugeStateCoherence.bandVelocityScale G.h n m * GaugeStateCoherence.bandScale n m * VariableGaugeMean.pressureAliasState p.gauge c u m ((GaugeStateCoherence.bandChartEquiv G.h n m k) x, theta) i
theorem
NavierStokes.CycleStateCoherence.wave_stage_band
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
(R : Realizes G p c)
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
{V : Set Plane}
(hV : IsOpen V)
(hsub : V ⊆ U.carrier)
(n m k : ℕ)
(hi : G.index n + k = G.index m)
(hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv G.h n m)) V U.carrier)
(HC : ContextBand G V n m k c)
{w g : CorrectionState.Oscillation Point}
{q : CorrectionState.OscillatoryScalar Point}
(H : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c u)
(HS : StateBand G V n m k u)
(hX :
∀ (i j : Fin 3),
GaugeMomentBalances.MovingField U p.gauge.radial.inner p.gauge.radial.outer
(SignedMeanGain.covarianceIncrement u.oscillation w i j))
(HW :
WaveOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv G.h n m k)
(GaugeStateCoherence.bandVelocityScale G.h n m) (GaugeStateCoherence.bandScale n m) w q g w q g n m)
:
StateBand G V n m k (CorrectionStep.gaugeWaveStage p.gauge c u w q { base := 0, gaussian := g, aliasError := 0 })
def
NavierStokes.CycleStateCoherence.ErrorBand
(G : Geometry)
(V : Set Plane)
(n m k : ℕ)
(a : CorrectionState.Oscillation Point)
:
Error band as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
NavierStokes.CycleStateCoherence.CycleWavesOn
{ι : Type}
(G : Geometry)
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(V : Set Plane)
(n m k : ℕ)
:
Only the two actual per-label wave insertions occur in this input. The state, reconstructed pressures and mean increments are not inputs.
- particular : LabelWavesOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv G.h n m k) (GaugeStateCoherence.bandVelocityScale G.h n m) (GaugeStateCoherence.bandScale n m) v.labels (p.particularBlock v c u) (p.particularGaussianBlock v c u) n m
- signed : LabelWavesOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv G.h n m k) (GaugeStateCoherence.bandVelocityScale G.h n m) (GaugeStateCoherence.bandScale n m) v.labels (p.signedBlock v c u) (p.signedGaussianBlock v c u) n m
Instances For
structure
NavierStokes.CycleStateCoherence.CycleTransport
{ι : Type}
(G : Geometry)
(p : CorrectionStep.CycleParameters ι)
(v : CorrectionStep.CycleCoefficients ι)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(V : Set Plane)
(n m k : ℕ)
:
A derived transport certificate for all four literal stages and the three aliases needed by the final pressure-alias replacement.
- particular : StateBand G V n m k (p.afterParticular v c u)
- signed : StateBand G V n m k (p.afterSigned v c u)
- temporal : StateBand G V n m k (p.afterTemporal v c u)
- temporalAlias : ErrorBand G V n m k (VariableGaugeMean.temporalAliasState p.gauge p.timeExponent p.commonIndex c (p.afterSigned v c u))
- oldPressureAlias : ErrorBand G V n m k (VariableGaugeMean.pressureAliasState p.gauge c u)
- currentPressureAlias : ErrorBand G V n m k (VariableGaugeMean.pressureAliasState p.gauge c (p.afterRank v c u))
Instances For
theorem
NavierStokes.CycleStateCoherence.cycle_transport
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
{V : Set Plane}
(R : Realizes G p c)
(hV : IsOpen V)
(hsub : V ⊆ U.carrier)
(n m k : ℕ)
(hi : G.index n + k = G.index m)
(hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv G.h n m)) V U.carrier)
(HC : ContextBand G V n m k c)
(HS : StateBand G V n m k u)
(H : MeanStateRegularity.PrimitiveData U p.gauge.radial.inner p.gauge.radial.outer c u)
(hX₁ :
∀ (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))
(hX₂ :
∀ (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))
(hg : LocalRankDefect.RankGeometry p.gauge p.rank U.carrier c u)
(HW : CycleWavesOn G p v c u V n m k)
:
CycleTransport G p v c u V n m k
theorem
NavierStokes.CycleStateCoherence.CycleTransport.axis
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{V : Set Plane}
{n m k : ℕ}
(H : CycleTransport G p v c u V n m k)
{a : CorrectionStep.AxisymmetricAlias}
(HA : AxisBand G V n m k a)
:
AxisBand G V n m k (p.nextAxisymmetricAlias v c u a)
theorem
NavierStokes.CycleStateCoherence.CycleTransport.step
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{x : CorrectionStep.CycleState ι}
{c : CorrectionState.Context Point}
{V : Set Plane}
{n m k : ℕ}
(H : CycleTransport G p x.coefficients c x.state V n m k)
(HA : AxisBand G V n m k x.axisymmetricAlias)
:
StateBand G V n m k (CorrectionStep.CycleState.step p c x).state ∧ AxisBand G V n m k (CorrectionStep.CycleState.step p c x).axisymmetricAlias
theorem
NavierStokes.CycleStateCoherence.step_labels
{ι : Type}
(p : CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(x : CorrectionStep.CycleState ι)
:
Stored labels and harmonic aliases are never reselected by a cycle.
theorem
NavierStokes.CycleStateCoherence.iterate_labels
{ι : Type}
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(j : ℕ)
:
theorem
NavierStokes.CycleStateCoherence.iterate_aliasCoefficients
{ι : Type}
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(j : ℕ)
:
(CorrectionStep.CycleState.iterate p c seed j).coefficients.aliasCoefficients = seed.coefficients.aliasCoefficients
theorem
NavierStokes.CycleStateCoherence.block_fields_next
{ι : Type}
{G : Geometry}
{p : CorrectionStep.CycleParameters ι}
{v : CorrectionStep.CycleCoefficients ι}
{c : CorrectionState.Context Point}
{u : CorrectionState.State Point}
{V : Set Plane}
{n m k : ℕ}
(HW : CycleWavesOn G p v c u V n m k)
(hc : ∀ (l : ι), CorrectionStep.SameCarrier (v.blocks l) (p.signedBlock v c u l))
(l : ι)
(H :
PhysicalResidualNaturality.BlockFieldsOn (PhysicalMeanDomain.slowDomain V)
(GaugeStateCoherence.bandChartEquiv G.h n m k) (GaugeStateCoherence.bandVelocityScale G.h n m)
(GaugeStateCoherence.bandScale n m) (v.blocks l) (v.blocks l) (v.gaussian l) (v.aliasCoefficients l) (v.gaussian l)
(v.aliasCoefficients l) n m)
:
PhysicalResidualNaturality.BlockFieldsOn (PhysicalMeanDomain.slowDomain V)
(GaugeStateCoherence.bandChartEquiv G.h n m k) (GaugeStateCoherence.bandVelocityScale G.h n m)
(GaugeStateCoherence.bandScale n m) ((p.nextCoefficients v c u).blocks l) ((p.nextCoefficients v c u).blocks l)
((p.nextCoefficients v c u).gaussian l) ((p.nextCoefficients v c u).aliasCoefficients l)
((p.nextCoefficients v c u).gaussian l) ((p.nextCoefficients v c u).aliasCoefficients l) n m
The primitive wave laws also propagate the complete individual harmonic blocks, so they remain available to the next reference solve.
theorem
NavierStokes.CycleStateCoherence.iterate_state_axis
{ι : Type}
(G : Geometry)
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(R : ∀ (j : ℕ), Realizes G (p j) c)
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
{V : Set Plane}
(hV : IsOpen V)
(hsub : V ⊆ U.carrier)
(n m k : ℕ)
(hi : G.index n + k = G.index m)
(hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv G.h n m)) V U.carrier)
(HC : ContextBand G V n m k c)
(HS : StateBand G V n m k seed.state)
(HA : AxisBand G V n m k seed.axisymmetricAlias)
(HP : MeanStateRegularity.PrimitiveData U G.inner G.outer c seed.state)
(HG : LocalRankDefect.RankGeometry G.gauge G.rank U.carrier c seed.state)
(hX₁ :
∀ (j : ℕ),
have x := CorrectionStep.CycleState.iterate p c seed j;
∀ (i l : Fin 3),
GaugeMomentBalances.MovingField U G.inner G.outer
(SignedMeanGain.covarianceIncrement x.state.oscillation ((p j).particularVelocity x.coefficients c x.state) i
l))
(hX₂ :
∀ (j : ℕ),
have x := CorrectionStep.CycleState.iterate p c seed j;
∀ (i l : Fin 3),
GaugeMomentBalances.MovingField U G.inner G.outer
(SignedMeanGain.covarianceIncrement ((p j).afterParticular x.coefficients c x.state).oscillation
((p j).signedVelocity x.coefficients c x.state) i l))
(HW :
∀ (j : ℕ),
have x := CorrectionStep.CycleState.iterate p c seed j;
CycleWavesOn G (p j) x.coefficients c x.state V n m k)
(j : ℕ)
:
StateBand G V n m k (CorrectionStep.CycleState.iterate p c seed j).state ∧ AxisBand G V n m k (CorrectionStep.CycleState.iterate p c seed j).axisymmetricAlias ∧ MeanStateRegularity.PrimitiveData U G.inner G.outer c (CorrectionStep.CycleState.iterate p c seed j).state
One fixed geometry and one fixed slow domain suffice for the entire actual recurrence. Only each stage's two native wave laws and covariance changes are supplied; next-state coherence is proved by induction.
theorem
NavierStokes.CycleStateCoherence.iterate_block_fields
{ι : Type}
(G : Geometry)
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(V : Set Plane)
(n m k : ℕ)
(Hseed :
∀ (l : ι),
PhysicalResidualNaturality.BlockFieldsOn (PhysicalMeanDomain.slowDomain V)
(GaugeStateCoherence.bandChartEquiv G.h n m k) (GaugeStateCoherence.bandVelocityScale G.h n m)
(GaugeStateCoherence.bandScale n m) (seed.coefficients.blocks l) (seed.coefficients.blocks l)
(seed.coefficients.gaussian l) (seed.coefficients.aliasCoefficients l) (seed.coefficients.gaussian l)
(seed.coefficients.aliasCoefficients l) n m)
(HW :
∀ (j : ℕ),
have x := CorrectionStep.CycleState.iterate p c seed j;
CycleWavesOn G (p j) x.coefficients c x.state V n m k)
(hc :
∀ (j : ℕ) (l : ι),
have x := CorrectionStep.CycleState.iterate p c seed j;
CorrectionStep.SameCarrier (x.coefficients.blocks l) ((p j).signedBlock x.coefficients c x.state l))
(j : ℕ)
(l : ι)
:
have x := CorrectionStep.CycleState.iterate p c seed j;
PhysicalResidualNaturality.BlockFieldsOn (PhysicalMeanDomain.slowDomain V)
(GaugeStateCoherence.bandChartEquiv G.h n m k) (GaugeStateCoherence.bandVelocityScale G.h n m)
(GaugeStateCoherence.bandScale n m) (x.coefficients.blocks l) (x.coefficients.blocks l) (x.coefficients.gaussian l)
(x.coefficients.aliasCoefficients l) (x.coefficients.gaussian l) (x.coefficients.aliasCoefficients l) n m
Explicit retention of the current pressure and all temporal aliases #
noncomputable def
NavierStokes.CycleStateCoherence.temporalAliasAt
{ι : Type}
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(j : ℕ)
:
Temporal alias at as an element of Oscillation Point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.CycleStateCoherence.iterate_alias_error
{ι : Type}
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(g : VariableGaugeMean.GaugeData Plane)
(hg : ∀ (j : ℕ), (p j).gauge = g)
(J : ℕ)
:
(CorrectionStep.CycleState.iterate p c seed J).state.errors.aliasError = seed.state.errors.aliasError + ∑ j ∈ Finset.range J, temporalAliasAt p c seed j + (VariableGaugeMean.pressureAliasState g c (CorrectionStep.CycleState.iterate p c seed J).state - VariableGaugeMean.pressureAliasState g c seed.state)
The obsolete pressure alias cancels at every step. The initial alias, every earlier temporal alias, and exactly one current pressure alias are retained with their actual signs. This is an identity of full fields.
theorem
NavierStokes.CycleStateCoherence.iterate_alias_separated
{ι : Type}
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(g : VariableGaugeMean.GaugeData Plane)
(hg : ∀ (j : ℕ), (p j).gauge = g)
(other : CorrectionState.Oscillation Point)
(hseed : seed.state.errors.aliasError = other + VariableGaugeMean.pressureAliasState g c seed.state)
(J : ℕ)
:
(CorrectionStep.CycleState.iterate p c seed J).state.errors.aliasError = other + ∑ j ∈ Finset.range J, temporalAliasAt p c seed j + VariableGaugeMean.pressureAliasState g c (CorrectionStep.CycleState.iterate p c seed J).state
theorem
NavierStokes.CycleStateCoherence.waveOn_of_positive_fibers
(h : ℝ)
(n m k : ℕ)
{V U : Set Plane}
(hmap : Set.MapsTo (⇑(GaugeStateCoherence.bandSlowEquiv h n m)) V U)
(w g : CorrectionState.Oscillation Point)
(q : CorrectionState.OscillatoryScalar Point)
(H :
WaveOn (PhysicalMeanDomain.slowDomain V ∩ {x : PressureStream.Lift Plane | 0 < x.1})
(GaugeStateCoherence.bandChartEquiv h n m k) (GaugeStateCoherence.bandVelocityScale h n m)
(GaugeStateCoherence.bandScale n m) w q g w q g n m)
(hzleft :
∀ x ∈ PhysicalMeanDomain.slowDomain V,
x.1 ≤ 0 → ∀ (theta : ℝ), w n (x, theta) = 0 ∧ q n (x, theta) = 0 ∧ g n (x, theta) = 0)
(hzright :
∀ x ∈ PhysicalMeanDomain.slowDomain U,
x.1 ≤ 0 → ∀ (theta : ℝ), w m (x, theta) = 0 ∧ q m (x, theta) = 0 ∧ g m (x, theta) = 0)
:
WaveOn (PhysicalMeanDomain.slowDomain V) (GaugeStateCoherence.bandChartEquiv h n m k)
(GaugeStateCoherence.bandVelocityScale h n m) (GaugeStateCoherence.bandScale n m) w q g w q g n m
Reference transport on positive radii extends to the entire required fiber when the actual supported wave fields vanish at nonpositive radii. No assertion is inferred from physical-graph equality.
One common index and one band floor for every field in the construction.
Instances For
Common atlas, bundling index, index_le, gap_le.
Equations
- NavierStokes.ActualMeanPhysicalData.commonAtlas h hh N = { index := NavierStokes.CorrectionInitialization.CommonWindow.index h, index_le := ⋯, gap_le := ⋯ }
Instances For
Overlap, given by U ∩ (bandSlowEquiv h n m) ⁻¹' U.
Equations
- NavierStokes.ActualMeanPhysicalData.overlap h U n m = U ∩ ⇑(NavierStokes.GaugeStateCoherence.bandSlowEquiv h n m) ⁻¹' U
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.power_scale_cancel
(hdegree : ℝ)
(n m : ℕ)
:
ChartScales.Q n ^ (-hdegree) * (ChartScales.Q n / ChartScales.Q m) ^ hdegree = ChartScales.Q m ^ (-hdegree)
theorem
NavierStokes.ActualMeanPhysicalData.coverMap_comp
(i k : ℕ)
(Y : Plane)
:
(TemporalMeanUpdate.coverMap k) ((TemporalMeanUpdate.coverMap i) Y) = (TemporalMeanUpdate.coverMap (i + k)) Y
noncomputable def
NavierStokes.ActualMeanPhysicalData.Atlas.family
{h degree : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{f : Scalar}
(H : A.OverlapLaw U degree f)
:
PhysicalMeanJetBounds.CoherentFamily h degree N Δ U ℝ
The physical field is constructed from overlapping valid bands. No reference band is evaluated outside its original slow strip.
Equations
Instances For
Extracting scalar families from actual state overlap #
def
NavierStokes.ActualMeanPhysicalData.Atlas.StateOverlap
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
(U : Set Plane)
(u : CorrectionState.State Point)
:
State overlap as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.StateOverlap.radial
{h : ℝ}
{N Δ : ℕ}
{A : Atlas h N Δ}
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
A.OverlapLaw U (CoordinateAlgebra.A h) u.mean.radial
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.StateOverlap.angular
{h : ℝ}
{N Δ : ℕ}
{A : Atlas h N Δ}
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
A.OverlapLaw U (CoordinateAlgebra.A h) u.mean.angular
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.StateOverlap.axial
{h : ℝ}
{N Δ : ℕ}
{A : Atlas h N Δ}
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
A.OverlapLaw U (CoordinateAlgebra.A h) u.mean.axial
theorem
NavierStokes.ActualMeanPhysicalData.velocityScale_square
(h : ℝ)
(n m : ℕ)
:
GaugeStateCoherence.bandVelocityScale h n m * GaugeStateCoherence.bandVelocityScale h n m = (ChartScales.Q n / ChartScales.Q m) ^ (2 * CoordinateAlgebra.A h)
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.StateOverlap.pressure
{h : ℝ}
{N Δ : ℕ}
{A : Atlas h N Δ}
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
A.OverlapLaw U (2 * CoordinateAlgebra.A h) u.pressure
noncomputable def
NavierStokes.ActualMeanPhysicalData.Atlas.radialFamily
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
PhysicalMeanJetBounds.CoherentFamily h (CoordinateAlgebra.A h) N Δ U ℝ
Radial family, given by A.family H.radial.
Equations
- A.radialFamily H = A.family ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.Atlas.angularFamily
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
PhysicalMeanJetBounds.CoherentFamily h (CoordinateAlgebra.A h) N Δ U ℝ
Angular family, given by A.family H.angular.
Equations
- A.angularFamily H = A.family ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.Atlas.axialFamily
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
PhysicalMeanJetBounds.CoherentFamily h (CoordinateAlgebra.A h) N Δ U ℝ
Axial family, given by A.family H.axial.
Equations
- A.axialFamily H = A.family ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.Atlas.pressureFamily
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{u : CorrectionState.State Point}
(H : A.StateOverlap U u)
:
PhysicalMeanJetBounds.CoherentFamily h (2 * CoordinateAlgebra.A h) N Δ U ℝ
Pressure family, given by A.family H.pressure /-! ## The literal initialized mean and pressure -/ open CorrectionInitialization.ActualPrimary.
Equations
- A.pressureFamily H = A.family ⋯
Instances For
The literal initialized mean and pressure #
Initial atlas, given by commonAtlas h outgoing.data.h_pos.le N.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Initial radial family, given by (initialAtlas N).radialFamily (initialized_overlap B N0 N).
Equations
Instances For
Initial angular family, given by (initialAtlas N).angularFamily (initialized_overlap B N0 N).
Equations
Instances For
Initial axial family, given by (initialAtlas N).axialFamily (initialized_overlap B N0 N).
Equations
Instances For
Initial pressure family, given by (initialAtlas N).pressureFamily (initialized_overlap B N0 N).
Equations
Instances For
Native classes supply the jets; no physical estimate is an input #
theorem
NavierStokes.ActualMeanPhysicalData.initial_nativeJets_of_class
{α : ℝ}
{f : Scalar}
(H :
GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion
CorrectionInitialization.ActualPrimary.commonGauge.radial.inner
CorrectionInitialization.ActualPrimary.commonGauge.radial.outer f)
(hc : WeightedClasses.MeanClass ActualInitialMean.strip α f)
(N : ℕ)
(hN : 1 ≤ N)
:
theorem
NavierStokes.ActualMeanPhysicalData.initialAngular_field_eq
(B N0 N n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu :
(PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((initialAtlas N).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier)
:
theorem
NavierStokes.ActualMeanPhysicalData.initialPressure_field_eq
(B N0 N n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu :
(PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((initialAtlas N).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier)
:
Scalar stream overlap from the actual primitive operators #
def
NavierStokes.ActualMeanPhysicalData.Atlas.ContextOverlap
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
(U : Set Plane)
(c : CorrectionState.Context Point)
:
Context overlap as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
NavierStokes.ActualMeanPhysicalData.Atlas.GaugeOverlap
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
(U : Set Plane)
(g : VariableGaugeMean.GaugeData Plane)
:
Gauge overlap as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.streamScale
(h : ℝ)
(n m : ℕ)
:
GaugeStateCoherence.bandVelocityScale h n m / GaugeStateCoherence.bandScale n m = (ChartScales.Q n / ChartScales.Q m) ^ (CoordinateAlgebra.A h - 1 / 2)
theorem
NavierStokes.ActualMeanPhysicalData.temporalPotential_moving
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(HP : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
(h : ℝ)
(index : ℕ → ℕ)
:
GaugeMomentBalances.MovingField U g.radial.inner g.radial.outer (VariableGaugeMean.temporalPotential g h index c u)
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.temporal_overlap
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
(U : LocalSignedRequest.SlowRegion (2 * h))
(g : VariableGaugeMean.GaugeData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(HC : A.ContextOverlap U.carrier c)
(HS : A.StateOverlap U.carrier u)
(HG : A.GaugeOverlap U.carrier g)
(HP : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(ha : 0 < g.radial.inner)
(hd : 0 < g.radial.exponent)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength (2 * h))
(hfixed : (VariableGaugeMean.reconstructState g c u).pressure = u.pressure)
:
A.OverlapLaw U.carrier (CoordinateAlgebra.A h - 1 / 2) (VariableGaugeMean.temporalPotential g h A.index c u)
theorem
NavierStokes.ActualMeanPhysicalData.rankPotential_moving
{coord : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(r : CorrectionState.RankData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(HG : LocalRankDefect.RankGeometry g r U.carrier c u)
(hell : ∀ (n : ℕ), g.length n = VariableGaugeMean.qLength coord)
:
GaugeMomentBalances.MovingField U g.radial.inner g.radial.outer (VariableGaugeMean.rankPotential g r c u)
def
NavierStokes.ActualMeanPhysicalData.Atlas.RankOverlap
{h : ℝ}
{N Δ : ℕ}
(_A : Atlas h N Δ)
(U : Set Plane)
(r : CorrectionState.RankData Plane)
:
Rank overlap as an element of Prop.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.rank_overlap
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
(U : LocalSignedRequest.SlowRegion (2 * h))
(g : VariableGaugeMean.GaugeData Plane)
(r : CorrectionState.RankData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(HC : A.ContextOverlap U.carrier c)
(HS : A.StateOverlap U.carrier u)
(HG : A.GaugeOverlap U.carrier g)
(HR : A.RankOverlap U.carrier r)
(HP : MeanStateRegularity.PrimitiveData U g.radial.inner g.radial.outer c u)
(HF : LocalRankDefect.RankGeometry g r U.carrier c u)
:
A.OverlapLaw U.carrier (CoordinateAlgebra.A h - 1 / 2) (VariableGaugeMean.rankPotential g r c u)
The actual initial temporal and rank streams #
Initial temporal scalar, constructed using VariableGaugeMean.temporalPotential.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Initial temporal family, given by (initialAtlas N).family (initialTemporal_overlap B N0 N).
Equations
Instances For
Initial rank family, given by (initialAtlas N).family (initialRank_overlap B N0 N).
Equations
Instances For
Stream classes derived from the actual sources #
theorem
NavierStokes.ActualMeanPhysicalData.rankPotential_class
{coord A0 B0 α cL cR : ℝ}
(U : LocalSignedRequest.SlowRegion coord)
(g : VariableGaugeMean.GaugeData Plane)
(r : CorrectionState.RankData Plane)
(c : CorrectionState.Context Point)
(u : CorrectionState.State Point)
(ha : 0 < g.radial.inner)
(hcL : 0 < cL)
(hcR : 0 < cR)
(ε L : ℕ → ℝ)
(hε : ∀ (n : ℕ), 0 < ε n)
(hεone : ∀ (n : ℕ), ε n ≤ 1)
(hL : ∀ (n : ℕ), 1 ≤ L n)
(HG : LocalRankDefect.RankGeometry g r U.carrier c u)
(HP : RankStateBounds.NormalizedParameters coord A0 B0 r U.carrier)
(hB : B0 ≠ 0)
(hleft : g.radial.inner < r.inner)
(hright : r.outer < g.radial.outer)
(HD :
WeightedClasses.UnweightedClass (PhysicalMeanDomain.localSlowStripData U.carrier ⋯ ε L hε hεone hL) α
(CorrectionState.debt c u))
:
WeightedClasses.MeanClass
(LocalSignedRequest.movingStripData U g.radial.inner g.radial.outer cL cR ha hcL hcR ε L hε hεone hL) α
(VariableGaugeMean.rankPotential g r c u)
One atlas for the literal correction recurrence #
structure
NavierStokes.ActualMeanPhysicalData.CycleData
{ι : Type}
(G : CycleStateCoherence.Geometry)
(N Δ : ℕ)
(p : ℕ → CorrectionStep.CycleParameters ι)
(c : CorrectionState.Context Point)
(seed : CorrectionStep.CycleState ι)
(U : LocalSignedRequest.SlowRegion (2 * G.h))
:
The inputs are the seed and the two actual wave insertions per cycle. Mean and pressure overlap at later states is proved from these data.
- realizes (j : ℕ) : CycleStateCoherence.Realizes G (p j) c
- context : self.atlas.ContextOverlap U.carrier c
- seed_state : self.atlas.StateOverlap U.carrier seed.state
- primitive : MeanStateRegularity.PrimitiveData U G.inner G.outer c seed.state
- rank : LocalRankDefect.RankGeometry G.gauge G.rank U.carrier c seed.state
- covariance_particular (j : ℕ) : let x := CorrectionStep.CycleState.iterate p c seed j; ∀ (i l : Fin 3), GaugeMomentBalances.MovingField U G.inner G.outer (SignedMeanGain.covarianceIncrement x.state.oscillation ((p j).particularVelocity x.coefficients c x.state) i l)
- covariance_signed (j : ℕ) : let x := CorrectionStep.CycleState.iterate p c seed j; ∀ (i l : Fin 3), GaugeMomentBalances.MovingField U G.inner G.outer (SignedMeanGain.covarianceIncrement ((p j).afterParticular x.coefficients c x.state).oscillation ((p j).signedVelocity x.coefficients c x.state) i l)
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.at_pair
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(n : ℕ)
(hn : N ≤ n)
(m : ℕ)
(hm : N ≤ m)
(k : ℕ)
(hk : D.atlas.index n + k = D.atlas.index m)
(j : ℕ)
:
CycleStateCoherence.StateBand G (overlap G.h U.carrier n m) n m k (CorrectionStep.CycleState.iterate p c seed j).state ∧ CycleStateCoherence.AxisBand G (overlap G.h U.carrier n m) n m k
(CorrectionStep.CycleState.iterate p c seed j).axisymmetricAlias ∧ MeanStateRegularity.PrimitiveData U G.inner G.outer c (CorrectionStep.CycleState.iterate p c seed j).state
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.state_overlap
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.StateOverlap U.carrier (CorrectionStep.CycleState.iterate p c seed j).state
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.primitives
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
MeanStateRegularity.PrimitiveData U G.inner G.outer c (CorrectionStep.CycleState.iterate p c seed j).state
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.inner_eq
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.outer_eq
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.rank_geometry
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
LocalRankDefect.RankGeometry (p j).gauge (p j).rank U.carrier c (CorrectionStep.CycleState.iterate p c seed j).state
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.stage_primitives
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
CycleStateCoherence.StagePrimitives G (p j) (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state U
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.stage_transport
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j n : ℕ)
(hn : N ≤ n)
(m : ℕ)
(hm : N ≤ m)
(k : ℕ)
(hk : D.atlas.index n + k = D.atlas.index m)
:
CycleStateCoherence.CycleTransport G (p j) (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state (overlap G.h U.carrier n m) n m k
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.radialFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h) N Δ U.carrier ℝ
Radial family, given by D.atlas.radialFamily (D.state_overlap j).
Equations
- D.radialFamily j = D.atlas.radialFamily ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.angularFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h) N Δ U.carrier ℝ
Angular family, given by D.atlas.angularFamily (D.state_overlap j).
Equations
- D.angularFamily j = D.atlas.angularFamily ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.axialFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h) N Δ U.carrier ℝ
Axial family, given by D.atlas.axialFamily (D.state_overlap j).
Equations
- D.axialFamily j = D.atlas.axialFamily ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.pressureFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (2 * CoordinateAlgebra.A G.h) N Δ U.carrier ℝ
Pressure family, given by D.atlas.pressureFamily (D.state_overlap j).
Equations
- D.pressureFamily j = D.atlas.pressureFamily ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.temporalScalar
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(_D : CycleData G N Δ p c seed U)
(j : ℕ)
:
Temporal scalar, constructed using VariableGaugeMean.temporalPotential.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.rankScalar
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(_D : CycleData G N Δ p c seed U)
(j : ℕ)
:
Rank scalar, constructed using VariableGaugeMean.rankPotential.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.gauge_overlap
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.GaugeOverlap U.carrier (p j).gauge
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.rank_overlap_data
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.RankOverlap U.carrier (p j).rank
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.signed_overlap
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.StateOverlap U.carrier
((p j).afterSigned (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state)
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.temporalState_overlap
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.StateOverlap U.carrier
((p j).afterTemporal (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state)
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.temporalScalar_overlap
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.OverlapLaw U.carrier (CoordinateAlgebra.A G.h - 1 / 2) (D.temporalScalar j)
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.rankScalar_overlap
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
D.atlas.OverlapLaw U.carrier (CoordinateAlgebra.A G.h - 1 / 2) (D.rankScalar j)
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.temporalFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h - 1 / 2) N Δ U.carrier ℝ
Temporal family, given by D.atlas.family (D.temporalScalar_overlap j).
Equations
- D.temporalFamily j = D.atlas.family ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.rankFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h - 1 / 2) N Δ U.carrier ℝ
Rank family, given by D.atlas.family (D.rankScalar_overlap j).
Equations
- D.rankFamily j = D.atlas.family ⋯
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.temporal_moving
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
GaugeMomentBalances.MovingField U G.inner G.outer (D.temporalScalar j)
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.rank_moving
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
GaugeMomentBalances.MovingField U G.inner G.outer (D.rankScalar j)
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.reconstructed
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(hseed : (VariableGaugeMean.reconstructState G.gauge c seed.state).pressure = seed.state.pressure)
(j : ℕ)
:
(VariableGaugeMean.reconstructState G.gauge c (CorrectionStep.CycleState.iterate p c seed j).state).pressure = (CorrectionStep.CycleState.iterate p c seed j).state.pressure
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.pressure_moving
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(hseed : (VariableGaugeMean.reconstructState G.gauge c seed.state).pressure = seed.state.pressure)
(j : ℕ)
:
GaugeMomentBalances.MovingField U G.inner G.outer (CorrectionStep.CycleState.iterate p c seed j).state.pressure
Concrete initialization of the overlap-preserving recurrence #
theorem
NavierStokes.ActualMeanPhysicalData.initial_realizes
{ι : Type}
(B : ℕ)
(particular : ι → CorrectionStep.ParticularParameters CorrectionStep.CycleSlow)
(signed : ι → CorrectionStep.PeriodizedSignedParameters CorrectionStep.CyclePoint TorusInverse.Frequency)
:
CycleStateCoherence.Realizes initialGeometry
(CorrectionStep.CycleParameters.ofGeometry ActualInitialization.geometry CorrectionInitialization.ActualPrimary.h
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) ActualInitialization.axial
particular signed CorrectionInitialization.ActualPrimary.rankData)
(CorrectionInitialization.ActualPrimary.commonContext B)
structure
NavierStokes.ActualMeanPhysicalData.InitialCycleInput
(B N0 N : ℕ)
(p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0))
:
Only the actual wave insertions remain inputs. All seed overlap and primitive regularity are supplied by the constructed initialization.
- realizes (j : ℕ) : CycleStateCoherence.Realizes initialGeometry (p j) (CorrectionInitialization.ActualPrimary.commonContext B)
- covariance_particular (j : ℕ) : let x := CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j; ∀ (i l : Fin 3), GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (SignedMeanGain.covarianceIncrement x.state.oscillation ((p j).particularVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) i l)
- covariance_signed (j : ℕ) : let x := CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j; ∀ (i l : Fin 3), GaugeMomentBalances.MovingField CorrectionInitialization.ActualPrimary.standardRegion CorrectionInitialization.ActualPrimary.commonGauge.radial.inner CorrectionInitialization.ActualPrimary.commonGauge.radial.outer (SignedMeanGain.covarianceIncrement ((p j).afterParticular x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state).oscillation ((p j).signedVelocity x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) i l)
- waves (n : ℕ) : n ≥ N → ∀ m ≥ N, ∀ (k : ℕ), CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n + k = CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h m → ∀ (j : ℕ), let x := CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B) (ActualInitialization.initialCycleState B N0) j; CycleStateCoherence.CycleWavesOn initialGeometry (p j) x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state (overlap CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.standardRegion.carrier n m) n m k
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.initialCycleData
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
:
Initial cycle data, bundling atlas, index_eq, realizes, context and the required
compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The actual increments and their single physical representatives #
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.OverlapLaw.add
{h d : ℝ}
{N Δ : ℕ}
{A : Atlas h N Δ}
{U : Set Plane}
{f g : Scalar}
(Hf : A.OverlapLaw U d f)
(Hg : A.OverlapLaw U d g)
:
A.OverlapLaw U d (f + g)
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.OverlapLaw.sub
{h d : ℝ}
{N Δ : ℕ}
{A : Atlas h N Δ}
{U : Set Plane}
{f g : Scalar}
(Hf : A.OverlapLaw U d f)
(Hg : A.OverlapLaw U d g)
:
A.OverlapLaw U d (f - g)
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.streamFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h - 1 / 2) N Δ U.carrier ℝ
Stream family, given by D.atlas.family ((D.temporalScalar_overlap j).add (D.rankScalar_overlap j)).
Equations
- D.streamFamily j = D.atlas.family ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.angularIncrementFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (CoordinateAlgebra.A G.h) N Δ U.carrier ℝ
Angular increment family, given by D.atlas.family (((D.state_overlap (j+1)).angular).sub ((D.state_overlap j).angular)).
Equations
- D.angularIncrementFamily j = D.atlas.family ⋯
Instances For
noncomputable def
NavierStokes.ActualMeanPhysicalData.CycleData.pressureIncrementFamily
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
PhysicalMeanJetBounds.CoherentFamily G.h (2 * CoordinateAlgebra.A G.h) N Δ U.carrier ℝ
Pressure increment family, given by D.atlas.family (((D.state_overlap (j+1)).pressure).sub ((D.state_overlap j).pressure)).
Equations
- D.pressureIncrementFamily j = D.atlas.family ⋯
Instances For
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.angularIncrement_native
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
(D.angularIncrementFamily j).native = ((p j).temporalIncrement (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state).angular + ((p j).rankIncrement (CorrectionStep.CycleState.iterate p c seed j).coefficients c
(CorrectionStep.CycleState.iterate p c seed j).state).angular
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.pressureIncrement_native
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
(D.pressureIncrementFamily j).native = (CorrectionStep.CycleState.iterate p c seed (j + 1)).state.pressure - (CorrectionStep.CycleState.iterate p c seed j).state.pressure
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.angularIncrement_moving
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.pressureIncrement_moving
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(hseed : (VariableGaugeMean.reconstructState G.gauge c seed.state).pressure = seed.state.pressure)
(j : ℕ)
:
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.stream_moving
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
GaugeMomentBalances.MovingField U G.inner G.outer (D.streamFamily j).native
Native quantitative adapters for the actual run #
theorem
NavierStokes.ActualMeanPhysicalData.cycleAngular_nativeJets
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
(hN : 1 ≤ N)
(HC :
CorrectionState.CumulativeBounds ActualInitialMean.strip
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state)
:
theorem
NavierStokes.ActualMeanPhysicalData.cyclePressure_nativeJets
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
(hN : 1 ≤ N)
(HC :
CorrectionState.CumulativeBounds ActualInitialMean.strip
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state)
:
theorem
NavierStokes.ActualMeanPhysicalData.angularIncrement_nativeJets
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
(hN : 1 ≤ N)
{α : ℝ}
(HT :
MeanIncrementBounds.IncrementBounds ActualInitialMean.strip α
((p j).temporalIncrement
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state))
(HR :
MeanIncrementBounds.IncrementBounds ActualInitialMean.strip α
((p j).rankIncrement
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state))
:
theorem
NavierStokes.ActualMeanPhysicalData.pressureIncrement_nativeJets
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
(hN : 1 ≤ N)
{α : ℝ}
(HC :
WeightedClasses.MeanClass ActualInitialMean.strip α
((CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) (j + 1)).state.pressure - (CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state.pressure))
:
Actual Cartesian chart values and curls #
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.field_on_chart
{h d : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{f : Scalar}
(H : A.OverlapLaw U d f)
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
(n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu : (PhysicalMeanJetBounds.graph h n (A.gap n) w).2.1 ∈ U)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
(A.family H).field w = ChartScales.Q n ^ (-d) * f n
(ActualMeanPotentialRealization.chartPoint (PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (A.index n))
(PhysicalCurlCovariance.polarCoordinates a j w))
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.stream_curl
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
(hU : IsOpen U)
{f : Scalar}
(H : A.OverlapLaw U (CoordinateAlgebra.A h - 1 / 2) f)
(hf : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U))
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
(n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu : (PhysicalMeanJetBounds.graph h n (A.gap n) w).2.1 ∈ U)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
SpatialCurl.spatialCurl (A.family H).angularField w = have G := PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (A.index n);
(CyclePhysicalPrefixes.polarVelocityMap a j)
((CyclePhysicalPrefixes.velocityMap G) (ActualMeanPotentialRealization.meridional G (f n))) w
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.angular_field
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{f : Scalar}
(H : A.OverlapLaw U (CoordinateAlgebra.A h) f)
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
(n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu : (PhysicalMeanJetBounds.graph h n (A.gap n) w).2.1 ∈ U)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
(A.family H).angularField w = have G := PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (A.index n);
(CyclePhysicalPrefixes.polarVelocityMap a j)
((CyclePhysicalPrefixes.velocityMap G) fun (x : CyclePhysicalPrefixes.Cylinder) => ![0, f n x.1, 0]) w
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.pressure_field
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{f : Scalar}
(H : A.OverlapLaw U (2 * CoordinateAlgebra.A h) f)
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
(n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu : (PhysicalMeanJetBounds.graph h n (A.gap n) w).2.1 ∈ U)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
(A.family H).field w = have G := PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (A.index n);
(CyclePhysicalPrefixes.polarPressureMap a j)
((CyclePhysicalPrefixes.pressureMap G) fun (x : CyclePhysicalPrefixes.Cylinder) => f n x.1) w
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.family_add_angular
{h d : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{f g : Scalar}
(Hf : A.OverlapLaw U d f)
(Hg : A.OverlapLaw U d g)
:
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.family_sub_angular
{h d : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
{f g : Scalar}
(Hf : A.OverlapLaw U d f)
(Hg : A.OverlapLaw U d g)
:
theorem
NavierStokes.ActualMeanPhysicalData.initialStream_angularField
(B N0 N : ℕ)
:
(initialStreamFamily B N0 N).angularField = (initialTemporalFamily B N0 N).angularField + (initialRankFamily B N0 N).angularField
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.stream_angularField
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.angularIncrement_angularField
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
(D.angularIncrementFamily j).angularField = (D.angularFamily (j + 1)).angularField - (D.angularFamily j).angularField
theorem
NavierStokes.ActualMeanPhysicalData.CycleData.pressureIncrement_field
{ι : Type}
{G : CycleStateCoherence.Geometry}
{N Δ : ℕ}
{p : ℕ → CorrectionStep.CycleParameters ι}
{c : CorrectionState.Context Point}
{seed : CorrectionStep.CycleState ι}
{U : LocalSignedRequest.SlowRegion (2 * G.h)}
(D : CycleData G N Δ p c seed U)
(j : ℕ)
:
Actual temporal-source and measured-debt class inputs #
theorem
NavierStokes.ActualMeanPhysicalData.cycleTemporal_class
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
{α : ℝ}
(HC :
WeightedClasses.MeanClass ActualInitialMean.strip α
(((p j).afterSigned
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state).axialResidual
(CorrectionInitialization.ActualPrimary.commonContext B)))
:
theorem
NavierStokes.ActualMeanPhysicalData.cycleRank_class
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
{α : ℝ}
(HC :
WeightedClasses.UnweightedClass ActualInitialMean.slowStrip α
(CorrectionState.debt (CorrectionInitialization.ActualPrimary.commonContext B)
((p j).afterTemporal
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state)))
:
theorem
NavierStokes.ActualMeanPhysicalData.cycleTemporal_nativeJets
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
(hN : 1 ≤ N)
{α : ℝ}
(HC :
WeightedClasses.MeanClass ActualInitialMean.strip α
(((p j).afterSigned
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state).axialResidual
(CorrectionInitialization.ActualPrimary.commonContext B)))
:
theorem
NavierStokes.ActualMeanPhysicalData.cycleRank_nativeJets
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(j : ℕ)
(hN : 1 ≤ N)
{α : ℝ}
(HC :
WeightedClasses.UnweightedClass ActualInitialMean.slowStrip α
(CorrectionState.debt (CorrectionInitialization.ActualPrimary.commonContext B)
((p j).afterTemporal
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).coefficients
(CorrectionInitialization.ActualPrimary.commonContext B)
(CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) j).state)))
:
The combined mean stream realizes the literal two mean increments #
theorem
NavierStokes.ActualMeanPhysicalData.Atlas.stream_add_curl
{h : ℝ}
{N Δ : ℕ}
(A : Atlas h N Δ)
{U : Set Plane}
(hU : IsOpen U)
{f g : Scalar}
(Hf : A.OverlapLaw U (CoordinateAlgebra.A h - 1 / 2) f)
(Hg : A.OverlapLaw U (CoordinateAlgebra.A h - 1 / 2) g)
(hf : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (f n) (PhysicalMeanDomain.slowDomain U))
(hg : ∀ n ≥ N, ContDiffOn ℝ (↑⊤) (g n) (PhysicalMeanDomain.slowDomain U))
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
(n : ℕ)
(hn : N ≤ n)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu : (PhysicalMeanJetBounds.graph h n (A.gap n) w).2.1 ∈ U)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
SpatialCurl.spatialCurl (A.family ⋯).angularField w = have G := PhysicalResidualBridge.commonGraph (ChartScales.Q n) h (A.index n);
(CyclePhysicalPrefixes.polarVelocityMap a j)
((CyclePhysicalPrefixes.velocityMap G)
(ActualMeanPotentialRealization.meridional G (f n) + ActualMeanPotentialRealization.meridional G (g n)))
w
theorem
NavierStokes.ActualMeanPhysicalData.initialGauge_matches
(B n : ℕ)
:
ActualMeanPotentialRealization.GaugeMatches CorrectionInitialization.ActualPrimary.commonGauge
(CorrectionInitialization.ActualPrimary.commonContext B)
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n))
n
theorem
NavierStokes.ActualMeanPhysicalData.initialStream_curl
(B N0 N n : ℕ)
(hn : N ≤ n)
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu :
(PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((initialAtlas N).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
SpatialCurl.spatialCurl (initialStreamFamily B N0 N).angularField w = (CyclePhysicalPrefixes.polarVelocityMap a j)
((CyclePhysicalPrefixes.velocityMap
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)))
(CyclePhysicalPrefixes.meridionalComponents (ActualInitialCoherence.initialized B N0).mean n))
w
theorem
NavierStokes.ActualMeanPhysicalData.cycleStream_curl
{B N0 N : ℕ}
{p : ℕ → CorrectionStep.CycleParameters (ActualInitialization.Index B N0)}
(H : InitialCycleInput B N0 N p)
(k n : ℕ)
(hn : N ≤ n)
{a : ℝ}
(ha : 0 < a)
(j : PolarCharts.Index)
{w : ProblemStatement.SpaceTime}
(ht : w ∈ PhysicalWaveSum.preterminal)
(hu :
(PhysicalMeanJetBounds.graph CorrectionInitialization.ActualPrimary.h n ((initialAtlas N).gap n) w).2.1 ∈ CorrectionInitialization.ActualPrimary.standardRegion.carrier)
(hw : w ∈ ActualMeanPotentialRealization.cartesianDomain a j)
:
SpatialCurl.spatialCurl ((initialCycleData H).streamFamily k).angularField w = have x :=
CorrectionStep.CycleState.iterate p (CorrectionInitialization.ActualPrimary.commonContext B)
(ActualInitialization.initialCycleState B N0) k;
(CyclePhysicalPrefixes.polarVelocityMap a j)
((CyclePhysicalPrefixes.velocityMap
(PhysicalResidualBridge.commonGraph (ChartScales.Q n) CorrectionInitialization.ActualPrimary.h
(CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h n)))
(CyclePhysicalPrefixes.meridionalComponents
((p k).temporalIncrement x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) n + CyclePhysicalPrefixes.meridionalComponents
((p k).rankIncrement x.coefficients (CorrectionInitialization.ActualPrimary.commonContext B) x.state) n))
w