Genuine all-order derivatives of the cutoff operators, with a fixed support-volume factor.

theorem EulerMeanBoundary.Cutoff.norm_iteratedFDeriv_directional (χ : Cutoff) (v x : EulerSmoothLimit.Space) (n : ℕ) : ‖iteratedFDeriv ℝ n (χ.directional v).field x‖ ≤ ‖v‖ * ‖iteratedFDeriv ℝ (n + 1) χ.field x‖

Differentiation of a smooth cutoff in one fixed direction has the expected tensor bound.

theorem EulerMeanBoundary.cutoffOperation_iteratedFDeriv_succ {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Cutoff → E) (hadd : ∀ (χ ψ : Cutoff), L (χ.add ψ) = L χ + L ψ) (hsmul : ∀ (χ : Cutoff) (c : ℝ), L (χ.scale c) = c • L χ) (hsub : ∀ (χ ψ : Cutoff), L (χ.sub ψ) = L χ - L ψ) (hbound : ∀ (χ : Cutoff), ‖L χ‖ ≤ cutoffBound χ) (χ : Cutoff) (a : EulerSmoothLimit.Space) (n : ℕ) (m : Fin (n + 1) → EulerSmoothLimit.Space) : (iteratedFDeriv ℝ (n + 1) (fun (b : EulerSmoothLimit.Space) => L (χ.translate b)) a) m = (iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => L ((χ.directional (m (Fin.last n))).translate b)) a) (Fin.init m)

Every actual higher derivative moves one direction onto the cutoff itself.

theorem EulerMeanBoundary.cutoffOperation_iteratedFDeriv_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Cutoff → E) (hadd : ∀ (χ ψ : Cutoff), L (χ.add ψ) = L χ + L ψ) (hsmul : ∀ (χ : Cutoff) (c : ℝ), L (χ.scale c) = c • L χ) (hsub : ∀ (χ ψ : Cutoff), L (χ.sub ψ) = L χ - L ψ) (hbound : ∀ (χ : Cutoff), ‖L χ‖ ≤ cutoffBound χ) (n : ℕ) (χ : Cutoff) (R M₀ M₁ : ℝ) (hM₀ : 0 ≤ M₀) (hM₁ : 0 ≤ M₁) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ M₀) (h₁ : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ (n + 1) χ.field x‖ ≤ M₁) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => L (χ.translate b)) a‖ ≤ 3 * EulerMeanCutoffCurl.cutoffCurlConstant * (M₀ + M₁ * (MeasureTheory.volume (Metric.closedBall 0 R)).toReal ^ (1 / 3))

Uniform pointwise bounds of orders n and n+1 control the actual operator-norm derivative. The support-volume factor is independent of n.

theorem EulerMeanBoundary.cutoffCurl_iteratedFDeriv_bound (n : ℕ) (χ : Cutoff) (R M₀ M₁ : ℝ) (hM₀ : 0 ≤ M₀) (hM₁ : 0 ≤ M₁) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ M₀) (h₁ : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ (n + 1) χ.field x‖ ≤ M₁) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => cutoffCurl (χ.translate b)) a‖ ≤ 3 * EulerMeanCutoffCurl.cutoffCurlConstant * (M₀ + M₁ * (MeasureTheory.volume (Metric.closedBall 0 R)).toReal ^ (1 / 3))

theorem EulerMeanBoundary.weakPotential_iteratedFDeriv_bound (n : ℕ) (χ : Cutoff) (R M₀ M₁ : ℝ) (hM₀ : 0 ≤ M₀) (hM₁ : 0 ≤ M₁) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (h₀ : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n χ.field x‖ ≤ M₀) (h₁ : ∀ (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ (n + 1) χ.field x‖ ≤ M₁) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => weakPotential (χ.translate b)) a‖ ≤ 3 * EulerMeanCutoffCurl.cutoffCurlConstant * (M₀ + M₁ * (MeasureTheory.volume (Metric.closedBall 0 R)).toReal ^ (1 / 3))