Stage estimates for the fixed actual iteration

The native step data and the actual physical field representations are assembled into the finite-stage obligations of the mixed diagonal theorem. No estimate of the output physical residual is an input.

Source indices do not change physical copy fields

noncomputable def NavierStokes.ActualStageEstimates.taggedSource {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {J : Type u_3} {T : Type u_4} (tag : T) (W : PhysicalStageBounds.WaveData h D I K J) : PhysicalStageBounds.WaveData h D (T × I) K J

Add an unused tag to native source indices. The actual copies, their carriers, and their physical fields are unchanged.

Equations

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

@[simp]

theorem NavierStokes.ActualStageEstimates.taggedSource_vector {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {T : Type u_3} (tag : T) (W : PhysicalStageBounds.WaveData h D I K (Fin 3)) : (taggedSource tag W).vector = W.vector

@[simp]

theorem NavierStokes.ActualStageEstimates.taggedSource_pressure {h : ℝ} {D : Type} [NormedAddCommGroup D] [NormedSpace ℝ D] {I : Type u_1} {K : Type u_2} {T : Type u_3} (tag : T) (W : PhysicalStageBounds.WaveData h D I K Unit) : (taggedSource tag W).pressure = W.pressure

One fixed native iteration

noncomputable def NavierStokes.ActualStageEstimates.StepData (B N0 j : ℕ) (H : ActualCyclePreservation.Invariant (ActualIterationLedger.sigma j) (ActualCyclePreservation.state B N0 j)) : Type

Step data, constructed using CorrectionAnalyticStep.StepData.

Equations

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

structure NavierStokes.ActualStageEstimates.RunData (B N0 : ℕ) : Type

All data refer to the same fixed parameters and actual initial state. The step record contains native wave constructions; it is not a physical stage-bound or residual-bound oracle.

• invariant (j : ℕ) : ActualCyclePreservation.Invariant (ActualIterationLedger.sigma j) (ActualCyclePreservation.state B N0 j)
• step (j : ℕ) : StepData B N0 j ⋯

  Step of RunData, of type ∀ j, StepData B N0 j (invariant j).

• particular (j : ℕ) : ActualParticularMeanGain.Inputs (ActualCyclePreservation.state B N0 j) (ActualIterationLedger.sigma j)

theorem NavierStokes.ActualStageEstimates.RunData.result {B N0 : ℕ} (R : RunData B N0) (j : ℕ) : CorrectionAnalyticStep.StepResult ActualInitialization.geometry CorrectionInitialization.ActualPrimary.h (CorrectionInitialization.CommonWindow.index CorrectionInitialization.ActualPrimary.h) ActualInitialization.axial (fun (l : ActualCycleParameters.Index B N0) => ActualParticularStageControls.canonicalParameters ((ActualCycleParameters.swap B N0) l)) ActualSignedStageControls.parameters CorrectionInitialization.ActualPrimary.rankData (CorrectionInitialization.ActualPrimary.commonContext B) (ActualCyclePreservation.state B N0 j) ActualInitialization.tangentBlock ActualInitialization.envelope ActualCoreSupport.refinedCarrier

theorem NavierStokes.ActualStageEstimates.RunData.rank_class {B N0 : ℕ} (R : RunData B N0) (j : ℕ) : WeightedClasses.UnweightedClass ActualInitialization.slowStrip (1 + ActualIterationLedger.sigma j - 2 * ChartScales.kappa) (CorrectionState.debt (CorrectionInitialization.ActualPrimary.commonContext B) (ActualIntermediateDebtBounds.postTemporal (ActualCyclePreservation.state B N0 j)))

theorem NavierStokes.ActualStageEstimates.nativeMean_eq_ledger (j : ℕ) : 1 + ActualIterationLedger.sigma j - 2 * ChartScales.kappa = ActualIterationLedger.meanNative ChartScales.kappa (j + 1)

theorem NavierStokes.ActualStageEstimates.nativePotential_eq_ledger (j : ℕ) : 1 / 2 + ActualIterationLedger.sigma j - ChartScales.kappa = ActualIterationLedger.waveNative ChartScales.kappa (j + 1)

theorem NavierStokes.ActualStageEstimates.nativePressure_eq_ledger (j : ℕ) : 1 + ActualIterationLedger.sigma j - ChartScales.kappa = ActualIterationLedger.wavePressureNative ChartScales.kappa (j + 1)

noncomputable def NavierStokes.ActualStageEstimates.temporalInput {B N0 N : ℕ} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (j : ℕ) : ActualPhysicalStageBounds.MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2)

Temporal input, given by actualCycleTemporalInput M j hN (R.result j).afterSignedAxial.

Equations

• NavierStokes.ActualStageEstimates.temporalInput R M hN j = NavierStokes.ActualPhysicalStageBounds.actualCycleTemporalInput M j hN ⋯

noncomputable def NavierStokes.ActualStageEstimates.rankInput {B N0 N : ℕ} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (j : ℕ) : ActualPhysicalStageBounds.MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h - 1 / 2)

Rank input, given by actualCycleRankInput M j hN (R.rank_class j).

Equations

• NavierStokes.ActualStageEstimates.rankInput R M hN j = NavierStokes.ActualPhysicalStageBounds.actualCycleRankInput M j hN ⋯

noncomputable def NavierStokes.ActualStageEstimates.angularInput {B N0 N : ℕ} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (j : ℕ) : ActualPhysicalStageBounds.MeanInput CorrectionInitialization.ActualPrimary.h (CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

Angular input, given by actualCycleAngularInput M j hN (R.result j).temporal (R.result j).rank.

Equations

• NavierStokes.ActualStageEstimates.angularInput R M hN j = NavierStokes.ActualPhysicalStageBounds.actualCycleAngularInput M j hN ⋯ ⋯

noncomputable def NavierStokes.ActualStageEstimates.pressureInput {B N0 N : ℕ} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (j : ℕ) : ActualPhysicalStageBounds.MeanInput CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

Pressure input, given by actualCyclePressureInput M j hN (R.result j).pressure /-! ## Actual wave records and their native exponents -/.

Equations

• NavierStokes.ActualStageEstimates.pressureInput R M hN j = NavierStokes.ActualPhysicalStageBounds.actualCyclePressureInput M j hN ⋯

Actual wave records and their native exponents

structure NavierStokes.ActualStageEstimates.WaveInputs (DP : Type) [NormedAddCommGroup DP] [NormedSpace ℝ DP] (IP : Type u_1) (KP : Type u_2) (DS : Type) [NormedAddCommGroup DS] [NormedSpace ℝ DS] (IS : Type u_3) (KS : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

Wave inputs data, collecting particularPotential, signedPotential, particularPressure, signedPressure, particularPotential_exponent, signedPotential_exponent and their compatibility conditions.

• particularPotential : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP (Fin 3 × IP) KP (Fin 3)

  Particular potential of WaveInputs, of type ℕ → PhysicalStageBounds.WaveData h DP (Fin 3 × IP) KP (Fin 3).

• signedPotential : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DS (Fin 3 × IS) KS (Fin 3)

  Signed potential of WaveInputs, of type ℕ → PhysicalStageBounds.WaveData h DS (Fin 3 × IS) KS (Fin 3).

• particularPressure : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP IP KP Unit

  Particular pressure of WaveInputs, of type ℕ → PhysicalStageBounds.WaveData h DP IP KP Unit.

• signedPressure : ℕ → PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DS IS KS Unit

  Signed pressure of WaveInputs, of type ℕ → PhysicalStageBounds.WaveData h DS IS KS Unit.

• particularPotential_exponent (j : ℕ) : 1 / 2 + ActualIterationLedger.sigma j - ChartScales.kappa ≤ (self.particularPotential j).alpha
• signedPotential_exponent (j : ℕ) : 1 / 2 + ActualIterationLedger.sigma j - ChartScales.kappa ≤ (self.signedPotential j).alpha
• particularPressure_exponent (j : ℕ) : 1 + ActualIterationLedger.sigma j - ChartScales.kappa ≤ (self.particularPressure j).alpha
• signedPressure_exponent (j : ℕ) : 1 + ActualIterationLedger.sigma j - ChartScales.kappa ≤ (self.signedPressure j).alpha
• particularPotential_shift (j : ℕ) : (self.particularPotential j).shift = -CorrectionInitialization.ActualPrimary.h
• signedPotential_shift (j : ℕ) : (self.signedPotential j).shift = -CorrectionInitialization.ActualPrimary.h
• particularPressure_shift (j : ℕ) : (self.particularPressure j).shift = -(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)
• signedPressure_shift (j : ℕ) : (self.signedPressure j).shift = -(2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h)

noncomputable def NavierStokes.ActualStageEstimates.cycleInputs {B N0 N : ℕ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) : ActualPhysicalStageBounds.CycleInputs CorrectionInitialization.ActualPrimary.h DP (Fin 3 × IP) KP DS (Fin 3 × IS) KS

Cycle inputs, bundling particularPotential, signedPotential, particularPressure, signedPressure and the required compatibility proofs.

Equations

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

theorem NavierStokes.ActualStageEstimates.cycleInputs_potential {B N0 N : ℕ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) (j : ℕ) : (cycleInputs R M hN W).potential j = fun (w : ProblemStatement.SpaceTime) => (W.particularPotential j).vector w + (W.signedPotential j).vector w + ((ActualMeanPhysicalData.initialCycleData M).temporalFamily j).angularField w + ((ActualMeanPhysicalData.initialCycleData M).rankFamily j).angularField w

theorem NavierStokes.ActualStageEstimates.cycleInputs_direct {B N0 N : ℕ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) (j : ℕ) : (cycleInputs R M hN W).direct j = ((ActualMeanPhysicalData.initialCycleData M).angularIncrementFamily j).angularField

theorem NavierStokes.ActualStageEstimates.cycleInputs_pressure {B N0 N : ℕ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) (j : ℕ) : (cycleInputs R M hN W).pressureField j = fun (w : ProblemStatement.SpaceTime) => (W.particularPressure j).pressure w + (W.signedPressure j).pressure w + ((ActualMeanPhysicalData.initialCycleData M).pressureIncrementFamily j).field w

theorem NavierStokes.ActualStageEstimates.cycleInputs_metadata {B N0 N : ℕ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) : (cycleInputs R M hN W).Metadata ChartScales.kappa

theorem NavierStokes.ActualStageEstimates.cycleInputs_validScale {B N0 N : ℕ} {DP DS : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) {qbig : ℝ} (hq : qbig ≤ ChartScales.Q N) : (cycleInputs R M hN W).ValidScale qbig

The actual finite-stage estimate record

noncomputable def NavierStokes.ActualStageEstimates.backgroundLoss (waveAlpha waveShift : ℝ) : ℕ → ℝ

The initialized background loss is fixed before the number of correction stages is chosen.

Equations

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

structure NavierStokes.ActualStageEstimates.Representations {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) (qbig : ℝ) (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) (A Bdirect : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : Prop

Literal component identities supplied by the physical sequence construction. These are equalities of fields on a fixed open sublevel, and contain no bounds for physical derivatives.

• potential_zero : Set.EqOn (A 0) (ActualPhysicalStageBounds.initialPotential CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B WA (ActualPhysicalStageBounds.actualInitialTemporalInput B N0 N hN) (ActualPhysicalStageBounds.actualInitialRankInput B N0 N hN)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• direct_zero : Set.EqOn (Bdirect 0) (ActualMeanPhysicalData.initialAngularFamily B N0 N).angularField (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• pressure_zero : Set.EqOn (P 0) (fun (w : ProblemStatement.SpaceTime) => FinalSlowBase.pressure CorrectionInitialization.ActualPrimary.certificate CorrectionInitialization.ActualPrimary.modulation CorrectionInitialization.ActualPrimary.upper B w + ActualPhysicalStageBounds.initialPressureIncrement WP (ActualPhysicalStageBounds.actualInitialPressureInput B N0 N hN) w) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• potential_succ (j : ℕ) : Set.EqOn ((cycleInputs R M hN W).potential j) (A (j + 1)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• direct_succ (j : ℕ) : Set.EqOn ((cycleInputs R M hN W).direct j) (Bdirect (j + 1)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)
• pressure_succ (j : ℕ) : Set.EqOn ((cycleInputs R M hN W).pressureField j) (P (j + 1)) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.ActualStageEstimates.Representations.potential_smooth {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) {qbig : ℝ} (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W qbig WA WP A Bdirect P) (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (A j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.ActualStageEstimates.Representations.direct_smooth {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) {qbig : ℝ} (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W qbig WA WP A Bdirect P) (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (Bdirect j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

theorem NavierStokes.ActualStageEstimates.Representations.pressure_smooth {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) {qbig : ℝ} (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W qbig WA WP A Bdirect P) (hq : qbig ≤ ChartScales.Q N) (j : ℕ) : ContDiffOn ℝ (↑⊤) (P j) (CutStageEstimates.physicalSublevel CorrectionInitialization.ActualPrimary.h qbig)

noncomputable def NavierStokes.ActualStageEstimates.stageEstimatesOfRepresentations {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) {qbig : ℝ} (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W qbig WA WP A Bdirect P) (hq : qbig ≤ ChartScales.Q N) (hqbig : 0 < qbig) {Nres : ℕ} (hNres : 4 ≤ Nres) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (d : ∀ (J : ℕ), ActualCycleResidualBounds.PhysicalData B Nres (ActualCyclePreservation.state B N0 J).state (MixedDiagonalResidual.uncutVelocity A Bdirect J) (DiagonalJetBounds.uncutPrefix P (J + 1))) : MixedCandidateAssembly.StageEstimates CorrectionInitialization.ActualPrimary.h qbig A Bdirect P

The complete estimate record is constructed from native data and exact physical realizations. The residual comparison floor is separate from the mean-family floor, so it can be chosen one band larger.

Equations

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

theorem NavierStokes.ActualStageEstimates.stageEstimates_ledger {B N0 N : ℕ} {DP DS DA0 DP0 : Type} [NormedAddCommGroup DP] [NormedSpace ℝ DP] [NormedAddCommGroup DS] [NormedSpace ℝ DS] [NormedAddCommGroup DA0] [NormedSpace ℝ DA0] [NormedAddCommGroup DP0] [NormedSpace ℝ DP0] {IP : Type u_1} {KP : Type u_2} {IS : Type u_3} {KS : Type u_4} {IA0 : Type u_5} {KA0 : Type u_6} {IP0 : Type u_7} {KP0 : Type u_8} (R : RunData B N0) (M : ActualMeanPhysicalData.InitialCycleInput B N0 N fun (x : ℕ) => ActualCycleParameters.fixedParameters B N0) (hN : 4 ≤ N) (W : WaveInputs DP IP KP DS IS KS) {qbig : ℝ} (WA : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DA0 IA0 KA0 (Fin 3)) (WP : PhysicalStageBounds.WaveData CorrectionInitialization.ActualPrimary.h DP0 IP0 KP0 Unit) {A Bdirect : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (e : Representations R M hN W qbig WA WP A Bdirect P) (hq : qbig ≤ ChartScales.Q N) (hqbig : 0 < qbig) {Nres : ℕ} (hNres : 4 ≤ Nres) (hGeom : ActualCarrierGeometry.geometricThreshold ≤ N0) (d : ∀ (J : ℕ), ActualCycleResidualBounds.PhysicalData B Nres (ActualCyclePreservation.state B N0 J).state (MixedDiagonalResidual.uncutVelocity A Bdirect J) (DiagonalJetBounds.uncutPrefix P (J + 1))) : have E := stageEstimatesOfRepresentations R M hN W WA WP e hq hqbig hNres hGeom d; E.gain = ActualIterationLedger.gain CorrectionInitialization.ActualPrimary.h ∧ E.potentialLoss = PhysicalStageBounds.potentialLoss CorrectionInitialization.ActualPrimary.h CorrectionInitialization.ActualPrimary.h 0 ∧ E.directLoss = PhysicalStageBounds.directLoss CorrectionInitialization.ActualPrimary.h 0 ∧ E.pressureLoss = PhysicalStageBounds.pressureLoss CorrectionInitialization.ActualPrimary.h (2 * CoordinateAlgebra.A CorrectionInitialization.ActualPrimary.h) 0 ∧ E.backgroundLoss = backgroundLoss WA.alpha WA.shift ∧ E.residualLoss = ActualCycleResidualBounds.fixedLoss