Genuine directional derivatives of the localized Newtonian operator family in operator norm.

@[instance_reducible]

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

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

Equations

• EulerMeanBoundary.instMeanBoundaryDerivative1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanBoundary.instMeanBoundaryDerivative2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanBoundary.instMeanBoundaryDerivative3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanBoundary.instMeanBoundaryDerivative4 = inferInstance

@[simp]

theorem EulerMeanBoundary.Cutoff.translate_zero (χ : Cutoff) : χ.translate 0 = χ

theorem EulerMeanBoundary.cutoffCurl_differenceError (χ : Cutoff) (a : EulerSmoothLimit.Space) (h : ℝ) : cutoffCurl (χ.differenceError a h) = h⁻¹ • (cutoffCurl (χ.translate (h • a)) - cutoffCurl χ) - cutoffCurl (χ.directional a)

theorem EulerMeanBoundary.Cutoff.exists_taylor_controls (χ : Cutoff) : ∃ (R : ℝ) (M₂ : ℝ) (M₃ : ℝ), 0 ≤ M₂ ∧ 0 ≤ M₃ ∧ tsupport χ.field ⊆ Metric.closedBall 0 R ∧ (∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ χ.field) x‖ ≤ M₂) ∧ ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ (fderiv ℝ χ.field)) x‖ ≤ M₃

theorem EulerMeanBoundary.cutoffCurl_hasDerivAt_zero (χ : Cutoff) (a : EulerSmoothLimit.Space) : HasDerivAt (fun (t : ℝ) => cutoffCurl (χ.translate (t • a))) (cutoffCurl (χ.directional a)) 0

Translating the actual cutoff differentiates the bounded cutoff-curl map in operator norm.

theorem EulerMeanBoundary.weakPotential_differenceError (χ : Cutoff) (a : EulerSmoothLimit.Space) (h : ℝ) : weakPotential (χ.differenceError a h) = h⁻¹ • (weakPotential (χ.translate (h • a)) - weakPotential χ) - weakPotential (χ.directional a)

theorem EulerMeanBoundary.weakPotential_operatorNorm_le (χ : Cutoff) : ‖weakPotential χ‖ ≤ cutoffBound χ

theorem EulerMeanBoundary.weakPotential_hasDerivAt_zero (χ : Cutoff) (a : EulerSmoothLimit.Space) : HasDerivAt (fun (t : ℝ) => weakPotential (χ.translate (t • a))) (weakPotential (χ.directional a)) 0

The represented weak potential differentiates with the same actual cutoff derivative.

theorem EulerMeanBoundary.mixedBoundaryOperator_hasDerivAt_zero (χ ψ : Cutoff) (a : EulerSmoothLimit.Space) : HasDerivAt (fun (t : ℝ) => mixedBoundaryOperator (χ.translate (t • a)) (ψ.translate (t • a))) (mixedBoundaryOperator (χ.directional a) ψ + mixedBoundaryOperator χ (ψ.directional a)) 0

Both cutoff positions contribute to the actual operator-norm derivative.

theorem EulerMeanBoundary.mixedBoundaryOperator_derivative_norm_le (χ ψ : Cutoff) (a : EulerSmoothLimit.Space) : ‖mixedBoundaryOperator (χ.directional a) ψ + mixedBoundaryOperator χ (ψ.directional a)‖ ≤ cutoffBound (χ.directional a) * cutoffBound ψ + cutoffBound χ * cutoffBound (ψ.directional a)

The corresponding differential commutator has the source's duality bound.