Uniform Taylor remainders for the actual smooth compact cutoffs.

@[instance_reducible]

noncomputable def EulerMeanBoundary.instMeanCutoffTaylor1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] ℝ)

Cache the standard NormedAddCommGroup (Space →L[ℝ] ℝ) instance to shorten typeclass synthesis.

Equations

• EulerMeanBoundary.instMeanCutoffTaylor1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanBoundary.instMeanCutoffTaylor2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] ℝ)

Cache the standard NormedSpace ℝ (Space →L[ℝ] ℝ) instance to shorten typeclass synthesis.

Equations

• EulerMeanBoundary.instMeanCutoffTaylor2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanBoundary.instMeanCutoffTaylor3 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] ℝ)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space →L[ℝ] ℝ) instance to shorten typeclass synthesis.

Equations

• EulerMeanBoundary.instMeanCutoffTaylor3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanBoundary.instMeanCutoffTaylor4 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] ℝ)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space →L[ℝ] ℝ) instance to shorten typeclass synthesis.

Equations

• EulerMeanBoundary.instMeanCutoffTaylor4 = inferInstance

theorem EulerMeanBoundary.norm_linearization_remainder_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : EulerSmoothLimit.Space → E) (hf : ContDiff ℝ (↑⊤) f) (M : ℝ) (hM : 0 ≤ M) (hD₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ M) (x v : EulerSmoothLimit.Space) : ‖f (x + v) - f x - (fderiv ℝ f x) v‖ ≤ M * ‖v‖ ^ 2

A global second derivative bound gives the quadratic Taylor remainder directly by mean value.

theorem EulerMeanBoundary.norm_differenceQuotient_remainder_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : EulerSmoothLimit.Space → E) (hf : ContDiff ℝ (↑⊤) f) (M : ℝ) (hM : 0 ≤ M) (hD₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ M) (a : EulerSmoothLimit.Space) (h : ℝ) (hh : h ≠ 0) (x : EulerSmoothLimit.Space) : ‖h⁻¹ • (f (x + h • a) - f x) - (fderiv ℝ f x) a‖ ≤ M * |h| * ‖a‖ ^ 2

Difference quotients converge with a quantitative first-order error.

noncomputable def EulerMeanBoundary.Cutoff.directional (χ : Cutoff) (a : EulerSmoothLimit.Space) : Cutoff

Directional, given by ⟨fun x => fderiv ℝ χ.field x a, (χ.smooth.fderiv_right (m := ∞) (by simp)).clm_apply contDiff_const, χ.compact.fderiv_apply ℝ a⟩.

Equations

• χ.directional a = { field := fun (x : EulerSmoothLimit.Space) => (fderiv ℝ χ.field x) a, smooth := ⋯, compact := ⋯ }

theorem EulerMeanBoundary.Cutoff.directional_fderiv (χ : Cutoff) (a x : EulerSmoothLimit.Space) : fderiv ℝ (χ.directional a).field x = (fderiv ℝ (fderiv ℝ χ.field) x) a

theorem EulerMeanBoundary.Cutoff.directional_support (χ : Cutoff) (a : EulerSmoothLimit.Space) : tsupport (χ.directional a).field ⊆ tsupport χ.field

theorem EulerMeanBoundary.Cutoff.sub_support (χ ψ : Cutoff) (K : Set EulerSmoothLimit.Space) (hK : IsClosed K) (hχ : tsupport χ.field ⊆ K) (hψ : tsupport ψ.field ⊆ K) : tsupport (χ.sub ψ).field ⊆ K

theorem EulerMeanBoundary.cutoffBound_le_of_support (χ : Cutoff) (R M₀ M₁ : ℝ) (hM₀ : 0 ≤ M₀) (hM₁ : 0 ≤ M₁) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (hb : ∀ (x : EulerSmoothLimit.Space), ‖χ.field x‖ ≤ M₀) (hdb : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ χ.field x‖ ≤ M₁) : cutoffBound χ ≤ 3 * EulerMeanCutoffCurl.cutoffCurlConstant * (M₀ + M₁ * (MeasureTheory.volume (Metric.closedBall 0 R)).toReal ^ (1 / 3))

A compactly supported cutoff is bounded in the exact duality norm by pointwise data.

noncomputable def EulerMeanBoundary.Cutoff.differenceError (χ : Cutoff) (a : EulerSmoothLimit.Space) (h : ℝ) : Cutoff

Difference error, given by (χ.differenceQuotient a h).sub (χ.directional a).

Equations

• χ.differenceError a h = (χ.differenceQuotient a h).sub (χ.directional a)

theorem EulerMeanBoundary.Cutoff.differenceError_support (χ : Cutoff) (R : ℝ) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (a : EulerSmoothLimit.Space) (h : ℝ) (hstep : ‖h • a‖ ≤ 1) : tsupport (χ.differenceError a h).field ⊆ Metric.closedBall 0 (R + 1)

theorem EulerMeanBoundary.Cutoff.differenceError_fderiv (χ : Cutoff) (a : EulerSmoothLimit.Space) (h : ℝ) (x : EulerSmoothLimit.Space) : fderiv ℝ (χ.differenceError a h).field x = h⁻¹ • (fderiv ℝ χ.field (x + h • a) - fderiv ℝ χ.field x) - (fderiv ℝ (fderiv ℝ χ.field) x) a

theorem EulerMeanBoundary.cutoffBound_differenceError (χ : Cutoff) (R M₂ M₃ : ℝ) (hM₂ : 0 ≤ M₂) (hM₃ : 0 ≤ M₃) (hs : tsupport χ.field ⊆ Metric.closedBall 0 R) (hD₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ χ.field) x‖ ≤ M₂) (hD₃ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ (fderiv ℝ χ.field)) x‖ ≤ M₃) (a : EulerSmoothLimit.Space) (h : ℝ) (hh : h ≠ 0) (hstep : ‖h • a‖ ≤ 1) : cutoffBound (χ.differenceError a h) ≤ cutoffDifferenceConstant R M₂ M₃ * |h| * ‖a‖ ^ 2

The cutoff difference quotient converges in precisely the norm controlling the boundary operator.