Continuous all-order realizations of the actual nonlinear source and time derivative.

@[instance_reducible]

noncomputable def EulerCorrectionAssembly.sourceTowerGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerCorrectionAssembly.sourceTowerGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionAssembly.sourceTowerSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerCorrectionAssembly.sourceTowerSpace period q = inferInstance

theorem EulerCorrectionAssembly.FiniteFamily.rawSourcePath_value_base (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((rawSourcePath period F q hq) t) = EulerCylinderSobolevSpace.value period ((rawSourcePath period F 6 ⋯) t)

noncomputable def EulerCorrectionAssembly.FiniteFamily.rawSourceTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) : EulerAllOrderCorrectionData.FieldTower period T

One actual source field, represented continuously at every finite order.

Equations

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

theorem EulerCorrectionAssembly.FiniteFamily.rawSourcePath_eq_realization (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : (rawSourcePath period F q hq) t = ((rawSourceTower period F C).realization q) t

noncomputable def EulerCorrectionAssembly.FiniteFamily.timeDerivativeTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) : EulerAllOrderCorrectionData.FieldTower period T

The literal signed pressure equation defines a continuous all-order field, subsequently identified with the genuine time derivative.

Equations

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

theorem EulerCorrectionAssembly.FiniteFamily.source_eq_timeDerivativeTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : (EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply t ((F.solution q hq) t) = ((timeDerivativeTower period F C).realization q) t

The source returned by the constructed finite solver is exactly the corresponding realization of the common derivative field.

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

Raw source tower, given by (B.family period).rawSourceTower period (B.comparisonData period).

Equations

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

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

Time derivative tower, given by (B.family period).timeDerivativeTower period (B.comparisonData period).

Equations

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

theorem EulerAllOrderDriftCorrection.Budget.rawSource_eq_realization (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)) : EulerCorrectionOperators.CorrectionData.rawSource period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq t (((fieldTower period B).realization (q + 1)) t) = ((rawSourceTower period B).realization q) t

theorem EulerAllOrderDriftCorrection.Budget.source_eq_timeDerivativeTower (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)) : (EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply t (((fieldTower period B).realization (q + 1)) t) = ((timeDerivativeTower period B).realization q) t

theorem EulerAllOrderDriftCorrection.Budget.fieldTower_hasDerivAt_timeDerivativeTower (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)) (((timeDerivativeTower period B).realization q) ⟨t, ⋯⟩) t

At every interior time, this continuous all-order field is the actual time derivative of the constructed common correction.