Uniform bounds for actual cutoff difference quotients from classical derivative bounds.

Exact spatial difference-quotient commutators with the actual mixed boundary operator.

theorem EulerMeanBoundary.lpNorm_translated {E : Type u_1} [NormedAddCommGroup E] (f : EulerSmoothLimit.Space → E) (hf : Continuous f) (a : EulerSmoothLimit.Space) (p : ENNReal) : MeasureTheory.lpNorm (fun (x : EulerSmoothLimit.Space) => f (x + a)) p MeasureTheory.volume = MeasureTheory.lpNorm f p MeasureTheory.volume

theorem EulerMeanBoundary.cutoffBound_translate (χ : Cutoff) (a : EulerSmoothLimit.Space) : cutoffBound (χ.translate a) = cutoffBound χ

noncomputable def EulerMeanBoundary.spatialDifference (a : EulerSmoothLimit.Space) (h : ℝ) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

The genuine directional spatial difference quotient, defined also at h = 0.

Equations

• EulerMeanBoundary.spatialDifference a h = h⁻¹ • ((EulerMeanSolenoidal.translation (h • a)).toContinuousLinearMap - ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)

theorem EulerMeanBoundary.spatialDifference_apply (a : EulerSmoothLimit.Space) (h : ℝ) (z : ↥EulerMeanSolenoidal.L2) : (spatialDifference a h) z = h⁻¹ • ((EulerMeanSolenoidal.translation (h • a)) z - z)

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

Difference quotient, given by ((χ.translate (h • a)).sub χ).scale h⁻¹.

Equations

• χ.differenceQuotient a h = ((χ.translate (h • a)).sub χ).scale h⁻¹

theorem EulerMeanBoundary.Cutoff.differenceQuotient_field (χ : Cutoff) (a : EulerSmoothLimit.Space) (h : ℝ) (x : EulerSmoothLimit.Space) : (χ.differenceQuotient a h).field x = h⁻¹ * (χ.field (x + h • a) - χ.field x)

theorem EulerMeanBoundary.spatialDifference_commutator (a : EulerSmoothLimit.Space) (h : ℝ) (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : spatialDifference a h ∘SL A - A ∘SL spatialDifference a h = h⁻¹ • translationCommutator (h • a) A

theorem EulerMeanBoundary.mixedBoundaryOperator_differenceCommutator (a : EulerSmoothLimit.Space) (h : ℝ) (χ ψ : Cutoff) : spatialDifference a h ∘SL mixedBoundaryOperator χ ψ - mixedBoundaryOperator χ ψ ∘SL spatialDifference a h = (mixedBoundaryOperator (χ.differenceQuotient a h) (ψ.translate (h • a)) + mixedBoundaryOperator χ (ψ.differenceQuotient a h)) ∘SL (EulerMeanSolenoidal.translation (h • a)).toContinuousLinearMap

Exact two-position derivative splitting for an actual spatial difference quotient.

theorem EulerMeanBoundary.mixedBoundaryOperator_differenceCommutator_norm_le (a : EulerSmoothLimit.Space) (h : ℝ) (χ ψ : Cutoff) : ‖spatialDifference a h ∘SL mixedBoundaryOperator χ ψ - mixedBoundaryOperator χ ψ ∘SL spatialDifference a h‖ ≤ cutoffBound (χ.differenceQuotient a h) * cutoffBound (ψ.translate (h • a)) + cutoffBound χ * cutoffBound (ψ.differenceQuotient a h)

The commutator is bounded by the actual two cutoff difference quotients.

theorem EulerMeanBoundary.mixedBoundaryOperator_differenceCommutator_norm_le_invariant (a : EulerSmoothLimit.Space) (h : ℝ) (χ ψ : Cutoff) : ‖spatialDifference a h ∘SL mixedBoundaryOperator χ ψ - mixedBoundaryOperator χ ψ ∘SL spatialDifference a h‖ ≤ cutoffBound (χ.differenceQuotient a h) * cutoffBound ψ + cutoffBound χ * cutoffBound (ψ.differenceQuotient a h)

theorem EulerMeanBoundary.lpNorm_le_bound_volume {E : Type u_1} [NormedAddCommGroup E] (f : EulerSmoothLimit.Space → E) (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (K : Set EulerSmoothLimit.Space) (hK : MeasureTheory.volume K ≠ ⊤) (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C) (hzero : ∀ x ∉ K, f x = 0) (p : ENNReal) : MeasureTheory.lpNorm f p MeasureTheory.volume ≤ C * (MeasureTheory.volume K).toReal ^ (1 / p.toReal)

A support-volume bound, derived from the genuine Lp seminorm.

theorem EulerMeanBoundary.norm_differenceQuotient_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : EulerSmoothLimit.Space → E) (hf : Differentiable ℝ f) (M : ℝ) (hM : 0 ≤ M) (hDf : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ f x‖ ≤ M) (a : EulerSmoothLimit.Space) (h : ℝ) (x : EulerSmoothLimit.Space) : ‖h⁻¹ • (f (x + h • a) - f x)‖ ≤ M * ‖a‖

The classical mean value inequality bounds a directional difference quotient uniformly.

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

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

noncomputable def EulerMeanBoundary.cutoffDifferenceConstant (R M₁ M₂ : ℝ) : ℝ

Cutoff difference constant, given by 3 * cutoffCurlConstant * (M₁ + M₂ * (volume (Metric.closedBall (0 : Space) (R+1))).toReal ^ (1/3 : ℝ)).

Equations

• EulerMeanBoundary.cutoffDifferenceConstant R M₁ M₂ = 3 * EulerMeanCutoffCurl.cutoffCurlConstant * (M₁ + M₂ * (MeasureTheory.volume (Metric.closedBall 0 (R + 1))).toReal ^ (1 / 3))

theorem EulerMeanBoundary.cutoffBound_differenceQuotient (χ : Cutoff) (R M₁ M₂ : ℝ) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) (hsupport : tsupport χ.field ⊆ Metric.closedBall 0 R) (hD₁ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ χ.field x‖ ≤ M₁) (hD₂ : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (fderiv ℝ χ.field) x‖ ≤ M₂) (a : EulerSmoothLimit.Space) (h : ℝ) (hstep : ‖h • a‖ ≤ 1) : cutoffBound (χ.differenceQuotient a h) ≤ cutoffDifferenceConstant R M₁ M₂ * ‖a‖

A bound independent of the difference step; the only data are genuine derivative bounds.

theorem EulerMeanBoundary.cutoffDifferenceConstant_nonneg (R M₁ M₂ : ℝ) (hM₁ : 0 ≤ M₁) (hM₂ : 0 ≤ M₂) : 0 ≤ cutoffDifferenceConstant R M₁ M₂