The actual viscous derivative expressed using the identical lower-order nonlinear source.
The actual viscous derivative expressed using the identical lower-order nonlinear source.
@[instance_reducible]
noncomputable def
EulerCorrectionLimitDerivative.limitDerivativeGroup
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
:
The inherited normed group on each actual Sobolev value space.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionLimitDerivative.limitDerivativeSpace
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period s)
The inherited real normed space on each actual Sobolev value space.
Equations
Instances For
theorem
EulerCorrectionLimitDerivative.lower_mild_value_derivative
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(hT : 0 ≤ 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))
(ν : ℝ)
(hν : 0 < ν)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = EulerQuadraticSource.quadraticDuhamel period ν hν hT ⋯
(EulerCorrectionOperators.CorrectionData.coefficients period D ⋯) 0 u t)
(r : ℝ)
(hr : r ∈ Set.Ioo 0 T)
:
HasDerivAt (fun (x : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u x))
(ν • (EulerSobolevHeatGenerator.laplacianEvaluation period (q + 1 + 1) ⋯) (u ⟨r, ⋯⟩) + EulerCylinderSobolevSpace.value period
((EulerCorrectionOperators.CorrectionData.coefficients period
(EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq).apply
⟨r, ⋯⟩ ((EulerCylinderSobolevSpace.truncateOperator period (q + 1)) (u ⟨r, ⋯⟩))))
r
The actual derivative of a high-order mild correction equals viscosity plus the literal lower-order nonlinear source.
A pointwise viscous derivative expressed as a continuous path.
theorem
EulerViscousPathDerivative.hasDerivAt_path
(period : ℝ)
[Fact (0 < period)]
{s q : ℕ}
(hs : 2 ≤ s)
(ν T : ℝ)
(hT : 0 ≤ T)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(r : ℝ)
(hr : r ∈ Set.Ioo 0 T)
(hd :
HasDerivAt (fun (x : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u x))
(ν • (EulerSobolevHeatGenerator.laplacianEvaluation period s hs) (u ⟨r, ⋯⟩) + EulerCylinderSobolevSpace.value period (f ⟨r, ⋯⟩))
r)
:
HasDerivAt (EulerVolterraConvolution.extendPath T hT (EulerViscosityCauchy.valuePath period T u))
(EulerVolterraConvolution.extendPath T hT
(EulerViscosityDefect.viscousDefect period hs ν T u + EulerViscosityCauchy.valuePath period T f) r)
r
The actual pointwise viscous derivative equals evaluation of its continuous source path.
@[instance_reducible]
noncomputable def
EulerCorrectionLimitPathDerivative.limitDerivativeGroup
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
:
The inherited normed group on each actual Sobolev value space.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionLimitPathDerivative.limitDerivativeSpace
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period s)
The inherited real normed space on each actual Sobolev value space.
Equations
Instances For
theorem
EulerCorrectionLimitPathDerivative.lower_mild_path_derivative
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(T : ℝ)
(hT : 0 ≤ 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))
(ν : ℝ)
(hν : 0 < ν)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = EulerQuadraticSource.quadraticDuhamel period ν hν hT ⋯
(EulerCorrectionOperators.CorrectionData.coefficients period D ⋯) 0 u t)
(r : ℝ)
(hr : r ∈ Set.Ioo 0 T)
:
HasDerivAt (EulerVolterraConvolution.extendPath T hT (EulerViscosityCauchy.valuePath period T u))
(EulerVolterraConvolution.extendPath T hT
(EulerViscosityDefect.viscousDefect period ⋯ ν T u + EulerViscosityCauchy.valuePath period T
(EulerQuadraticSourceLimit.sourcePath
(EulerCorrectionOperators.CorrectionData.coefficients period
(EulerCorrectionLowerData.lowerData period D KG KL KQ hG hL hQ) hq)
((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T))
(EulerCylinderSobolevSpace.truncateOperator period (q + 1)))
u)))
r)
r
The actual derivative of a high-order mild correction equals viscosity plus the literal lower-order nonlinear source.