Actual metric Gevrey energy and radius loss as continuous paths, with exact higher-representative compatibility.
noncomputable def
EulerEnergyMetricPaths.energyPath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(T : ℝ)
(R : C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The genuine finite Gevrey metric energy along an actual continuous Sobolev solution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerEnergyMetricPaths.lossPath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(T : ℝ)
(R : C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The genuine radius-loss metric quantity along the same actual solution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerEnergyMetricPaths.energyPath_apply
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(T : ℝ)
(R : C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(t : ↑(Set.Icc 0 T))
:
(energyPath period N hN T R K e) t = EulerGevreyMetricEstimate.energyNorm period N hN (R t) (K t) (e t)
The continuous energy path is exactly the spatial metric norm at each time.
theorem
EulerEnergyMetricPaths.lossPath_apply
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(T : ℝ)
(R : C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(t : ↑(Set.Icc 0 T))
:
(lossPath period N hN T R K e) t = EulerGevreyMetricEstimate.energyLoss period N hN (R t) (K t) (e t)
The continuous loss path is exactly the spatial metric radius loss at each time.
theorem
EulerEnergyMetricPaths.energyNorm_of_value_eq
(period : ℝ)
[Fact (0 < period)]
{p q : ℕ}
(N : ℕ)
(hp : N + 6 ≤ p)
(hq : N + 6 ≤ q)
(ρ : ℝ)
(K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p))
(v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(huv : EulerCylinderSobolevSpace.value period u = EulerCylinderSobolevSpace.value period v)
:
EulerGevreyMetricEstimate.energyNorm period N hp ρ K u = EulerGevreyMetricEstimate.energyNorm period N hq ρ K v
Equal actual fields at adequate derivative orders have the same literal finite metric energy.
theorem
EulerEnergyMetricPaths.energyLoss_of_value_eq
(period : ℝ)
[Fact (0 < period)]
{p q : ℕ}
(N : ℕ)
(hp : N + 6 ≤ p)
(hq : N + 6 ≤ q)
(ρ : ℝ)
(K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p))
(v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(huv : EulerCylinderSobolevSpace.value period u = EulerCylinderSobolevSpace.value period v)
:
EulerGevreyMetricEstimate.energyLoss period N hp ρ K u = EulerGevreyMetricEstimate.energyLoss period N hq ρ K v
The identical representative principle holds for the actual radius-loss energy.
theorem
EulerEnergyMetricPaths.maximal_metric_paths
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(R : C(↑(Set.Icc 0 T), ℝ))
(K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
(hU :
Filter.Tendsto
(fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n e))
Filter.atTop (nhds U))
:
∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, EulerGevreyMetricEstimate.energyNorm period N ⋯ (R (Set.projIcc 0 T hT t)) (K (Set.projIcc 0 T hT t))
(↑↑(EulerSobolevWordValueIdentity.reindexMaximalTime period q T U) t) = (energyPath period N hN T R K e) (Set.projIcc 0 T hT t) ∧ EulerGevreyMetricEstimate.energyLoss period N ⋯ (R (Set.projIcc 0 T hT t)) (K (Set.projIcc 0 T hT t))
(↑↑(EulerSobolevWordValueIdentity.reindexMaximalTime period q T U) t) = (lossPath period N hN T R K e) (Set.projIcc 0 T hT t)
Genuine maximal-regularity representatives have exactly the original metric energy and loss almost everywhere in time.