A genuine ordinary-space cutoff-curl dual estimate. All spatial norms and integrals in this file use Lebesgue measure on Euclidean three-space.

noncomputable def EulerMeanCutoffCurl.vectorCurl (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Curl of a vector-valued field, using the existing coordinate curl.

Equations

• EulerMeanCutoffCurl.vectorCurl f = EulerVectorCalculus.curl fun (i : Fin 3) (x : EulerSmoothLimit.Space) => (f x).ofLp i

noncomputable def EulerMeanCutoffCurl.sobolevConstant : NNReal

The fixed homogeneous Sobolev constant for dimension three and exponent two.

Equations

• EulerMeanCutoffCurl.sobolevConstant = MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst MeasureTheory.volume 2

theorem EulerMeanCutoffCurl.homogeneous_sobolev (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : MeasureTheory.lpNorm f 6 MeasureTheory.volume ≤ ↑sobolevConstant * MeasureTheory.lpNorm (fderiv ℝ f) 2 MeasureTheory.volume

The ordinary homogeneous Sobolev inequality, with no dependence on support size.

theorem EulerMeanCutoffCurl.norm_le_sum_coordinates (v : EulerSmoothLimit.Space) : ‖v‖ ≤ ∑ i : Fin 3, ‖v.ofLp i‖

A three-vector's Euclidean norm is at most the sum of its component norms.

theorem EulerMeanCutoffCurl.norm_vectorCurl_le (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hf : DifferentiableAt ℝ f x) : ‖vectorCurl f x‖ ≤ 6 * ‖fderiv ℝ f x‖

The coordinate definition of curl is bounded by six times the full derivative norm.

theorem EulerMeanCutoffCurl.norm_cutoff_curl_le (ψ : EulerSmoothLimit.Space → ℝ) (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hψ : DifferentiableAt ℝ ψ x) (hφ : DifferentiableAt ℝ φ x) : ‖vectorCurl (fun (y : EulerSmoothLimit.Space) => ψ y • φ y) x‖ ≤ 6 * (‖ψ x‖ * ‖fderiv ℝ φ x‖ + ‖fderiv ℝ ψ x‖ * ‖φ x‖)

The actual cutoff product rule gives the pointwise bound used in the dual estimate.

theorem EulerMeanCutoffCurl.lpNorm_norm_mul_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : EulerSmoothLimit.Space → E} {g : EulerSmoothLimit.Space → F} {p q r : ENNReal} [p.HolderTriple q r] (hf : MeasureTheory.MemLp f p MeasureTheory.volume) (hg : MeasureTheory.MemLp g q MeasureTheory.volume) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => ‖f x‖ * ‖g x‖) r MeasureTheory.volume ≤ MeasureTheory.lpNorm f p MeasureTheory.volume * MeasureTheory.lpNorm g q MeasureTheory.volume

Hölder's inequality for the product of the pointwise norms, in real-valued Lp norms.

theorem EulerMeanCutoffCurl.vectorCurl_memLp (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : MeasureTheory.MemLp (vectorCurl f) 2 MeasureTheory.volume

Smooth compactly supported vector fields have square-integrable actual curl.

theorem EulerMeanCutoffCurl.cutoff_curl_lpNorm_le (ψ : EulerSmoothLimit.Space → ℝ) (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : MeasureTheory.lpNorm (vectorCurl fun (x : EulerSmoothLimit.Space) => ψ x • φ x) 2 MeasureTheory.volume ≤ 6 * (MeasureTheory.lpNorm ψ ⊤ MeasureTheory.volume + ↑sobolevConstant * MeasureTheory.lpNorm (fderiv ℝ ψ) 3 MeasureTheory.volume) * MeasureTheory.lpNorm (fderiv ℝ φ) 2 MeasureTheory.volume

The actual L² cutoff-curl estimate, retaining the two Hölder terms.

theorem EulerMeanCutoffCurl.norm_gradient_eq_fderiv (ψ : EulerSmoothLimit.Space → ℝ) (x : EulerSmoothLimit.Space) : ‖gradient ψ x‖ = ‖fderiv ℝ ψ x‖

The norm of a scalar gradient equals the norm of its Fréchet derivative.

theorem EulerMeanCutoffCurl.lpNorm_gradient_eq_fderiv (ψ : EulerSmoothLimit.Space → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) : MeasureTheory.lpNorm (gradient ψ) 3 MeasureTheory.volume = MeasureTheory.lpNorm (fderiv ℝ ψ) 3 MeasureTheory.volume

The L³ cutoff derivative norm can equivalently be written using its actual gradient.

noncomputable def EulerMeanCutoffCurl.cutoffCurlConstant : ℝ

A dimension-only constant, independent of the cutoff, test field, and support radii.

Equations

• EulerMeanCutoffCurl.cutoffCurlConstant = 6 * (1 + ↑EulerMeanCutoffCurl.sobolevConstant)

theorem EulerMeanCutoffCurl.cutoffCurlConstant_pos : 0 < cutoffCurlConstant

theorem EulerMeanCutoffCurl.cutoff_curl_bound (ψ : EulerSmoothLimit.Space → ℝ) (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : MeasureTheory.lpNorm (vectorCurl fun (x : EulerSmoothLimit.Space) => ψ x • φ x) 2 MeasureTheory.volume ≤ cutoffCurlConstant * (MeasureTheory.lpNorm ψ ⊤ MeasureTheory.volume + MeasureTheory.lpNorm (gradient ψ) 3 MeasureTheory.volume) * MeasureTheory.lpNorm (fderiv ℝ φ) 2 MeasureTheory.volume

The source's ordinary-space cutoff-curl bound with the actual gradient L³ norm.

theorem EulerMeanCutoffCurl.integral_cutoff_curl_bound (ψ : EulerSmoothLimit.Space → ℝ) (φ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (z : ↥(MeasureTheory.Lp EulerSmoothLimit.Space 2 MeasureTheory.volume)) : |∫ (x : EulerSmoothLimit.Space), inner ℝ (↑↑z x) (vectorCurl (fun (y : EulerSmoothLimit.Space) => ψ y • φ y) x)| ≤ cutoffCurlConstant * (MeasureTheory.lpNorm ψ ⊤ MeasureTheory.volume + MeasureTheory.lpNorm (gradient ψ) 3 MeasureTheory.volume) * ‖z‖ * MeasureTheory.lpNorm (fderiv ℝ φ) 2 MeasureTheory.volume

The distributional cutoff-curl functional on an arbitrary genuine L² field. No derivative or divergence condition on z is required.