Adding the actual correction removes a genuine approximate-solution residual.
@[instance_reducible]
noncomputable def
EulerCorrectionResidualCancellation.residualSobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The inherited Sobolev group structure for exact residual cancellation.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionResidualCancellation.residualSobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The inherited real Sobolev module structure for exact residual cancellation.
Equations
Instances For
noncomputable def
EulerCorrectionResidualCancellation.nonlinearity
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The actual linear coefficient plus the full transport-and-algebraic quadratic nonlinearity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionResidualCancellation.rawSource_eq_residual_increment
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
EulerCorrectionOperators.CorrectionData.rawSource period D hq t e = D.residual t + nonlinearity period D hq t (D.approximation t + e) - nonlinearity period D hq t (D.approximation t)
The actual raw correction source is exactly the prescribed residual plus the full nonlinear increment about the prescribed approximation.
theorem
EulerCorrectionResidualCancellation.residual_cancellation
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(pa : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
D.residual t - nonlinearity period D hq t (D.approximation t) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet t)) pa + (-EulerCorrectionOperators.CorrectionData.rawSource period D hq t e - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet t))
(EulerCorrectionOperators.CorrectionData.pressure period D hq t e)) = -nonlinearity period D hq t (D.approximation t + e) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet t))
(pa + EulerCorrectionOperators.CorrectionData.pressure period D hq t e)
The signed approximate and correction equations cancel the residual and add their actual pressures.
noncomputable def
EulerCorrectionResidualCancellation.correctedPath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual continuous corrected path is the prescribed approximation plus the constructed error.
Equations
- EulerCorrectionResidualCancellation.correctedPath period D e = D.approximation + e
Instances For
theorem
EulerCorrectionResidualCancellation.correctedPath_initial
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(he : e ⟨0, ⋯⟩ = 0)
:
A zero initial correction preserves the actual initial field.
theorem
EulerCorrectionResidualCancellation.correctedPath_divergenceFree
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hz :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(he :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(t : ↑(Set.Icc 0 T))
:
EulerCylinderSobolevSpace.value period ((correctedPath period D e) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction
The corrected path retains the genuine lifted divergence constraint by addition in its closed subspace.
theorem
EulerCorrectionResidualCancellation.corrected_pressure_mem_gradient
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
[TopologicalSpace T]
(D : EulerCorrectionOperators.CorrectionData period q T)
(hq : 6 ≤ q)
(t : T)
(e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(pa : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(hpa : EulerCylinderSobolevSpace.value period pa ∈ EulerLiftedGradientSpace.gradientSpace period D.κ D.direction)
:
EulerCylinderSobolevSpace.value period (pa + EulerCorrectionOperators.CorrectionData.pressure period D hq t e) ∈ EulerLiftedGradientSpace.gradientSpace period D.κ D.direction
Adding a genuine approximate pressure to the actual correction pressure preserves membership in the lifted gradient space.
theorem
EulerCorrectionResidualCancellation.correctedPath_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(pa : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
(hz :
HasDerivAt
(fun (r : ℝ) =>
(EulerCylinderSobolevSpace.truncateOperator period q)
(EulerVolterraConvolution.extendPath T hT D.approximation r))
(D.residual ⟨t, ⋯⟩ - nonlinearity period D hq ⟨t, ⋯⟩ (D.approximation ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet ⟨t, ⋯⟩)) (pa ⟨t, ⋯⟩))
t)
(he :
HasDerivAt
(fun (r : ℝ) =>
(EulerCylinderSobolevSpace.truncateOperator period q) (EulerVolterraConvolution.extendPath T hT e r))
(-EulerCorrectionOperators.CorrectionData.rawSource period D hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet ⟨t, ⋯⟩))
(EulerCorrectionOperators.CorrectionData.pressure period D hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩)))
t)
:
HasDerivAt
(fun (r : ℝ) =>
(EulerCylinderSobolevSpace.truncateOperator period q)
(EulerVolterraConvolution.extendPath T hT (correctedPath period D e) r))
(-nonlinearity period D hq ⟨t, ⋯⟩ ((correctedPath period D e) ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (D.metric.jet ⟨t, ⋯⟩))
(pa ⟨t, ⋯⟩ + EulerCorrectionOperators.CorrectionData.pressure period D hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩)))
t
Actual approximate and correction derivatives give the zero-residual nonlinear equation for their sum, with the sum of their genuine pressures.