Weighted Sobolev estimates for compact cutoffs

The derivative estimate is local: the unweighted velocity only needs to be in L². No integrability assumption is made on its unweighted derivative.

noncomputable def NavierStokesR3.WeightedSobolev.sobolevConstant : ℝ

The fixed whole-space H¹ → L⁶ Sobolev constant in dimension three.

Equations

• NavierStokesR3.WeightedSobolev.sobolevConstant = ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst MeasureTheory.volume 2)

theorem NavierStokesR3.WeightedSobolev.sobolevConstant_nonneg : 0 ≤ sobolevConstant

theorem NavierStokesR3.WeightedSobolev.memLp_of_compact {E : Type u_1} [NormedAddCommGroup E] {f : ProblemStatement.Space → E} (hf : Continuous f) (hs : HasCompactSupport f) (p : ENNReal) : MeasureTheory.MemLp f p MeasureTheory.volume

Compactly supported continuous functions have finite norms at every exponent, including infinity.

theorem NavierStokesR3.WeightedSobolev.lpNorm_six_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : ProblemStatement.Space → E} (hf : ContDiff ℝ 1 f) (hs : HasCompactSupport f) : Comparison.comparisonLpNorm 6 f ≤ sobolevConstant * Comparison.comparisonLpNorm 2 (fderiv ℝ f)

Mathlib's homogeneous Sobolev inequality specialized to Euclidean R³. The finite derivative norm is supplied by compact support and C¹ regularity.

theorem NavierStokesR3.WeightedSobolev.hasCompactSupport_cutoff_pow_smul {E : Type u_1} [Zero E] [SMulWithZero ℝ E] {φ : ProblemStatement.Space → ℝ} (hs : HasCompactSupport φ) (w : ProblemStatement.Space → E) {n : ℕ} (hn : n ≠ 0) : HasCompactSupport fun (x : ProblemStatement.Space) => φ x ^ n • w x

Multiplication by any positive natural power of a compact cutoff preserves compact support, even if the multiplied function is not compactly supported.

theorem NavierStokesR3.WeightedSobolev.memLp_cutoff_pow_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → E} (hφ : Continuous φ) (hs : HasCompactSupport φ) (hw : Continuous w) {n : ℕ} (hn : n ≠ 0) (p : ENNReal) : MeasureTheory.MemLp (fun (x : ProblemStatement.Space) => φ x ^ n • w x) p MeasureTheory.volume

All weighted velocity norms in the comparison argument are finite.

theorem NavierStokesR3.WeightedSobolev.fderiv_cutoff_four {φ : ProblemStatement.Space → ℝ} {x : ProblemStatement.Space} (hφ : DifferentiableAt ℝ φ x) : fderiv ℝ (fun (y : ProblemStatement.Space) => φ y ^ 4) x = (4 * φ x ^ 3) • fderiv ℝ φ x

Derivative of the fourth power of a scalar cutoff.

theorem NavierStokesR3.WeightedSobolev.norm_fderiv_cutoff_four_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} {x : ProblemStatement.Space} (hφ : DifferentiableAt ℝ φ x) (hw : DifferentiableAt ℝ w x) (hφ0 : 0 ≤ φ x) : ‖fderiv ℝ (fun (y : ProblemStatement.Space) => φ y ^ 4 • w y) x‖ ≤ φ x ^ 4 * ‖fderiv ℝ w x‖ + 4 * φ x ^ 3 * ‖fderiv ℝ φ x‖ * ‖w x‖

The pointwise product rule keeps the derivative of the velocity weighted.

noncomputable def NavierStokesR3.WeightedSobolev.cutoffGradientAmplitude (φ : ProblemStatement.Space → ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ℝ

The pointwise magnitude of the weighted coordinate gradient.

Equations

• NavierStokesR3.WeightedSobolev.cutoffGradientAmplitude φ w x = φ x ^ 4 * √(NavierStokesR3.Comparison.gradientSq w x)

theorem NavierStokesR3.WeightedSobolev.cutoffGradientAmplitude_nonneg (φ : ProblemStatement.Space → ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : 0 ≤ cutoffGradientAmplitude φ w x

theorem NavierStokesR3.WeightedSobolev.continuous_cutoffGradientAmplitude {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : Continuous φ) (hw : ContDiff ℝ 1 w) : Continuous (cutoffGradientAmplitude φ w)

theorem NavierStokesR3.WeightedSobolev.hasCompactSupport_cutoffGradientAmplitude {φ : ProblemStatement.Space → ℝ} (hs : HasCompactSupport φ) (w : ProblemStatement.Space → ProblemStatement.Space) : HasCompactSupport (cutoffGradientAmplitude φ w)

theorem NavierStokesR3.WeightedSobolev.memLp_cutoffGradientAmplitude {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : Continuous φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ 1 w) (p : ENNReal) : MeasureTheory.MemLp (cutoffGradientAmplitude φ w) p MeasureTheory.volume

theorem NavierStokesR3.WeightedSobolev.norm_cutoffGradientAmplitude_sq (φ : ProblemStatement.Space → ℝ) (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ‖cutoffGradientAmplitude φ w x‖ ^ 2 = φ x ^ 8 * Comparison.gradientSq w x

theorem NavierStokesR3.WeightedSobolev.integrable_weighted_gradientSq {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : Continuous φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ 1 w) : MeasureTheory.Integrable (fun (x : ProblemStatement.Space) => φ x ^ 8 * Comparison.gradientSq w x) MeasureTheory.volume

The weighted dissipation integral is finite solely from local regularity.

theorem NavierStokesR3.WeightedSobolev.lpNorm_cutoffGradientAmplitude {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : Continuous φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ 1 w) : Comparison.comparisonLpNorm 2 (cutoffGradientAmplitude φ w) = √(∫ (x : ProblemStatement.Space), φ x ^ 8 * Comparison.gradientSq w x)

theorem NavierStokesR3.WeightedSobolev.norm_fderiv_cutoff_four_le_amplitude {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} {x : ProblemStatement.Space} (hφ : DifferentiableAt ℝ φ x) (hw : DifferentiableAt ℝ w x) (hφ0 : 0 ≤ φ x) (hφ1 : φ x ≤ 1) {L : ℝ} (hL : ‖fderiv ℝ φ x‖ ≤ L) : ‖fderiv ℝ (fun (y : ProblemStatement.Space) => φ y ^ 4 • w y) x‖ ≤ 3 * cutoffGradientAmplitude φ w x + 4 * L * ‖w x‖

A pointwise majorant with no unweighted derivative term.

theorem NavierStokesR3.WeightedSobolev.lpNorm_fderiv_cutoff_four_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ 1 φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ 1 w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) {L : ℝ} (hL0 : 0 ≤ L) (hL : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ φ x‖ ≤ L) : Comparison.comparisonLpNorm 2 (fderiv ℝ fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ≤ 3 * √(∫ (x : ProblemStatement.Space), φ x ^ 8 * Comparison.gradientSq w x) + 4 * L * Comparison.comparisonLpNorm 2 w

The derivative of the cutoff velocity has a finite L² bound involving only weighted dissipation and the velocity's unweighted L² norm.

noncomputable def NavierStokesR3.WeightedSobolev.weightedSobolevConstant : ℝ

A positive, fixed constant for the cutoff Sobolev estimate.

Equations

• NavierStokesR3.WeightedSobolev.weightedSobolevConstant = 4 * NavierStokesR3.WeightedSobolev.sobolevConstant + 1

theorem NavierStokesR3.WeightedSobolev.weightedSobolevConstant_pos : 0 < weightedSobolevConstant

theorem NavierStokesR3.WeightedSobolev.weighted_sobolev {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.Space → ProblemStatement.Space} (hφ : ContDiff ℝ 1 φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ 1 w) (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) {L : ℝ} (hL0 : 0 ≤ L) (hL : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ φ x‖ ≤ L) : (Comparison.comparisonLpNorm 6 fun (x : ProblemStatement.Space) => φ x ^ 4 • w x) ≤ weightedSobolevConstant * (√(∫ (x : ProblemStatement.Space), φ x ^ 8 * Comparison.gradientSq w x) + L * Comparison.comparisonLpNorm 2 w)

The weighted Sobolev estimate B ≤ C (A + L M). All dependence on the cutoff is isolated in the derivative bound L; the constant is fixed.

theorem NavierStokesR3.WeightedSobolev.cutoffL6_le {φ : ProblemStatement.Space → ℝ} {w : ProblemStatement.VelocityField} {t : ℝ} (hφ : ContDiff ℝ 1 φ) (hs : HasCompactSupport φ) (hw : ContDiff ℝ 1 fun (x : NavierStokes.ProblemStatement.Space) => w (t, x)) (hw2 : MeasureTheory.MemLp (fun (x : NavierStokes.ProblemStatement.Space) => w (t, x)) 2 MeasureTheory.volume) (hφ0 : ∀ (x : ProblemStatement.Space), 0 ≤ φ x) (hφ1 : ∀ (x : ProblemStatement.Space), φ x ≤ 1) {L : ℝ} (hL0 : 0 ≤ L) (hL : ∀ (x : ProblemStatement.Space), ‖fderiv ℝ φ x‖ ≤ L) : Comparison.cutoffL6 φ w t ≤ weightedSobolevConstant * (Comparison.dissipationRoot φ w t + L * Comparison.comparisonLpNorm 2 fun (x : ProblemStatement.Space) => w (t, x))

Time-slice form using precisely the common comparison definitions.