Exact restriction compatibility of actual finite Gevrey energies and derivative losses.
theorem
EulerGevreyRestriction.weightedNorm_restrict
(period : ℝ)
[Fact (0 < period)]
{p q : ℕ}
(hqp : q ≤ p)
(r N : ℕ)
(hN : N + r ≤ q)
(ρ : ℝ)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p))
:
EulerSobolevGevreyOperators.weightedNorm period r N ρ ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) = EulerSobolevGevreyOperators.weightedNorm period r N ρ u
Actual Gevrey norms are identical under every restriction retaining their derivative cutoff.
theorem
EulerGevreyRestriction.weightedLoss_restrict
(period : ℝ)
[Fact (0 < period)]
{p q : ℕ}
(hqp : q ≤ p)
(r N : ℕ)
(hN : N + r ≤ q)
(ρ : ℝ)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p))
:
EulerSobolevTransportCommutator.weightedLoss period r N ρ ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) = EulerSobolevTransportCommutator.weightedLoss period r N ρ u
The actual radius-loss sum is identical under every restriction retaining its cutoff.
theorem
EulerGevreyRestriction.wordAtLevel_restrict
(period : ℝ)
[Fact (0 < period)]
{p q r n : ℕ}
(hqp : q ≤ p)
(w : Fin n → Fin 4)
(hq : n + r ≤ q)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p))
:
(EulerSobolevWordLevel.wordAtLevel period r n w hq) ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) = (EulerSobolevWordLevel.wordAtLevel period r n w ⋯) u
Actual derivative words agree after restricting the input to any sufficiently high Sobolev level.
theorem
EulerGevreyRestriction.energyValues_restrict
(period : ℝ)
[Fact (0 < period)]
{p q : ℕ}
(hqp : q ≤ p)
(r N : ℕ)
(hN : N + r ≤ q)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p))
:
EulerGevreyMetricComparison.energyValues period r N hN ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) = EulerGevreyMetricComparison.energyValues period r N ⋯ u
Every literal metric-energy derivative is unchanged by a valid Sobolev restriction.
theorem
EulerGevreyRestriction.weightedNorm_truncate
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
(r N : ℕ)
(hN : N + r ≤ s)
(ρ : ℝ)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))
:
EulerSobolevGevreyOperators.weightedNorm period r N ρ ((EulerCylinderSobolevSpace.truncateOperator period s) u) = EulerSobolevGevreyOperators.weightedNorm period r N ρ u
The complete-solution truncation leaves every retained actual Gevrey norm unchanged.
theorem
EulerGevreyRestriction.weightedLoss_truncate
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
(r N : ℕ)
(hN : N + r ≤ s)
(ρ : ℝ)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))
:
EulerSobolevTransportCommutator.weightedLoss period r N ρ ((EulerCylinderSobolevSpace.truncateOperator period s) u) = EulerSobolevTransportCommutator.weightedLoss period r N ρ u
The complete-solution truncation leaves the retained radius-loss sum unchanged.