Candidate assembly from the actual finite-stage obligations

The inputs here concern raw increments, their finite uncut prefixes, and their local endpoint models. The scale sequence, infinite residual limits, away extensions, divergence and blow-up are then derived for the same sums.

This is a conditional consumer. It does not construct the complete correction iteration or supply the finite-stage estimates it requires.

structure NavierStokes.MixedCandidateAssembly.StageEstimates (h qbig : ℝ) (A B : ℕ → ProblemStatement.VelocityField) (P : ℕ → ProblemStatement.PressureField) : Type

The quantitative obligations are all on the raw fields or finite prefixes. In particular no infinite residual limit is a field here.

• potential_smooth (j : ℕ) : ContDiffOn ℝ (↑⊤) (A j) (CutStageEstimates.physicalSublevel h qbig)
• direct_smooth (j : ℕ) : ContDiffOn ℝ (↑⊤) (B j) (CutStageEstimates.physicalSublevel h qbig)
• pressure_smooth (j : ℕ) : ContDiffOn ℝ (↑⊤) (P j) (CutStageEstimates.physicalSublevel h qbig)
• gain : ℕ → ℝ

  Gain of StageEstimates, of type ℕ → ℝ.

• gain_zero : 0 ≤ self.gain 0
• gain_pos (j : ℕ) : 1 ≤ j → 0 < self.gain j
• gain_mono : Monotone self.gain
• gain_top : Filter.Tendsto self.gain Filter.atTop Filter.atTop
• potentialLoss : ℕ → ℝ

  Potential loss of StageEstimates, of type ℕ → ℝ.

• directLoss : ℕ → ℝ

  Direct loss of StageEstimates, of type ℕ → ℝ.

• pressureLoss : ℕ → ℝ

  Pressure loss of StageEstimates, of type ℕ → ℝ.

• potentialConstant : ℕ → ℕ → ℝ

  Potential constant of StageEstimates, of type ℕ → ℕ → ℝ.

• directConstant : ℕ → ℕ → ℝ

  Direct constant of StageEstimates, of type ℕ → ℕ → ℝ.

• pressureConstant : ℕ → ℕ → ℝ

  Pressure constant of StageEstimates, of type ℕ → ℕ → ℝ.

• potentialLog : ℕ → ℕ → ℝ

  Potential log of StageEstimates, of type ℕ → ℕ → ℝ.

• directLog : ℕ → ℕ → ℝ

  Direct log of StageEstimates, of type ℕ → ℕ → ℝ.

• pressureLog : ℕ → ℕ → ℝ

  Pressure log of StageEstimates, of type ℕ → ℕ → ℝ.

• potential_bound : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) A self.gain self.potentialLoss self.potentialConstant self.potentialLog (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)
• direct_bound : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) B self.gain self.directLoss self.directConstant self.directLog (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)
• pressure_bound : CutStageEstimates.RawStageBounds (PhysicalWaveSum.physicalQ h) P self.gain self.pressureLoss self.pressureConstant self.pressureLog (PhysicalWaveSum.preterminal ∩ CutStageEstimates.physicalSublevel h qbig)
• backgroundLoss : ℕ → ℝ

  Background loss of StageEstimates, of type ℕ → ℝ.

• residualLoss : ℕ → ℝ

  Residual loss of StageEstimates, of type ℕ → ℝ.

• finite_background (J m : ℕ) : DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (MixedDiagonalResidual.uncutVelocity A B J) m (-self.backgroundLoss m)
• finite_residual (J m : ℕ) : DiagonalResidual.JetRate (nhdsWithin (1, 0) (SpacetimeEndpoint.openPast 1)) (PhysicalWaveSum.physicalQ h) (fun (z : ℝ × ProblemStatement.Space) => ProblemStatement.navierStokesResidual (MixedDiagonalResidual.uncutVelocity A B J) (DiagonalJetBounds.uncutPrefix P (J + 1)) z.1 z.2) m (self.gain J - self.residualLoss m)

theorem NavierStokes.MixedCandidateAssembly.StageEstimates.exists_schedule {h qbig : ℝ} {A B : ℕ → ProblemStatement.VelocityField} {P : ℕ → ProblemStatement.PressureField} (E : StageEstimates h qbig A B P) (hh : 0 < h) (hh1 : h < 1 / 2) (hqbig : 0 < qbig) (lower : ℕ) : ∃ (a : ℕ → ℕ), lower ≤ a 0 ∧ (∀ (j : ℕ), 0 < a j) ∧ (∀ (j : ℕ), 2 * a j ≤ a (j + 1)) ∧ StrictMono a ∧ Filter.Tendsto (fun (j : ℕ) => ↑(a j)) Filter.atTop Filter.atTop ∧ (∀ (j : ℕ), 1 / ↑(a j) < qbig) ∧ MixedDiagonalSchedule.ThreeSmoothSums a h A B P ∧ JointResidualLimits.VanishingJointJets (MixedDiagonalResidual.residual (fun (j : ℕ) => ↑(a j)) (PhysicalWaveSum.physicalQ h) A B P)

noncomputable def NavierStokes.MixedCandidateAssembly.potentialStages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig : ℝ} (initial : MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (stages : ℕ → MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) : ℕ → ProblemStatement.VelocityField

The actual anchored base and finite initialization share stage zero.

Equations

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

noncomputable def NavierStokes.MixedCandidateAssembly.pressureStages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) (initial : ProblemStatement.PressureField) (stages : ℕ → ProblemStatement.PressureField) : ℕ → ProblemStatement.PressureField

Pressure is recorded as the actual base plus its initialization change, followed by the pressure differences of full correction stages.

Equations

• NavierStokes.MixedCandidateAssembly.pressureStages H v upper bandFloor initial stages j w = if j = 0 then NavierStokes.FinalSlowBase.pressure H v upper bandFloor w + initial w else stages (j - 1) w

theorem NavierStokes.MixedCandidateAssembly.pressureStages_zero {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) (initial : ProblemStatement.PressureField) (stages : ℕ → ProblemStatement.PressureField) (w : ProblemStatement.SpaceTime) : pressureStages H v upper bandFloor initial stages 0 w = FinalSlowBase.pressure H v upper bandFloor w + initial w

theorem NavierStokes.MixedCandidateAssembly.pressureStages_succ {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) (initial : ProblemStatement.PressureField) (stages : ℕ → ProblemStatement.PressureField) (j : ℕ) : pressureStages H v upper bandFloor initial stages (j + 1) = stages j

theorem NavierStokes.MixedCandidateAssembly.candidate_of_finite_stages {F : OutgoingProfile.Profile} {W : NominalProfile.Witness F} (H : NominalConeAssembly.Certificate W) {ld : ModulatedProfileAssembly.LoopData W} (v : ModulatedProfileAssembly.Witness ld) (upper : ℝ) (bandFloor : ℕ) {qbig C : ℝ} (hqbig : 0 < qbig) (initial : MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (stages : ℕ → MixedAxisPreservation.PotentialStage F.data.h (MixedAxisPreservation.localDomain F.data.h qbig)) (D : ℕ → DirectAngularDiagonal.AngularData (LocalAngularDiagonal.localSlowDomain F.data.h qbig)) (pInitial : ProblemStatement.PressureField) (pStages : ℕ → ProblemStatement.PressureField) (E : StageEstimates F.data.h qbig (potentialStages H v upper bandFloor initial stages) (LocalAngularDiagonal.rawSeries D) (pressureStages H v upper bandFloor pInitial pStages)) (hInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig initial.field) (hStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (stages j).field) (hDirect : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (LocalAngularDiagonal.rawSeries D j)) (hpInitial : MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig pInitial) (hpStages : ∀ (j : ℕ), MixedDiagonalExtensions.SublevelShrinkingSupport F.data.h C qbig (pStages j)) (eA : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (potentialStages H v upper bandFloor initial stages j) x)) (eB : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (LocalAngularDiagonal.rawSeries D j) x)) (eP : ∀ (x : ProblemStatement.Space), x.ofLp 2 ≠ 0 → EndpointCoordinates.endpointRoot (2 * F.data.h) (x.ofLp 2) < qbig → ∀ (j : ℕ), Nonempty (JointResidualLimits.OneSidedExtension (pressureStages H v upper bandFloor pInitial pStages j) x)) : ProblemStatement.candidateStatement

Supply the finite-stage construction once, for these exact raw families. All infinite-sum and final-force conditions are proved below.