Genuine finite-Sobolev norms of the small four-component transport drift.

noncomputable def EulerSobolevDriftNorm.driftWordOperator (period : ℝ) [Fact (0 < period)] {s : ℕ} (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (w : EulerCylinderSobolevSpace.SobolevWord s) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(MeasureTheory.Lp (EulerSobolev.Domain 4) 2 (EulerLiftedGradientSpace.liftMeasure period))

Postcomposition of an actual derivative coordinate with the fixed drift map.

Equations

• EulerSobolevDriftNorm.driftWordOperator period L w = ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure period) L ∘SL EulerCylinderSobolevSpace.wordOperator period w

noncomputable def EulerSobolevDriftNorm.driftLevelNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The exact sum of L² norms of drift derivatives at one total derivative order.

Equations

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

noncomputable def EulerSobolevDriftNorm.driftBlockNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The drift norm at one external order, including all derivatives in the fixed base Sobolev block.

Equations

• EulerSobolevDriftNorm.driftBlockNorm period q n L u = ∑ r ∈ Finset.range (q + 1), EulerSobolevDriftNorm.driftLevelNorm period (n + r) L u

noncomputable def EulerSobolevDriftNorm.weightedDriftNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ℝ

The weighted genuine drift norm, retaining cancellations in the fixed velocity map.

Equations

• EulerSobolevDriftNorm.weightedDriftNorm period q N ρ L u = ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerSobolevDriftNorm.driftBlockNorm period q n L u

theorem EulerSobolevDriftNorm.driftWordOperator_eq (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : (ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure period) L) ((EulerCylinderSobolevSpace.toJet period u).word w) = (driftWordOperator period L ⟨⟨n, ⋯⟩, w⟩) u

theorem EulerSobolevDriftNorm.driftLevelNorm_nonneg (period : ℝ) [Fact (0 < period)] {s : ℕ} (n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : 0 ≤ driftLevelNorm period n L u

theorem EulerSobolevDriftNorm.driftBlockNorm_nonneg (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : 0 ≤ driftBlockNorm period q n L u

theorem EulerSobolevDriftNorm.weightedDriftNorm_nonneg (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : 0 ≤ weightedDriftNorm period q N ρ L u

theorem EulerSobolevDriftNorm.continuous_driftLevelNorm (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) : Continuous (driftLevelNorm period n L)

Valid drift coordinates are continuous on the complete finite Sobolev space.

theorem EulerSobolevDriftNorm.continuous_driftBlockNorm (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (h : n + q ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) : Continuous (driftBlockNorm period q n L)

theorem EulerSobolevDriftNorm.continuous_weightedDriftNorm_pair (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) : Continuous fun (p : ℝ × ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) => weightedDriftNorm period q N p.1 L p.2

Joint continuity in radius and field follows directly from finite sums of continuous linear coordinates.

theorem EulerSobolevDriftNorm.continuous_weightedDriftNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) : Continuous (weightedDriftNorm period q N ρ L)

theorem EulerSobolevDriftNorm.driftLevelNorm_add_le (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : driftLevelNorm period n L (u + v) ≤ driftLevelNorm period n L u + driftLevelNorm period n L v

The drift norm is subadditive without discarding its directional cancellations.

theorem EulerSobolevDriftNorm.weightedDriftNorm_add_le (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedDriftNorm period q N ρ L (u + v) ≤ weightedDriftNorm period q N ρ L u + weightedDriftNorm period q N ρ L v

theorem EulerSobolevDriftNorm.driftLevelNorm_le (period : ℝ) [Fact (0 < period)] {s : ℕ} (n : ℕ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : driftLevelNorm period n L u ≤ ‖L‖ * EulerJetProductBounds.levelNorm period (EulerCylinderSobolevSpace.toJet period u) n

The coarse comparison is used for the correction field, not for the prescribed drift.

theorem EulerSobolevDriftNorm.weightedDriftNorm_le_weightedNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedDriftNorm period q N ρ L u ≤ ‖L‖ * EulerSobolevGevreyOperators.weightedNorm period q N ρ u

theorem EulerSobolevDriftNorm.velocityMap_norm_le_four (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : ‖EulerFunctionalVelocity.velocityMap L‖ ≤ 4

Four contractive coordinate functionals assemble into a map of norm at most four.

theorem EulerSobolevDriftNorm.weightedDriftNorm_velocityMap_le (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedDriftNorm period q N ρ (EulerFunctionalVelocity.velocityMap L) u ≤ 4 * EulerSobolevGevreyOperators.weightedNorm period q N ρ u

theorem EulerSobolevDriftNorm.wordSobolevNorm_eq_total (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (q n : ℕ) (f : EulerLiftedGradientSpace.LiftDomain period → F) : EulerH6Nonlinear.wordSobolevNorm period q n f = ∑ r ∈ Finset.range (q + 1), ∑ w : Fin (n + r) → Fin 4, (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

External-word Sobolev blocks equal the sum over the corresponding total derivative orders.

theorem EulerSobolevDriftNorm.driftWord_ae (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (w : Fin n → Fin 4) (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)) : ↑↑((ContinuousLinearMap.compLpL 2 (EulerLiftedGradientSpace.liftMeasure period) L) ((EulerCylinderSobolevSpace.toJet period u).word w)) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerCylinderSobolev.iteratedFieldDerivative period w (⇑L ∘ f)

Each postcomposed strong word agrees almost everywhere with the actual classical drift derivative.

theorem EulerSobolevDriftNorm.driftLevelNorm_eq_classical (period : ℝ) [Fact (0 < period)] {s n : ℕ} (hn : n ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (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)) : driftLevelNorm period n L u = ∑ w : Fin n → Fin 4, (MeasureTheory.eLpNorm (EulerCylinderSobolev.iteratedFieldDerivative period w (⇑L ∘ f)) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

theorem EulerSobolevDriftNorm.driftBlockNorm_eq_classical (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (h : n + q ≤ s) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (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)) : driftBlockNorm period q n L u = EulerH6Nonlinear.wordSobolevNorm period q n (⇑L ∘ f)

The rough drift block is exactly the classical external-word Sobolev norm on every smooth representative.

theorem EulerSobolevDriftNorm.weightedDriftNorm_eq_classical (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (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)) : weightedDriftNorm period q N ρ L u = ∑ n ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ n * EulerH6Nonlinear.wordSobolevNorm period q n (⇑L ∘ f)

Exact representative identity for the finite weighted drift norm.

theorem EulerSobolevDriftNorm.driftLevelNorm_restrict (period : ℝ) [Fact (0 < period)] {s t n : ℕ} (h : t ≤ s) (hn : n ≤ t) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : driftLevelNorm period n L ((EulerCylinderSobolevSpace.restrictOperator period h) u) = driftLevelNorm period n L u

Restriction of the finite Sobolev ambient space preserves each retained drift coordinate.

theorem EulerSobolevDriftNorm.weightedDriftNorm_restrict (period : ℝ) [Fact (0 < period)] {s t : ℕ} (h : t ≤ s) (q N : ℕ) (hN : N + q ≤ t) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : weightedDriftNorm period q N ρ L ((EulerCylinderSobolevSpace.restrictOperator period h) u) = weightedDriftNorm period q N ρ L u

theorem EulerSobolevDriftNorm.weightedDriftNorm_truncate (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : weightedDriftNorm period q N ρ L ((EulerCylinderSobolevSpace.truncateOperator period s) u) = weightedDriftNorm period q N ρ L u

theorem EulerSobolevDriftNorm.weightedDriftNorm_smoothApprox_tendsto (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : Filter.Tendsto (fun (n : ℕ) => weightedDriftNorm period q N ρ L ((EulerCylinderSobolevSpace.restrictOperator period ⋯) ((EulerCylinderSobolevSpace.smoothApprox period s n) u))) Filter.atTop (nhds (weightedDriftNorm period q N ρ L u))

Actual smooth approximations converge in the drift norm at every retained weighted cutoff.

theorem EulerSobolevDriftNorm.weightedDriftNorm_zero (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) : weightedDriftNorm period q N ρ L 0 = 0

A zero field has zero drift at every valid weighted cutoff.

theorem EulerSobolevDriftNorm.weightedDriftNorm_smoothApprox_sub_tendsto (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerSobolev.Domain 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : Filter.Tendsto (fun (n : ℕ) => weightedDriftNorm period q N ρ L ((EulerCylinderSobolevSpace.restrictOperator period ⋯) ((EulerCylinderSobolevSpace.smoothApprox period s n) u) - u)) Filter.atTop (nhds 0)

Smoothing errors themselves tend to zero in the genuine drift norm.