Coherence and all-order regularity of the actual pressure associated with a finite correction family.
A common actual smooth lifted correction assembled from finite solves and proved uniqueness.
noncomputable def
EulerCorrectionAssembly.FiniteFamily.commonPath
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
:
The actual common continuous L² path, defined from the base finite correction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionAssembly.FiniteFamily.value_common
(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))
:
Every supplied finite correction realizes the common actual L² path.
theorem
EulerCorrectionAssembly.FiniteFamily.commonPath_initial
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
:
The common correction has zero initial trace.
theorem
EulerCorrectionAssembly.FiniteFamily.commonPath_divergence
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(t : ↑(Set.Icc 0 T))
:
The common correction satisfies the actual closed lifted divergence constraint.
noncomputable def
EulerCorrectionAssembly.FiniteFamily.commonJet
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(C : ComparisonData period hT A)
(n : ℕ)
(t : ↑(Set.Icc 0 T))
:
EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection n ((commonPath period F) t)
The common correction has an actual strong spatial jet at every derivative order.
Equations
- EulerCorrectionAssembly.FiniteFamily.commonJet period F C n t = ⋯.mpr (EulerH6Pressure.SpatialJet.restrict (EulerCylinderSobolevSpace.toJet period ((F.solution (n + 6) ⋯) t)) n ⋯)
Instances For
theorem
EulerCorrectionAssembly.FiniteFamily.commonPath_hasDerivAt
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (commonPath period F))
(EulerCylinderSobolevSpace.value period
((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A 6)
⋯).apply
⟨t, ⋯⟩ ((F.solution 6 ⋯) ⟨t, ⋯⟩)))
t
The common L² path satisfies the actual nonlinear inviscid equation.
theorem
EulerCorrectionAssembly.FiniteFamily.realizes_common
(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)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hi : u ⟨0, ⋯⟩ = 0)
(hd :
∀ (t : ↑(Set.Icc 0 T)),
EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction)
(hu :
∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T),
HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T ⋯ u r))
(EulerCylinderSobolevSpace.value period
((EulerCorrectionOperators.CorrectionData.coefficients period
(EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply
⟨t, ⋯⟩ (u ⟨t, ⋯⟩)))
t)
(t : ↑(Set.Icc 0 T))
:
Every other genuine finite-order correction realizes this same common field. Consequently bounds proved for any particular finite solver may be transferred to the assembled solution.
noncomputable def
EulerCorrectionAssembly.FiniteFamily.pointField
(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)
:
Bounded H3 evaluation fixes a canonical actual pointwise representative of the common correction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionAssembly.FiniteFamily.pointField_ae
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(t : ↑(Set.Icc 0 T))
:
↑↑((commonPath period F) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] pointField period F t
The canonical common field is an actual representative of its L² path.
theorem
EulerCorrectionAssembly.FiniteFamily.pointField_joint_continuous
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
:
Continuous (Function.uncurry (pointField period F))
The canonical common field is jointly continuous in time and the cylinder point.
theorem
EulerCorrectionAssembly.FiniteFamily.pointField_smooth
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(C : ComparisonData period hT A)
(t : ↑(Set.Icc 0 T))
(x : EulerLiftedGradientSpace.LiftDomain period)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (pointField period F t) x)
Proved compatibility and all finite genuine jets make the canonical common field spatially smooth.
theorem
EulerCorrectionAssembly.FiniteFamily.pointField_divergence
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(C : ComparisonData 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 F t) x).ofLp
i = 0
The canonical smooth field has pointwise zero lifted divergence.
noncomputable def
EulerCorrectionAssembly.FiniteFamily.rawSourcePath
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(q : ℕ)
(hq : 6 ≤ q)
:
The actual continuous nonlinear raw source of each finite correction.
Equations
- EulerCorrectionAssembly.FiniteFamily.rawSourcePath period F q hq = EulerCorrectionLowerData.rawPath period hq (EulerAllOrderCorrectionData.Data.atOrder period A q) (F.solution q hq)
Instances For
noncomputable def
EulerCorrectionAssembly.FiniteFamily.signedPressurePath
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(q : ℕ)
(hq : 6 ≤ q)
:
The actual signed coercive pressure of each finite correction.
Equations
- EulerCorrectionAssembly.FiniteFamily.signedPressurePath period F q hq = EulerCorrectionLowerData.pressurePath period hq (EulerAllOrderCorrectionData.Data.atOrder period A q) (F.solution q hq)
Instances For
theorem
EulerCorrectionAssembly.FiniteFamily.rawSourcePath_truncate
(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.truncateOperator period q) ((rawSourcePath period F (q + 1) ⋯) t) = (rawSourcePath period F q hq) t
Proved correction compatibility gives exact restriction of the actual nonlinear sources.
theorem
EulerCorrectionAssembly.FiniteFamily.rawSourcePath_value_succ
(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 + 1) ⋯) t) = EulerCylinderSobolevSpace.value period ((rawSourcePath period F q hq) t)
Adjacent nonlinear source realizations have the same actual L² value.
theorem
EulerCorrectionAssembly.FiniteFamily.signedPressurePath_value_succ
(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 ((signedPressurePath period F (q + 1) ⋯) t) = EulerCylinderSobolevSpace.value period ((signedPressurePath period F q hq) t)
The genuine signed coercive pressures agree at adjacent Sobolev orders.
theorem
EulerCorrectionAssembly.FiniteFamily.signedPressurePath_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 ((signedPressurePath period F q hq) t) = EulerCylinderSobolevSpace.value period ((signedPressurePath period F 6 ⋯) t)
Every finite signed pressure is a realization of the same actual base pressure.
noncomputable def
EulerCorrectionAssembly.FiniteFamily.commonPressure
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
:
The actual common signed correction pressure is a continuous L² path.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionAssembly.FiniteFamily.signedPressurePath_value_common
(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 ((signedPressurePath period F q hq) t) = (commonPressure period F) t
Each finite pressure realizes the common actual signed pressure field.
theorem
EulerCorrectionAssembly.FiniteFamily.commonPressure_gradient
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(t : ↑(Set.Icc 0 T))
:
The actual common pressure lies in the closed lifted gradient space.
noncomputable def
EulerCorrectionAssembly.FiniteFamily.pressureJet
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(C : ComparisonData period hT A)
(n : ℕ)
(t : ↑(Set.Icc 0 T))
:
EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection n ((commonPressure period F) t)
The actual common pressure has genuine strong spatial jets of every order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionAssembly.FiniteFamily.commonPath_pressure_equation
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(F : FiniteFamily period hT A)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (EulerVolterraConvolution.extendPath T ⋯ (commonPath period F))
(-EulerCylinderSobolevSpace.value period ((rawSourcePath period F 6 ⋯) ⟨t, ⋯⟩) - (A.metric.coefficient ⟨t, ⋯⟩).operator ((commonPressure period F) ⟨t, ⋯⟩))
t
The common correction satisfies the literal equation with its reconstructed actual signed pressure.