Full spatial-parameter smoothness of the actual localized Newtonian operators.

theorem EulerMeanBoundary.Cutoff.translate_add (χ : Cutoff) (a b : EulerSmoothLimit.Space) : (χ.translate a).translate b = χ.translate (a + b)

theorem EulerMeanBoundary.Cutoff.directional_translate (χ : Cutoff) (a b : EulerSmoothLimit.Space) : (χ.translate b).directional a = (χ.directional a).translate b

theorem EulerMeanBoundary.Cutoff.directional_add (χ : Cutoff) (a b : EulerSmoothLimit.Space) : χ.directional (a + b) = (χ.directional a).add (χ.directional b)

theorem EulerMeanBoundary.Cutoff.directional_smul (χ : Cutoff) (c : ℝ) (a : EulerSmoothLimit.Space) : χ.directional (c • a) = (χ.directional a).scale c

noncomputable def EulerMeanBoundary.cutoffDirectionalMap {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 χ) (χ : Cutoff) : EulerSmoothLimit.Space →L[ℝ] E

The derivative with respect to a translation parameter of an operation linear in the cutoff.

Equations

• EulerMeanBoundary.cutoffDirectionalMap L hadd hsmul χ = LinearMap.toContinuousLinearMap { toFun := fun (a : EulerSmoothLimit.Space) => L (χ.directional a), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem EulerMeanBoundary.cutoffDirectionalMap_apply {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 χ) (χ : Cutoff) (a : EulerSmoothLimit.Space) : (cutoffDirectionalMap L hadd hsmul χ) a = L (χ.directional a)

theorem EulerMeanBoundary.cutoffOperation_differenceError {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Cutoff → E) (hsmul : ∀ (χ : Cutoff) (c : ℝ), L (χ.scale c) = c • L χ) (hsub : ∀ (χ ψ : Cutoff), L (χ.sub ψ) = L χ - L ψ) (χ : Cutoff) (a b : EulerSmoothLimit.Space) : L ((χ.translate a).differenceError (b - a) 1) = L (χ.translate b) - L (χ.translate a) - L ((χ.translate a).directional (b - a))

theorem EulerMeanBoundary.cutoffOperation_hasFDerivAt {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) : HasFDerivAt (fun (b : EulerSmoothLimit.Space) => L (χ.translate b)) (cutoffDirectionalMap L hadd hsmul (χ.translate a)) a

The proved cutoff dual norm and a genuine Taylor remainder give the full Fréchet derivative.

theorem EulerMeanBoundary.cutoffOperation_contDiff {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) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => L (χ.translate a)

Induction differentiates the actual cutoff repeatedly, with no smoothness hypothesis on L.

theorem EulerMeanBoundary.cutoffCurl_hasFDerivAt (χ : Cutoff) (a : EulerSmoothLimit.Space) : HasFDerivAt (fun (b : EulerSmoothLimit.Space) => cutoffCurl (χ.translate b)) (cutoffDirectionalMap cutoffCurl cutoffCurl_add cutoffCurl_scale (χ.translate a)) a

Actual Fréchet derivative of the cutoff-curl extension.

theorem EulerMeanBoundary.weakPotential_hasFDerivAt (χ : Cutoff) (a : EulerSmoothLimit.Space) : HasFDerivAt (fun (b : EulerSmoothLimit.Space) => weakPotential (χ.translate b)) (cutoffDirectionalMap weakPotential weakPotential_add weakPotential_scale (χ.translate a)) a

Actual Fréchet derivative of the weak Newtonian potential.

theorem EulerMeanBoundary.cutoffCurl_contDiff (χ : Cutoff) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => cutoffCurl (χ.translate a)

theorem EulerMeanBoundary.weakPotential_contDiff (χ : Cutoff) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => weakPotential (χ.translate a)

theorem EulerMeanBoundary.mixedBoundaryOperator_contDiff (χ ψ : Cutoff) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => mixedBoundaryOperator (χ.translate a) (ψ.translate a)

Joint translation of both cutoffs is smooth in the full three-dimensional parameter.