One all-order correction from the actual small-drift construction

The finite solutions used here are Budget.solution from AllOrderDriftFinite. Their existence is proved by the drift-aware finite-Sobolev solver. The generic assembly proves compatibility from their literal equations and uniqueness; it does not require the coarse full-velocity shrinking-radius assumption.

The resulting single field retains the residual and target-error estimates at every external cutoff and satisfies the actual equation in every finite Sobolev order. Smoothness asserted here is spatial smoothness, with a jointly continuous representative and its genuine first time derivative.

Genuine pointwise time differentiation of the generically assembled correction.

noncomputable def EulerCorrectionAssembly.FiniteFamily.pointRawSource (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

The canonical pointwise nonlinear raw source of the actual common correction.

Equations

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

noncomputable def EulerCorrectionAssembly.FiniteFamily.pointTimeDerivative (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

The canonical actual time derivative, defined by bounded evaluation of the genuine continuous Sobolev source.

Equations

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

theorem EulerCorrectionAssembly.FiniteFamily.pointTimeDerivative_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) : Continuous (Function.uncurry (pointTimeDerivative period F))

The actual pointwise time derivative is jointly continuous in time and space.

theorem EulerCorrectionAssembly.FiniteFamily.pointTimeDerivative_eq_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : pointTimeDerivative period F t x = -pointRawSource period F t x - ((A.metric.coefficient t).coefficient x) (pointPressure period F t x)

The pointwise time derivative is the literal raw-source and signed-pressure expression.

theorem EulerCorrectionAssembly.FiniteFamily.pointField_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (x : EulerLiftedGradientSpace.LiftDomain period) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => pointField period F (Set.projIcc 0 T ⋯ r) x) (pointTimeDerivative period F ⟨t, ⋯⟩ x) t

The canonical common field has its genuine pointwise first time derivative at every interior time.

theorem EulerCorrectionAssembly.FiniteFamily.pointField_hasDerivAt_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (x : EulerLiftedGradientSpace.LiftDomain period) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => pointField period F (Set.projIcc 0 T ⋯ r) x) (-pointRawSource period F ⟨t, ⋯⟩ x - ((A.metric.coefficient ⟨t, ⋯⟩).coefficient x) (pointPressure period F ⟨t, ⋯⟩ x)) t

The actual pointwise correction equation uses the reconstructed signed pressure and literal matrix multiplication.

theorem EulerAllOrderDriftCorrection.Budget.solution_compatible (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period (q + 1))) (solution period B (q + 1) ⋯) = solution period B q hq

The drift-aware finite solutions coincide under the actual Sobolev restriction.

noncomputable def EulerAllOrderDriftCorrection.Budget.commonPath (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The common continuous L² correction constructed by the small-drift solver.

Equations

• EulerAllOrderDriftCorrection.Budget.commonPath period B = EulerCorrectionAssembly.FiniteFamily.commonPath period (EulerAllOrderDriftCorrection.Budget.family period B)

theorem EulerAllOrderDriftCorrection.Budget.solution_value_common (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((solution period B q hq) t) = (commonPath period B) t

Every actual drift-aware finite solution represents this same common field.

theorem EulerAllOrderDriftCorrection.Budget.commonPath_initial (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : (commonPath period B) ⟨0, ⋯⟩ = 0

The common correction has zero initial trace.

theorem EulerAllOrderDriftCorrection.Budget.commonPath_divergence (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) : (commonPath period B) t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

The common correction satisfies the genuine closed lifted divergence constraint.

theorem EulerAllOrderDriftCorrection.Budget.commonPath_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (commonPath period B)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A 6) ⋯).apply ⟨t, ⋯⟩ ((solution period B 6 ⋯) ⟨t, ⋯⟩))) t

The common L² path satisfies the actual projected correction equation.

noncomputable def EulerAllOrderDriftCorrection.Budget.commonJet (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (n : ℕ) (t : ↑(Set.Icc 0 T)) : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection n ((commonPath period B) t)

An actual strong spatial jet of every order for the constructed common field.

Equations

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

noncomputable def EulerAllOrderDriftCorrection.Budget.fieldTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : EulerAllOrderCorrectionData.FieldTower period T

The common correction, with genuine continuous Sobolev realizations at all orders.

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_field (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : (fieldTower period B).field = commonPath period B

The tower's underlying field is exactly the constructed common correction.

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_initial (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) : ((fieldTower period B).realization q) ⟨0, ⋯⟩ = 0

Every Sobolev realization of the common correction has zero initial data.

theorem EulerAllOrderDriftCorrection.Budget.solution_eq_realization (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) : solution period B q hq = (fieldTower period B).realization (q + 1)

A finite drift-aware solution equals the common tower's realization at its order.

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_energy (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : ℕ) (t : ↑(Set.Icc 0 T)) : EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) (((fieldTower period B).realization (P + 6 + 1)) t) ≤ 2 * (B.spatial (P + 6) ⋯).full.residual * Real.exp (3 * B.growthCoefficient * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) (((fieldTower period B).realization (P + 6 + 1)) t) ≤ B.delta / 2

Both quantitative finite-solver bounds hold for the actual common realization. The radius and residual envelope are the drift-aware input budgets.

theorem EulerAllOrderDriftCorrection.Budget.solution_sobolev_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (EulerVolterraConvolution.extendPath T ⋯ (solution period B q hq) r)) ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ ((solution period B q hq) ⟨t, ⋯⟩)) t

The constructed finite solution has its genuine time derivative in Hq.

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ ((fieldTower period B).realization q)) ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ (((fieldTower period B).realization (q + 1)) ⟨t, ⋯⟩)) t

Every finite Sobolev realization of the common correction satisfies the actual projected nonlinear evolution, not merely an equation for an unrelated finite solve.

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_hasDerivAt_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ ((fieldTower period B).realization q)) (-EulerCorrectionOperators.CorrectionData.rawSource period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq ⟨t, ⋯⟩ (((fieldTower period B).realization (q + 1)) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (A.metric.jet q ⟨t, ⋯⟩)) (EulerCorrectionOperators.CorrectionData.pressure period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq ⟨t, ⋯⟩ (((fieldTower period B).realization (q + 1)) ⟨t, ⋯⟩))) t

The common realization's actual derivative is the literal raw source plus signed pressure.

noncomputable def EulerAllOrderDriftCorrection.Budget.pointField (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

Canonical bounded evaluation fixes a pointwise representative of the correction.

Equations

• EulerAllOrderDriftCorrection.Budget.pointField period B t x = EulerCorrectionAssembly.FiniteFamily.pointField period (EulerAllOrderDriftCorrection.Budget.family period B) t x

theorem EulerAllOrderDriftCorrection.Budget.pointField_ae (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) : ↑↑((commonPath period B) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] pointField period B t

The pointwise correction is an actual representative of the constructed L² field.

theorem EulerAllOrderDriftCorrection.Budget.pointField_initial (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (x : EulerLiftedGradientSpace.LiftDomain period) : pointField period B ⟨0, ⋯⟩ x = 0

The canonical correction vanishes pointwise at the initial time.

theorem EulerAllOrderDriftCorrection.Budget.pointField_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : Continuous (Function.uncurry (pointField period B))

The canonical correction is jointly continuous in time and the cylinder point.

theorem EulerAllOrderDriftCorrection.Budget.pointField_smooth (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (pointField period B t) x)

The one common correction has a spatially smooth representative at every time.

theorem EulerAllOrderDriftCorrection.Budget.pointField_divergence (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection A.κ A.direction i) (pointField period B t) x).ofLp i = 0

Its lifted divergence vanishes pointwise.

theorem EulerAllOrderDriftCorrection.Budget.commonPath_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection period) ((commonPath period B) t) = (commonPath period B) t

Odd input data give an odd common correction by the proved PDE uniqueness.

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (q : ℕ) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period q) (((fieldTower period B).realization q) t) = ((fieldTower period B).realization q) t

The actual common Sobolev realizations retain the prescribed odd parity.

theorem EulerAllOrderDriftCorrection.Budget.pointField_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (P : EulerCorrectionAssembly.ParityData period A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : pointField period B t (-x) = -pointField period B t x

The canonical spatially smooth correction is pointwise odd for odd input data.

noncomputable def EulerAllOrderDriftCorrection.Budget.pointTimeDerivative (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

The actual pointwise time derivative, obtained from the constructed Sobolev source.

Equations

• EulerAllOrderDriftCorrection.Budget.pointTimeDerivative period B t x = EulerCorrectionAssembly.FiniteFamily.pointTimeDerivative period (EulerAllOrderDriftCorrection.Budget.family period B) t x

theorem EulerAllOrderDriftCorrection.Budget.pointTimeDerivative_joint_continuous (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : Continuous (Function.uncurry (pointTimeDerivative period B))

The correction's actual first time derivative is jointly continuous.

theorem EulerAllOrderDriftCorrection.Budget.pointTimeDerivative_eq_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : pointTimeDerivative period B t x = -EulerCorrectionAssembly.FiniteFamily.pointRawSource period (family period B) t x - ((A.metric.coefficient t).coefficient x) (EulerCorrectionAssembly.FiniteFamily.pointPressure period (family period B) t x)

The actual time derivative equals the raw source and the signed pressure term.

theorem EulerAllOrderDriftCorrection.Budget.pointField_hasDerivAt (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (x : EulerLiftedGradientSpace.LiftDomain period) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => pointField period B (Set.projIcc 0 T ⋯ r) x) (pointTimeDerivative period B ⟨t, ⋯⟩ x) t

The canonical common field has its genuine first time derivative at interior times.

theorem EulerAllOrderDriftCorrection.Budget.pointField_hasDerivAt_pressure (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) (x : EulerLiftedGradientSpace.LiftDomain period) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => pointField period B (Set.projIcc 0 T ⋯ r) x) (-EulerCorrectionAssembly.FiniteFamily.pointRawSource period (family period B) ⟨t, ⋯⟩ x - ((A.metric.coefficient ⟨t, ⋯⟩).coefficient x) (EulerCorrectionAssembly.FiniteFamily.pointPressure period (family period B) ⟨t, ⋯⟩ x)) t

The pointwise correction equation contains the actual raw source and signed pressure.

theorem EulerAllOrderDriftCorrection.exists_smooth_lifted_correction (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (B : Budget period hT A) : ∃ (E : EulerAllOrderCorrectionData.FieldTower period T) (g : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (v : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), E.field ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), E.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction) ∧ Continuous (Function.uncurry g) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (g t) x)) ∧ (∀ (t : ↑(Set.Icc 0 T)), ↑↑(E.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g t) ∧ (∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection A.κ A.direction i) (g t) x).ofLp i = 0) ∧ Continuous (Function.uncurry v) ∧ (∀ (x : EulerLiftedGradientSpace.LiftDomain period) (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => g (Set.projIcc 0 T ⋯ r) x) (v ⟨t, ⋯⟩ x) t) ∧ (∀ (P : ℕ) (t : ↑(Set.Icc 0 T)), EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((E.realization (P + 6 + 1)) t) ≤ 2 * (B.spatial (P + 6) ⋯).full.residual * Real.exp (3 * B.growthCoefficient * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period P ⋯ (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((E.realization (P + 6 + 1)) t) ≤ B.delta / 2) ∧ ∀ (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (E.realization q)) ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ ((E.realization (q + 1)) ⟨t, ⋯⟩)) t

Genuine coherent input bounds, with radius loss determined only by the actual transport drift, construct one smooth spatial correction with all-cutoff energy bounds and its actual finite-Sobolev evolution. Finite existence, compatibility, energy estimates and the correction equation are conclusions here.