The actual finite-Sobolev external transport commutator satisfies the Gevrey radius-loss bound.

@[instance_reducible]

noncomputable def EulerSobolevTransportCommutator.weightedCommGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevTransportCommutator.weightedCommGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevTransportCommutator.weightedCommSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerSobolevTransportCommutator.weightedCommSpace period q = inferInstance

noncomputable def EulerSobolevTransportCommutator.weightedLoss (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The actual finite weighted derivative-loss norm.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSobolevTransportCommutator.weightedLoss_nonneg (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : 0 ≤ weightedLoss period q N ρ u

theorem EulerSobolevTransportCommutator.continuous_weightedLoss (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) : Continuous (weightedLoss period q N ρ)

Continuity of the actual finite loss norm.

theorem EulerSobolevTransportCommutator.weightedNorm_eq_classical (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : EulerSobolevGevreyOperators.weightedNorm period q N ρ u = ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period q n f

Exact identification of weighted complete-Sobolev blocks with classical representative norms.

theorem EulerSobolevTransportCommutator.weightedLoss_eq_classical (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : weightedLoss period q N ρ u = ∑ n ∈ Finset.range (N + 1), ↑n * EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period q n f

The same exact identification for the derivative-loss norm.

noncomputable def EulerSobolevTransportCommutator.weightedCommutatorNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : ℝ

Weighted sum of the genuine H⁶ external transport commutators.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSobolevTransportCommutator.continuous_weightedCommutatorNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : Continuous fun (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) => weightedCommutatorNorm period hs N hN ρ L hL p.1 p.2

The weighted commutator expression is continuous in its actual finite-Sobolev inputs.

theorem EulerSobolevTransportCommutator.weightedCommutator_smooth_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : weightedCommutatorNorm period hs N hN ρ L hL u v ≤ 4 * EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * weightedLoss period 6 N ρ v

The external commutator bound for actual smooth representatives depends only on derivatives inside the energy cutoff.

theorem EulerSobolevTransportCommutator.weightedCommutator_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : weightedCommutatorNorm period hs N hN ρ L hL u v ≤ 4 * EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * weightedLoss period 6 N ρ v

The genuine finite-Sobolev external transport commutator has the cutoff-independent radius-loss bound. One additional derivative is used only to define the individual terms; it does not occur in the bound.