The actual lower Sobolev equation and its continuous source and pressure paths.
Exact almost-everywhere restriction of the actual nonlinear source and pressure time fields.
@[instance_reducible]
noncomputable def
EulerTimeCorrectionSource.timeRestrictGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten
typeclass synthesis.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerTimeCorrectionSource.timeRestrictSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass
synthesis.
Equations
Instances For
noncomputable def
EulerTimeCorrectionSource.lowerRawValue
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ)
(hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1)
(C0 : EulerCorrectionOperators.CoefficientPath period (q + 1) ↑(Set.Icc 0 T))
(C : Fin 3 → EulerCorrectionOperators.CoefficientPath period (q + 1) ↑(Set.Icc 0 T))
(K0 :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (C0.coefficient t))
(K :
(i : Fin 3) →
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((C i).coefficient t))
(z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
(r e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(t : ↑(Set.Icc 0 T))
:
↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The literal lower-order raw correction source obtained from genuine higher coefficient data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTimeCorrectionSource.rawSourceTime_restriction
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(hT : 0 ≤ T)
(L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ)
(hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1)
(C0 : EulerCorrectionOperators.CoefficientPath period (q + 1) ↑(Set.Icc 0 T))
(C : Fin 3 → EulerCorrectionOperators.CoefficientPath period (q + 1) ↑(Set.Icc 0 T))
(K0 :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (C0.coefficient t))
(K :
(i : Fin 3) →
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((C i).coefficient t))
(z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
(r e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
(hU :
(fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT e)
:
(fun (t : ℝ) =>
(EulerCylinderSobolevSpace.truncateOperator period q)
(↑↑(rawSourceTime period ⋯ T hT L hL (EulerCorrectionOperators.CoefficientPath.operatorPath period C0)
(fun (i : Fin 3) => EulerCorrectionOperators.CoefficientPath.operatorPath period (C i)) z r e U)
t)) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => lowerRawValue period hq T L hL C0 C K0 K z r e (Set.projIcc 0 T hT t)
The constructed energy-order raw source is a genuine higher regularity representative of the original correction source.
theorem
EulerTimeCorrectionSource.pressureTime_restriction
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(hT : 0 ≤ T)
(G : EulerCorrectionOperators.CoefficientPath period (q + 1) ↑(Set.Icc 0 T))
(K :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (G.coefficient t))
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v)
(F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(f : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] f)
:
(fun (t : ℝ) =>
(EulerCylinderSobolevSpace.truncateOperator period q)
(↑↑(pressureTime period T hT G κ m c hc hpos F) t)) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
-(EulerSobolevCoefficientPressure.pressureSobolevOperator period (K (Set.projIcc 0 T hT t)) κ m c hc ⋯) (f t)
Actual signed coercive pressure commutes with the energy-to-source Sobolev restriction almost everywhere.
theorem
EulerTimeCorrectionSource.projectedTime_restriction
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(T : ℝ)
(hT : 0 ≤ T)
(G : EulerCorrectionOperators.CoefficientPath period (q + 1) ↑(Set.Icc 0 T))
(K :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (G.coefficient t))
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ (((G.coefficient t).coefficient x) v) v)
(F : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(f : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(hF : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (↑↑F t)) =ᵐ[EulerTimeLp.timeMeasure T] f)
:
(fun (t : ℝ) =>
(EulerCylinderSobolevSpace.truncateOperator period q)
(↑↑(projectedTime period T hT G κ m c hc hpos F) t)) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
-(EulerSobolevCoefficientPressure.projectedSourceOperator period (K (Set.projIcc 0 T hT t)) κ m c hc ⋯) (f t)
The actual projected nonlinear mild source restricts to the original forcing almost everywhere.
@[instance_reducible]
noncomputable def
EulerCorrectionLowerData.lowerDataGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
A local normed-group instance for the concrete lower Sobolev scale.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionLowerData.lowerDataSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
A local real normed-space instance for the concrete lower Sobolev scale.
Equations
Instances For
noncomputable def
EulerCorrectionLowerData.lowerData
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(KG :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t))
(KL :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t))
(KQ :
(i : Fin 3) →
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q
((D.quadratic i).coefficient t))
(hG : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t))
(hL : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t))
(hQ :
∀ (i : Fin 3),
Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t))
:
EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)
The same genuine correction coefficients and background restricted by one Sobolev order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionLowerData.rawPath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual nonlinear raw source along a continuous Sobolev path is continuous.
Equations
- EulerCorrectionLowerData.rawPath period hq D e = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerCorrectionOperators.CorrectionData.rawSource period D hq t (e t), continuous_toFun := ⋯ }
Instances For
noncomputable def
EulerCorrectionLowerData.forcingPath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual projected nonlinear mild forcing along the continuous solution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionLowerData.pressurePath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual signed coercive pressure along the continuous solution is continuous.
Equations
- EulerCorrectionLowerData.pressurePath period hq D e = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerCorrectionOperators.CorrectionData.pressure period D hq t (e t), continuous_toFun := ⋯ }
Instances For
theorem
EulerCorrectionLowerData.rawPath_lower
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(KG :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t))
(KL :
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t))
(KQ :
(i : Fin 3) →
(t : ↑(Set.Icc 0 T)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q
((D.quadratic i).coefficient t))
(hG : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t))
(hL : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t))
(hQ :
∀ (i : Fin 3),
Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(t : ↑(Set.Icc 0 T))
:
(rawPath period hq (lowerData period D KG KL KQ hG hL hQ) e) t = EulerTimeCorrectionSource.lowerRawValue period hq T (EulerSobolevTransport.velocityComponents D.κ D.direction) ⋯
D.linear D.quadratic KL KQ D.approximation D.residual e t
The actual lower raw source is exactly the lower restriction used by the constructed Bochner source.
theorem
EulerCorrectionLowerData.pressurePath_gradient
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(t : ↑(Set.Icc 0 T))
:
EulerCylinderSobolevSpace.value period ((pressurePath period hq D e) t) ∈ EulerLiftedGradientSpace.gradientSpace period D.κ D.direction
The actual continuous pressure path lies in the genuine lifted gradient space at every time.