Constructed smooth cutoffs for the diagonal sum and time switch

The fixed cutoff is an actual Mathlib ContDiffBump, centered at zero, with inner radius 1/2 and outer radius 1. Smoothness below is C^∞, written ∞; no analyticity assertion is made. The scaled cutoff and time switch are explicit functions obtained from that bump. No convergence or PDE claim is encoded here.

noncomputable def NavierStokes.SmoothCutoffs.cutoffBump : ContDiffBump 0

Cutoff bump, bundling rIn, rOut, rIn_pos, rIn_lt_rOut.

Equations

• NavierStokes.SmoothCutoffs.cutoffBump = { rIn := 1 / 2, rOut := 1, rIn_pos := NavierStokes.SmoothCutoffs.cutoffBump._proof_1, rIn_lt_rOut := NavierStokes.SmoothCutoffs.cutoffBump._proof_2 }

noncomputable def NavierStokes.SmoothCutoffs.cutoff : ℝ → ℝ

Cutoff, given by cutoffBump.

Equations

• NavierStokes.SmoothCutoffs.cutoff = ↑NavierStokes.SmoothCutoffs.cutoffBump

theorem NavierStokes.SmoothCutoffs.cutoff_contDiff : ContDiff ℝ (↑⊤) cutoff

theorem NavierStokes.SmoothCutoffs.cutoff_mem_Icc (x : ℝ) : cutoff x ∈ Set.Icc 0 1

theorem NavierStokes.SmoothCutoffs.cutoff_one_of_abs_le {x : ℝ} (hx : |x| ≤ 1 / 2) : cutoff x = 1

theorem NavierStokes.SmoothCutoffs.cutoff_zero_of_one_le_abs {x : ℝ} (hx : 1 ≤ |x|) : cutoff x = 0

theorem NavierStokes.SmoothCutoffs.cutoff_zero_of_one_le {x : ℝ} (hx : 1 ≤ x) : cutoff x = 0

theorem NavierStokes.SmoothCutoffs.cutoff_support : Function.support cutoff = Set.Ioo (-1) 1

theorem NavierStokes.SmoothCutoffs.cutoff_tsupport : tsupport cutoff = Set.Icc (-1) 1

theorem NavierStokes.SmoothCutoffs.cutoff_hasCompactSupport : HasCompactSupport cutoff

theorem NavierStokes.SmoothCutoffs.cutoff_eventually_one {x : ℝ} (hx : |x| < 1 / 2) : cutoff =ᶠ[nhds x] fun (x : ℝ) => 1

theorem NavierStokes.SmoothCutoffs.cutoff_eventually_zero {x : ℝ} (hx : 1 < |x|) : cutoff =ᶠ[nhds x] fun (x : ℝ) => 0

theorem NavierStokes.SmoothCutoffs.cutoff_eventually_one_at_zero : cutoff =ᶠ[nhds 0] fun (x : ℝ) => 1

theorem NavierStokes.SmoothCutoffs.iteratedDeriv_const_succ (n : ℕ) (c : ℝ) : (iteratedDeriv (n + 1) fun (x : ℝ) => c) = fun (x : ℝ) => 0

theorem NavierStokes.SmoothCutoffs.cutoff_iteratedDeriv_zero_inside (n : ℕ) {x : ℝ} (hx : |x| < 1 / 2) : iteratedDeriv (n + 1) cutoff x = 0

theorem NavierStokes.SmoothCutoffs.cutoff_iteratedDeriv_zero_outside (n : ℕ) {x : ℝ} (hx : 1 < |x|) : iteratedDeriv (n + 1) cutoff x = 0

theorem NavierStokes.SmoothCutoffs.cutoff_iteratedDeriv_support (n : ℕ) : Function.support (iteratedDeriv (n + 1) cutoff) ⊆ {x : ℝ | 1 / 2 ≤ |x| ∧ |x| ≤ 1}

Every positive-order derivative is supported in a fixed collar away from zero.

theorem NavierStokes.SmoothCutoffs.cutoff_iteratedDeriv_tsupport (n : ℕ) : tsupport (iteratedDeriv (n + 1) cutoff) ⊆ {x : ℝ | 1 / 2 ≤ |x| ∧ |x| ≤ 1}

theorem NavierStokes.SmoothCutoffs.cutoff_iteratedDeriv_hasCompactSupport (n : ℕ) : HasCompactSupport (iteratedDeriv n cutoff)

theorem NavierStokes.SmoothCutoffs.cutoff_iteratedDeriv_bounded (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : ℝ), |iteratedDeriv n cutoff x| ≤ C

noncomputable def NavierStokes.SmoothCutoffs.scaledCutoff (a : ℝ) : ℝ → ℝ

Scaled cutoff, defined pointwise by cutoff (a * q).

Equations

• NavierStokes.SmoothCutoffs.scaledCutoff a q = NavierStokes.SmoothCutoffs.cutoff (a * q)

theorem NavierStokes.SmoothCutoffs.scaledCutoff_contDiff (a : ℝ) : ContDiff ℝ (↑⊤) (scaledCutoff a)

theorem NavierStokes.SmoothCutoffs.scaledCutoff_mem_Icc (a q : ℝ) : scaledCutoff a q ∈ Set.Icc 0 1

theorem NavierStokes.SmoothCutoffs.scaledCutoff_one_of_abs_le {a q : ℝ} (hq : |a * q| ≤ 1 / 2) : scaledCutoff a q = 1

theorem NavierStokes.SmoothCutoffs.scaledCutoff_zero_of_one_le_abs {a q : ℝ} (hq : 1 ≤ |a * q|) : scaledCutoff a q = 0

theorem NavierStokes.SmoothCutoffs.scaledCutoff_zero_of_inv_le {a q : ℝ} (ha : 0 < a) (hq : 1 / a ≤ q) : scaledCutoff a q = 0

theorem NavierStokes.SmoothCutoffs.scaledCutoff_hasCompactSupport {a : ℝ} (ha : a ≠ 0) : HasCompactSupport (scaledCutoff a)

theorem NavierStokes.SmoothCutoffs.scaledCutoff_eventually_one {a q : ℝ} (hq : |a * q| < 1 / 2) : scaledCutoff a =ᶠ[nhds q] fun (x : ℝ) => 1

theorem NavierStokes.SmoothCutoffs.scaledCutoff_eventually_zero {a q : ℝ} (hq : 1 < |a * q|) : scaledCutoff a =ᶠ[nhds q] fun (x : ℝ) => 0

theorem NavierStokes.SmoothCutoffs.scaledCutoff_eventually_one_at_zero (a : ℝ) : scaledCutoff a =ᶠ[nhds 0] fun (x : ℝ) => 1

theorem NavierStokes.SmoothCutoffs.finite_scaledCutoffs_eventually_one {ι : Type u_1} (s : Finset ι) (a : ι → ℝ) : ∀ᶠ (q : ℝ) in nhds 0, ∀ i ∈ s, scaledCutoff (a i) q = 1

Every finite list of stage cutoffs has a common plateau around zero.

theorem NavierStokes.SmoothCutoffs.scaledCutoffs_zero_on_common_neighborhood (a : ℕ → ℝ) (ha : Filter.Tendsto a Filter.atTop Filter.atTop) {q₀ : ℝ} (hq₀ : 0 < q₀) : ∃ (N : ℕ), ∀ n ≥ N, ∀ (q : ℝ), q₀ / 2 < q → scaledCutoff (a n) q = 0

If the scales diverge, a common neighborhood of each positive q₀ meets only finitely many stage cutoffs. The neighborhood is explicitly q > q₀/2.

theorem NavierStokes.SmoothCutoffs.scaledCutoff_iteratedDeriv (a : ℝ) (n : ℕ) : iteratedDeriv n (scaledCutoff a) = fun (q : ℝ) => a ^ n * iteratedDeriv n cutoff (a * q)

The exact all-order chain rule for the scale used in Sections 7 and 11.

theorem NavierStokes.SmoothCutoffs.scaledCutoff_iteratedDeriv_support (a : ℝ) (n : ℕ) : Function.support (iteratedDeriv (n + 1) (scaledCutoff a)) ⊆ {q : ℝ | 1 / 2 ≤ |a * q| ∧ |a * q| ≤ 1}

theorem NavierStokes.SmoothCutoffs.scale_power_bound {a q : ℝ} (ha : 0 ≤ a) (hq : 0 < q) (n b : ℕ) (hs : iteratedDeriv (n + 1) (scaledCutoff a) q ≠ 0) : a ^ b ≤ (1 / q) ^ b

Powers of the scale on derivative support are bounded by powers of q⁻¹.

theorem NavierStokes.SmoothCutoffs.scaledCutoff_iteratedDeriv_bound (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a q : ℝ), 0 ≤ a → 0 < q → |iteratedDeriv (n + 1) (scaledCutoff a) q| ≤ C * (1 / q) ^ (n + 1)

Uniform scale-independent derivative loss used by the diagonal cutoff argument.

noncomputable def NavierStokes.SmoothCutoffs.timeSwitch (t : ℝ) : ℝ

Zero near time zero, and one for every time at least 3/4.

Equations

• NavierStokes.SmoothCutoffs.timeSwitch t = 1 - NavierStokes.SmoothCutoffs.scaledCutoff (4 / 3) t

theorem NavierStokes.SmoothCutoffs.timeSwitch_contDiff : ContDiff ℝ (↑⊤) timeSwitch

theorem NavierStokes.SmoothCutoffs.timeSwitch_mem_Icc (t : ℝ) : timeSwitch t ∈ Set.Icc 0 1

theorem NavierStokes.SmoothCutoffs.timeSwitch_zero_of_abs_le {t : ℝ} (ht : |t| ≤ 3 / 8) : timeSwitch t = 0

theorem NavierStokes.SmoothCutoffs.timeSwitch_one_of_three_quarters_le {t : ℝ} (ht : 3 / 4 ≤ t) : timeSwitch t = 1

theorem NavierStokes.SmoothCutoffs.timeSwitch_eventually_zero : timeSwitch =ᶠ[nhds 0] fun (x : ℝ) => 0

theorem NavierStokes.SmoothCutoffs.timeSwitch_eventually_one {t : ℝ} (ht : 3 / 4 < t) : timeSwitch =ᶠ[nhds t] fun (x : ℝ) => 1

theorem NavierStokes.SmoothCutoffs.timeSwitch_iteratedDeriv_at_zero (n : ℕ) : iteratedDeriv (n + 1) timeSwitch 0 = 0

theorem NavierStokes.SmoothCutoffs.timeSwitch_iteratedDeriv_late (n : ℕ) {t : ℝ} (ht : 3 / 4 < t) : iteratedDeriv (n + 1) timeSwitch t = 0

theorem NavierStokes.SmoothCutoffs.timeSwitch_iteratedDeriv_formula (n : ℕ) (t : ℝ) : iteratedDeriv (n + 1) timeSwitch t = -((4 / 3) ^ (n + 1) * iteratedDeriv (n + 1) cutoff (4 / 3 * t))

theorem NavierStokes.SmoothCutoffs.timeSwitch_iteratedDeriv_support_nonneg (n : ℕ) {t : ℝ} (ht : 0 ≤ t) (hs : iteratedDeriv (n + 1) timeSwitch t ≠ 0) : 3 / 8 ≤ t ∧ t ≤ 3 / 4

On the physical half-line, all nonzero positive derivatives lie in [3/8,3/4].