Smooth spatial cutoffs for whole-space comparison

The fixed bump is one on the unit ball and supported in the ball of radius two. All scaled cutoffs are obtained from this same bump by dilation. In particular, the constants in their derivative estimates do not depend on the radius.

noncomputable def NavierStokesR3.ComparisonCutoffs.baseBump : ContDiffBump 0

The fixed bump with inner radius one and outer radius two.

Equations

• NavierStokesR3.ComparisonCutoffs.baseBump = NavierStokesAndEuler.SmoothCutoff.baseBump NavierStokesR3.ProblemStatement.Space

noncomputable def NavierStokesR3.ComparisonCutoffs.baseCutoff (x : ProblemStatement.Space) : ℝ

The unscaled cutoff.

Equations

• NavierStokesR3.ComparisonCutoffs.baseCutoff x = NavierStokesAndEuler.SmoothCutoff.baseCutoff NavierStokesR3.ProblemStatement.Space x

noncomputable def NavierStokesR3.ComparisonCutoffs.cutoff (R : ℝ) (x : ProblemStatement.Space) : ℝ

The cutoff at spatial radius R; its estimates are stated for 0 < R.

Equations

• NavierStokesR3.ComparisonCutoffs.cutoff R x = NavierStokesAndEuler.SmoothCutoff.cutoff NavierStokesR3.ProblemStatement.Space R x

noncomputable def NavierStokesR3.ComparisonCutoffs.weight (R : ℝ) (x : ProblemStatement.Space) : ℝ

The weight in the localized energy.

Equations

• NavierStokesR3.ComparisonCutoffs.weight R x = NavierStokesR3.ComparisonCutoffs.cutoff R x ^ 8

noncomputable def NavierStokesR3.ComparisonCutoffs.multiplier (R : ℝ) (x : ProblemStatement.Space) : ℝ

The multiplier used to commute the pressure operator.

Equations

• NavierStokesR3.ComparisonCutoffs.multiplier R x = NavierStokesR3.ComparisonCutoffs.cutoff R x ^ 2

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_smooth : ContDiff ℝ (↑⊤) baseCutoff

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_nonneg (x : ProblemStatement.Space) : 0 ≤ baseCutoff x

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_le_one (x : ProblemStatement.Space) : baseCutoff x ≤ 1

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_eq_one {x : ProblemStatement.Space} (hx : ‖x‖ ≤ 1) : baseCutoff x = 1

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_eq_zero {x : ProblemStatement.Space} (hx : 2 ≤ ‖x‖) : baseCutoff x = 0

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_hasCompactSupport : HasCompactSupport baseCutoff

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_tsupport : tsupport baseCutoff = Metric.closedBall 0 2

theorem NavierStokesR3.ComparisonCutoffs.cutoff_smooth (R : ℝ) : ContDiff ℝ (↑⊤) (cutoff R)

theorem NavierStokesR3.ComparisonCutoffs.cutoff_nonneg (R : ℝ) (x : ProblemStatement.Space) : 0 ≤ cutoff R x

theorem NavierStokesR3.ComparisonCutoffs.cutoff_le_one (R : ℝ) (x : ProblemStatement.Space) : cutoff R x ≤ 1

theorem NavierStokesR3.ComparisonCutoffs.cutoff_mem_Icc (R : ℝ) (x : ProblemStatement.Space) : cutoff R x ∈ Set.Icc 0 1

theorem NavierStokesR3.ComparisonCutoffs.norm_scaled {R : ℝ} (hR : 0 < R) (x : ProblemStatement.Space) : ‖R⁻¹ • x‖ = ‖x‖ / R

theorem NavierStokesR3.ComparisonCutoffs.cutoff_eq_one {R : ℝ} (hR : 0 < R) {x : ProblemStatement.Space} (hx : ‖x‖ ≤ R) : cutoff R x = 1

theorem NavierStokesR3.ComparisonCutoffs.cutoff_eq_one_on_closedBall {R : ℝ} (hR : 0 < R) : Set.EqOn (cutoff R) (fun (x : ProblemStatement.Space) => 1) (Metric.closedBall 0 R)

theorem NavierStokesR3.ComparisonCutoffs.cutoff_eq_zero {R : ℝ} (hR : 0 < R) {x : ProblemStatement.Space} (hx : 2 * R ≤ ‖x‖) : cutoff R x = 0

theorem NavierStokesR3.ComparisonCutoffs.cutoff_support_subset {R : ℝ} (hR : 0 < R) : Function.support (cutoff R) ⊆ Metric.ball 0 (2 * R)

theorem NavierStokesR3.ComparisonCutoffs.cutoff_tsupport_subset {R : ℝ} (hR : 0 < R) : tsupport (cutoff R) ⊆ Metric.closedBall 0 (2 * R)

theorem NavierStokesR3.ComparisonCutoffs.cutoff_hasCompactSupport {R : ℝ} (hR : 0 < R) : HasCompactSupport (cutoff R)

theorem NavierStokesR3.ComparisonCutoffs.weight_smooth (R : ℝ) : ContDiff ℝ (↑⊤) (weight R)

theorem NavierStokesR3.ComparisonCutoffs.multiplier_smooth (R : ℝ) : ContDiff ℝ (↑⊤) (multiplier R)

theorem NavierStokesR3.ComparisonCutoffs.weight_nonneg (R : ℝ) (x : ProblemStatement.Space) : 0 ≤ weight R x

theorem NavierStokesR3.ComparisonCutoffs.weight_le_one (R : ℝ) (x : ProblemStatement.Space) : weight R x ≤ 1

theorem NavierStokesR3.ComparisonCutoffs.multiplier_nonneg (R : ℝ) (x : ProblemStatement.Space) : 0 ≤ multiplier R x

theorem NavierStokesR3.ComparisonCutoffs.multiplier_le_one (R : ℝ) (x : ProblemStatement.Space) : multiplier R x ≤ 1

theorem NavierStokesR3.ComparisonCutoffs.weight_hasCompactSupport {R : ℝ} (hR : 0 < R) : HasCompactSupport (weight R)

theorem NavierStokesR3.ComparisonCutoffs.multiplier_hasCompactSupport {R : ℝ} (hR : 0 < R) : HasCompactSupport (multiplier R)

theorem NavierStokesR3.ComparisonCutoffs.weight_eq_one {R : ℝ} (hR : 0 < R) {x : ProblemStatement.Space} (hx : ‖x‖ ≤ R) : weight R x = 1

theorem NavierStokesR3.ComparisonCutoffs.multiplier_eq_one {R : ℝ} (hR : 0 < R) {x : ProblemStatement.Space} (hx : ‖x‖ ≤ R) : multiplier R x = 1

theorem NavierStokesR3.ComparisonCutoffs.exists_derivative_bound (n : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ProblemStatement.Space), ‖iteratedFDeriv ℝ n baseCutoff x‖ ≤ C

noncomputable def NavierStokesR3.ComparisonCutoffs.derivativeConstant (n : ℕ) : ℝ

A fixed positive bound for the nth derivative of the unscaled bump.

Equations

• NavierStokesR3.ComparisonCutoffs.derivativeConstant n = NavierStokesAndEuler.SmoothCutoff.derivativeConstant NavierStokesR3.ProblemStatement.Space n

theorem NavierStokesR3.ComparisonCutoffs.derivativeConstant_pos (n : ℕ) : 0 < derivativeConstant n

theorem NavierStokesR3.ComparisonCutoffs.baseCutoff_iteratedFDeriv_le (n : ℕ) (x : ProblemStatement.Space) : ‖iteratedFDeriv ℝ n baseCutoff x‖ ≤ derivativeConstant n

theorem NavierStokesR3.ComparisonCutoffs.cutoff_iteratedFDeriv_le {R : ℝ} (hR : 0 < R) (n : ℕ) (x : ProblemStatement.Space) : ‖iteratedFDeriv ℝ n (cutoff R) x‖ ≤ derivativeConstant n / R ^ n

Each spatial derivative contributes precisely one inverse power of the radius.

theorem NavierStokesR3.ComparisonCutoffs.cutoff_fderiv_le {R : ℝ} (hR : 0 < R) (x : ProblemStatement.Space) : ‖fderiv ℝ (cutoff R) x‖ ≤ derivativeConstant 1 / R

theorem NavierStokesR3.ComparisonCutoffs.cutoff_second_fderiv_le {R : ℝ} (hR : 0 < R) (x : ProblemStatement.Space) : ‖fderiv ℝ (fderiv ℝ (cutoff R)) x‖ ≤ derivativeConstant 2 / R ^ 2

noncomputable def NavierStokesR3.ComparisonCutoffs.laplacian (f : ProblemStatement.Space → ℝ) (x : ProblemStatement.Space) : ℝ

The scalar spatial Laplacian, using the fixed standard coordinate vectors.

Equations

• NavierStokesR3.ComparisonCutoffs.laplacian f x = ∑ i : Fin 3, NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial i f) x

theorem NavierStokesR3.ComparisonCutoffs.fderiv_apply_derivative {f : ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x a b : ProblemStatement.Space) : (fderiv ℝ (fun (y : ProblemStatement.Space) => (fderiv ℝ f y) b) x) a = ((fderiv ℝ (fderiv ℝ f) x) a) b

theorem NavierStokesR3.ComparisonCutoffs.norm_partial_partial_le {f : ProblemStatement.Space → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (x : ProblemStatement.Space) : ‖NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial j f) x‖ ≤ ‖fderiv ℝ (fderiv ℝ f) x‖

theorem NavierStokesR3.ComparisonCutoffs.cutoff_partial_partial_le {R : ℝ} (hR : 0 < R) (i j : Fin 3) (x : ProblemStatement.Space) : ‖NavierStokes.SolutionDifference.spatialPartial i (NavierStokes.SolutionDifference.spatialPartial j (cutoff R)) x‖ ≤ derivativeConstant 2 / R ^ 2

theorem NavierStokesR3.ComparisonCutoffs.cutoff_laplacian_le {R : ℝ} (hR : 0 < R) (x : ProblemStatement.Space) : ‖laplacian (cutoff R) x‖ ≤ 3 * derivativeConstant 2 / R ^ 2

theorem NavierStokesR3.ComparisonCutoffs.compact_plateau {K : Set ProblemStatement.Space} (hK : IsCompact K) : ∃ R₀ > 0, ∀ R ≥ R₀, Set.EqOn (cutoff R) (fun (x : ProblemStatement.Space) => 1) K

Every fixed compact set lies in the plateau of all sufficiently large cutoffs.

theorem NavierStokesR3.ComparisonCutoffs.eventually_compact_plateau {K : Set ProblemStatement.Space} (hK : IsCompact K) : ∀ᶠ (R : ℝ) in Filter.atTop, Set.EqOn (cutoff R) (fun (x : ProblemStatement.Space) => 1) K

theorem NavierStokesR3.ComparisonCutoffs.eventually_cutoff_eq_one (x : ProblemStatement.Space) : ∀ᶠ (R : ℝ) in Filter.atTop, cutoff R x = 1

theorem NavierStokesR3.ComparisonCutoffs.cutoff_tendsto_one (x : ProblemStatement.Space) : Filter.Tendsto (fun (R : ℝ) => cutoff R x) Filter.atTop (nhds 1)