Actual nonlinear correction mild solutions obey the full-order continuous scalar integral energy estimate.
noncomputable def
EulerCorrectionMildEnergy.correctionRhs
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : ℝ}
{hq : 6 ≤ q + 1}
{D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)}
{N : ℕ}
{R : C(↑(Set.Icc 0 T), ℝ)}
(S : EulerCorrectionEnergyData.SpatialBudget period hq D N R)
(hN : N + 6 ≤ q + 1)
{hT : 0 ≤ T}
(K : EulerCorrectionEnergyData.MetricBudget period T hT D)
(Rdot : C(↑(Set.Icc 0 T), ℝ))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual continuous scalar right-hand side of the nonlinear correction energy estimate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionMildEnergy.correction_mild_integral
(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))
(hGq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t))
(hLq : Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t))
(hQq :
∀ (i : Fin 3),
Continuous fun (t : ↑(Set.Icc 0 T)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t))
(hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator)
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(R Rdot : C(↑(Set.Icc 0 T), ℝ))
(S : EulerCorrectionEnergyData.SpatialBudget period ⋯ D N R)
(K : EulerCorrectionEnergyData.MetricBudget period T hT D)
(hRd :
∀ t ∈ Set.Ioo 0 T,
HasDerivAt (EulerVolterraConvolution.extendPath T hT R) (EulerVolterraConvolution.extendPath T hT Rdot t) t)
(ν : ℝ)
(hν : 0 < ν)
(hν1 : ν ≤ 1)
(e₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
e t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) e₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r)
(EulerVolterraConvolution.extendPath T hT
(EulerCorrectionLowerData.forcingPath period hq
(EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) e)
(↑t - r)))
(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)
(s t : ℝ)
(h0s : 0 ≤ s)
(hst : s ≤ t)
(htT : t ≤ T)
:
(EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e)
⟨t, ⋯⟩ - (EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e)
⟨s, ⋯⟩ ≤ ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT (correctionRhs period S hN K Rdot e) r
The actual nonlinear lower mild equation yields the full energy-order scalar integral bound on every subinterval. Maximal regularity, the higher nonlinear source, the pressure, and their constraints are all constructed or proved inside the argument.