Actual spatial L² paths of the constructed correction and its pressure on every fixed continuous phase graph, including every cylinder word and the genuine time derivative.

noncomputable def EulerAllOrderDriftCorrection.Budget.graphCorrectionWordPath (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume))

Spatial L² path of the word derivative of the correction, restricted to the graph of θ.

Equations

• EulerAllOrderDriftCorrection.Budget.graphCorrectionWordPath P B θ hθ n w = (EulerAllOrderDriftCorrection.Budget.fieldTower P B).canonicalGraphWordPath θ hθ n w

noncomputable def EulerAllOrderDriftCorrection.Budget.graphTimeDerivativeWordPath (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume))

Spatial L² path of the word derivative of the time derivative, on the graph of θ.

Equations

• EulerAllOrderDriftCorrection.Budget.graphTimeDerivativeWordPath P B θ hθ n w = (EulerAllOrderDriftCorrection.Budget.timeDerivativeTower P B).canonicalGraphWordPath θ hθ n w

noncomputable def EulerAllOrderDriftCorrection.Budget.graphPressureWordPath (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume))

Spatial L² path of the word derivative of the pressure, restricted to the graph of θ.

Equations

• EulerAllOrderDriftCorrection.Budget.graphPressureWordPath P B θ hθ n w = (EulerAllOrderDriftCorrection.Budget.pressureTower P B).canonicalGraphWordPath θ hθ n w

theorem EulerAllOrderDriftCorrection.Budget.correctionTower_pointField (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (t : ↑(Set.Icc 0 T)) : (fieldTower P B).pointField t = pointField P B t

theorem EulerAllOrderDriftCorrection.Budget.pressureTower_pointField (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (t : ↑(Set.Icc 0 T)) : (pressureTower P B).pointField t = pointPressure P B t

theorem EulerAllOrderDriftCorrection.Budget.graphCorrectionWordPath_ae (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ↑↑((graphCorrectionWordPath P B θ hθ n w) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w (pointField P B t) (x, θ x)

theorem EulerAllOrderDriftCorrection.Budget.graphPressureWordPath_ae (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ↑↑((graphPressureWordPath P B θ hθ n w) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w (pointPressure P B t) (x, θ x)

theorem EulerAllOrderDriftCorrection.Budget.graphCorrectionWordPath_hasDerivAt (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (graphCorrectionWordPath P B θ hθ n w)) ((graphTimeDerivativeWordPath P B θ hθ n w) ⟨t, ⋯⟩) t

theorem EulerAllOrderDriftCorrection.Budget.graphCorrectionWordPath_initial (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) : (graphCorrectionWordPath P B θ hθ n w) ⟨0, ⋯⟩ = 0