Expanding spatial cutoffs and transport cancellation for noncompact fields on the cylinder.

def EulerNoncompactTransport.spatialBump : ContDiffBump 0

A fixed smooth spatial cutoff equal to one on the unit ball.

Equations

• EulerNoncompactTransport.spatialBump = { rIn := 1, rOut := 2, rIn_pos := EulerNoncompactTransport.spatialBump._proof_1, rIn_lt_rOut := EulerNoncompactTransport.spatialBump._proof_2 }

noncomputable def EulerNoncompactTransport.cutoffScale (n : ℕ) : ℝ

The reciprocal spatial scale in the expanding cutoff sequence.

Equations

• EulerNoncompactTransport.cutoffScale n = (↑n + 1)⁻¹

noncomputable def EulerNoncompactTransport.spatialCutoff (period : ℝ) (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) : ℝ

Smooth expanding cutoffs on the cylinder; the angular variable is unchanged.

Equations

• EulerNoncompactTransport.spatialCutoff period n x = ↑EulerNoncompactTransport.spatialBump (EulerNoncompactTransport.cutoffScale n • x.1)

theorem EulerNoncompactTransport.cutoffScale_pos (n : ℕ) : 0 < cutoffScale n

theorem EulerNoncompactTransport.cutoffScale_le_one (n : ℕ) : cutoffScale n ≤ 1

theorem EulerNoncompactTransport.cutoffScale_tendsto : Filter.Tendsto cutoffScale Filter.atTop (nhds 0)

theorem EulerNoncompactTransport.spatialCutoff_bounds (period : ℝ) (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) : 0 ≤ spatialCutoff period n x ∧ spatialCutoff period n x ≤ 1

theorem EulerNoncompactTransport.spatialCutoff_smooth (period : ℝ) (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period (spatialCutoff period n) x)

theorem EulerNoncompactTransport.spatialCutoff_tendsto (period : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : Filter.Tendsto (fun (n : ℕ) => spatialCutoff period n x) Filter.atTop (nhds 1)

theorem EulerNoncompactTransport.spatialCutoff_compact (period : ℝ) [Fact (0 < period)] (n : ℕ) : HasCompactSupport (spatialCutoff period n)

theorem EulerNoncompactTransport.spatialCutoff_fderiv (period : ℝ) (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.LiftTangent) : (fderiv ℝ (EulerLiftedGradientSpace.localLift period (spatialCutoff period n) x) 0) v = (fderiv ℝ (↑spatialBump) (cutoffScale n • x.1)) (cutoffScale n • v.1)

theorem EulerNoncompactTransport.spatialCutoff_derivative_bound (period : ℝ) : ∃ (M : ℝ), 0 < M ∧ ∀ (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.LiftTangent), ‖(fderiv ℝ (EulerLiftedGradientSpace.localLift period (spatialCutoff period n) x) 0) v‖ ≤ M * cutoffScale n * ‖v‖

The cutoff derivatives have a uniform constant times their reciprocal spatial scale.

theorem EulerNoncompactTransport.spatialCutoff_derivative_tendsto (period : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.LiftTangent) : Filter.Tendsto (fun (n : ℕ) => (fderiv ℝ (EulerLiftedGradientSpace.localLift period (spatialCutoff period n) x) 0) v) Filter.atTop (nhds 0)

theorem EulerNoncompactTransport.cutoff_product_transport (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period φ x)) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3) : inner ℝ (EulerLiftedGradientSpace.liftedGradient period κ m (fun (y : EulerLiftedGradientSpace.LiftDomain period) => spatialCutoff period n y * φ y) x) v = spatialCutoff period n x * (fderiv ℝ (EulerLiftedGradientSpace.localLift period φ x) 0) (EulerMetricTransport.transportDirection κ m v) + φ x * (fderiv ℝ (EulerLiftedGradientSpace.localLift period (spatialCutoff period n) x) 0) (EulerMetricTransport.transportDirection κ m v)

theorem EulerNoncompactTransport.weak_divergence_integral_noncompact (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (B : ℝ) (_hB : 0 ≤ B) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ B) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period φ x)) (hφI : MeasureTheory.Integrable φ (EulerLiftedGradientSpace.liftMeasure period)) (hflux : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => (fderiv ℝ (EulerLiftedGradientSpace.localLift period φ x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) (EulerLiftedGradientSpace.liftMeasure period)) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), (fderiv ℝ (EulerLiftedGradientSpace.localLift period φ x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x)) ∂EulerLiftedGradientSpace.liftMeasure period = 0

Smooth scalar weak-divergence tests extend to integrable noncompact energies.

theorem EulerNoncompactTransport.metric_transport_noncompact_by_parts (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (B : ℝ) (hB : 0 ≤ B) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ B) (hE : MeasureTheory.Integrable (EulerMetricTransport.metricEnergy period K e) (EulerLiftedGradientSpace.liftMeasure period)) (hT : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => inner ℝ ((K x) (e x)) ((fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x)))) (EulerLiftedGradientSpace.liftMeasure period)) (hQ : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => 1 / 2 * inner ℝ (((fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) (e x)) (e x)) (EulerLiftedGradientSpace.liftMeasure period)) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (e x)) ((fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period = -∫ (x : EulerLiftedGradientSpace.LiftDomain period), 1 / 2 * inner ℝ (((fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) (e x)) (e x) ∂EulerLiftedGradientSpace.liftMeasure period

Integration by parts for a noncompact smooth metric energy with integrable terms.

theorem EulerNoncompactTransport.aestronglyMeasurable_apply (period : ℝ) [Fact (0 < period)] {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {A : EulerLiftedGradientSpace.LiftDomain period → V →L[ℝ] W} {u : EulerLiftedGradientSpace.LiftDomain period → V} (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (hu : MeasureTheory.AEStronglyMeasurable u (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.AEStronglyMeasurable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => (A x) (u x)) (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerNoncompactTransport.metricEnergy_integrable (period : ℝ) [Fact (0 < period)] (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : MeasureTheory.AEStronglyMeasurable K (EulerLiftedGradientSpace.liftMeasure period)) (he : MeasureTheory.MemLp e 2 (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hC : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C) : MeasureTheory.Integrable (EulerMetricTransport.metricEnergy period K e) (EulerLiftedGradientSpace.liftMeasure period)

Bounded metrics have integrable quadratic energy on every actual L² field.

theorem EulerNoncompactTransport.transportDirection_aestronglyMeasurable (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) : MeasureTheory.AEStronglyMeasurable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerMetricTransport.transportDirection κ m (↑↑z x)) (EulerLiftedGradientSpace.liftMeasure period)

The actual lifted transport velocity of an L² field is measurable.

theorem EulerNoncompactTransport.metricTransport_integrable (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : MeasureTheory.AEStronglyMeasurable K (EulerLiftedGradientSpace.liftMeasure period)) (he : MeasureTheory.MemLp e 2 (EulerLiftedGradientSpace.liftMeasure period)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (C B : NNReal) (hC : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hz : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖EulerMetricTransport.transportDirection κ m (↑↑z x)‖ ≤ ↑B) : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => inner ℝ ((K x) (e x)) ((fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x)))) (EulerLiftedGradientSpace.liftMeasure period)

The principal transport pairing is integrable for smooth H¹ fields and bounded velocity.

theorem EulerNoncompactTransport.metricCorrection_pointwise_bound (period : ℝ) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (D B : NNReal) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.LiftTangent) (hD : ‖fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0‖ ≤ ↑D) (hv : ‖v‖ ≤ ↑B) : ‖1 / 2 * inner ℝ (((fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0) v) (e x)) (e x)‖ ≤ 1 / 2 * ↑D * ↑B * ‖e x‖ ^ 2

theorem EulerNoncompactTransport.metricCorrection_integrable (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hDK : MeasureTheory.AEStronglyMeasurable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0) (EulerLiftedGradientSpace.liftMeasure period)) (he : MeasureTheory.MemLp e 2 (EulerLiftedGradientSpace.liftMeasure period)) (D B : NNReal) (hD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0‖ ≤ ↑D) (z : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hz : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖EulerMetricTransport.transportDirection κ m (↑↑z x)‖ ≤ ↑B) : MeasureTheory.Integrable (fun (x : EulerLiftedGradientSpace.LiftDomain period) => 1 / 2 * inner ℝ (((fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) (e x)) (e x)) (EulerLiftedGradientSpace.liftMeasure period)

The metric correction is integrable for L² fields and bounded metric derivative and velocity.

theorem EulerNoncompactTransport.metric_transport_H1_bound (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x)) (heLp : MeasureTheory.MemLp e 2 (EulerLiftedGradientSpace.liftMeasure period)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (C D B : NNReal) (hC : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C) (hD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0‖ ≤ ↑D) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : |∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (e x)) ((fderiv ℝ (EulerMetricTransport.localFieldLift period e x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period| ≤ 1 / 2 * ↑D * ((|κ| + ‖m‖) * ↑B) * ∫ (x : EulerLiftedGradientSpace.LiftDomain period), ‖e x‖ ^ 2 ∂EulerLiftedGradientSpace.liftMeasure period

The genuine noncompact H¹ metric transport estimate; no cancellation is assumed.

theorem EulerNoncompactTransport.metric_transport_L2_H1_bound (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (e : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hK : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period K x)) (he : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => ↑↑e y) x)) (hDe : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => ↑↑e y) x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hsym : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ ((K x) v) w = inner ℝ v ((K x) w)) {z : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hz : z ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (C D B : NNReal) (hC : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖K x‖ ≤ ↑C) (hD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period K x) 0‖ ≤ ↑D) (hzB : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑z x‖ ≤ ↑B) : |∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((K x) (↑↑e x)) ((fderiv ℝ (EulerMetricTransport.localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => ↑↑e y) x) 0) (EulerMetricTransport.transportDirection κ m (↑↑z x))) ∂EulerLiftedGradientSpace.liftMeasure period| ≤ 1 / 2 * ↑D * ((|κ| + ‖m‖) * ↑B) * ‖e‖ ^ 2

The noncompact transport estimate expressed in the genuine L² Hilbert norm.