Functions of bounded and of vanishing mean oscillation

Let μ be a measure on a pseudometric space X. The BMO seminorm of f : X → F is the supremum of its mean oscillations over all open balls,

‖f‖_{BMO} = sup_B ⨍_B ‖f - f_B‖, where f_B = ⨍_B f,

taken in ℝ≥0∞ (TauCeti.bmoSeminorm). A locally integrable f has bounded mean oscillation (TauCeti.MemBMO) when this is finite. The seminorm is the supremum of the sharp maximal function f^# (TauCeti.bmoSeminorm_eq_iSup_sharpMaximalFunction), it ignores constants, is subadditive and homogeneous, and vanishes exactly on the a.e. constant functions (TauCeti.bmoSeminorm_eq_zero_iff). Bounded functions have bounded mean oscillation, with ‖f‖_{BMO} ≤ 2 ‖f‖_∞ (TauCeti.bmoSeminorm_le_two_mul_eLpNorm_top). On a seminormed group with a right-invariant measure the seminorm is invariant under translation, and on a finite-dimensional real normed space with an additive Haar measure it is invariant under dilation (TauCeti.bmoSeminorm_comp_add_right, TauCeti.bmoSeminorm_comp_smul). The John–Nirenberg inequality for functions of bounded mean oscillation on ℝⁿ is in TauCeti.MeasureTheory.Integral.JohnNirenberg.

The VMO modulus of f is the supremum of its mean oscillations over the balls of radius at most r,

η_f(r) = sup_{B = B(c, s), s ≤ r} ⨍_B ‖f - f_B‖

(TauCeti.vmoModulus). It is monotone in r and its supremum over all r is ‖f‖_{BMO}. A function of bounded mean oscillation has vanishing mean oscillation (TauCeti.MemVMO) when η_f(r) → 0 as r → 0. On ℝⁿ with Lebesgue measure the ball of radius r has measure ωₙ rⁿ, so this agrees with Sarason's definition through the measure of the balls. The modulus is the quantity in which perturbation arguments for equations whose coefficients have vanishing mean oscillation are carried out: on balls of radius at most r such a coefficient is close in mean to a constant, with error η(r).

Functions of vanishing mean oscillation form a subspace of the functions of bounded mean oscillation that is closed for the BMO seminorm (TauCeti.memVMO_of_tendsto_bmoSeminorm) and contains every uniformly continuous function of bounded mean oscillation (UniformContinuous.memVMO), in particular every continuous function with compact support (Continuous.memVMO_of_hasCompactSupport). Hence the BMO-closure of the uniformly continuous functions of bounded mean oscillation consists of functions of vanishing mean oscillation, the easy half of Sarason's characterization.

Main declarations

• TauCeti.bmoSeminorm, TauCeti.MemBMO: the BMO seminorm and the space of functions of bounded mean oscillation.
• TauCeti.bmoSeminorm_eq_iSup_sharpMaximalFunction: the seminorm is the supremum of f^#.
• TauCeti.bmoSeminorm_le_two_mul_eLpNorm_top and MeasureTheory.MemLp.memBMO: L^∞ ⊆ BMO.
• TauCeti.bmoSeminorm_eq_zero_iff: the seminorm vanishes exactly on a.e. constant functions.
• TauCeti.bmoSeminorm_comp_add_right, TauCeti.bmoSeminorm_comp_smul: translation and dilation invariance, and TauCeti.vmoModulus_comp_add_right: translation invariance of the VMO modulus.
• TauCeti.vmoModulus, TauCeti.MemVMO: the VMO modulus and the space of functions of vanishing mean oscillation.
• TauCeti.memVMO_of_tendsto_bmoSeminorm: VMO is closed in BMO.
• UniformContinuous.memVMO, Continuous.memVMO_of_hasCompactSupport: uniformly continuous functions of bounded mean oscillation, and continuous functions with compact support, have vanishing mean oscillation.

References

• F. John and L. Nirenberg, On functions of bounded mean oscillation, Comm. Pure Appl. Math. 14 (1961), 415–426.
• D. Sarason, Functions of vanishing mean oscillation, Trans. Amer. Math. Soc. 207 (1975), 391–405.
• L. Grafakos, Modern Fourier Analysis, 3rd ed., Section 3.1.

The BMO seminorm

noncomputable def TauCeti.bmoSeminorm {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : ENNReal

The BMO seminorm of f with respect to μ: the supremum, over all open balls B, of the mean oscillation ⨍_B ‖f - f_B‖ₑ of f on B about its average f_B = ⨍_B f.

It takes values in ℝ≥0∞, so it is defined for every f; balls of radius r ≤ 0 are empty and contribute 0.

theorem TauCeti.setLAverage_enorm_sub_setAverage_le_bmoSeminorm {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) (c : X) (r : ℝ) : ⨍⁻ (y : X) in Metric.ball c r, ‖f y - ⨍ (z : X) in Metric.ball c r, f z ∂μ‖ₑ ∂μ ≤ bmoSeminorm f μ

The mean oscillation of f on any open ball is at most its BMO seminorm.

theorem TauCeti.bmoSeminorm_le_iff {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {a : ENNReal} : bmoSeminorm f μ ≤ a ↔ ∀ (c : X) (r : ℝ), ⨍⁻ (y : X) in Metric.ball c r, ‖f y - ⨍ (z : X) in Metric.ball c r, f z ∂μ‖ₑ ∂μ ≤ a

The BMO seminorm is at most a exactly when the mean oscillation of f on every open ball is.

theorem TauCeti.bmoSeminorm_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {a : ENNReal} (h : ∀ (c : X) (r : ℝ), ⨍⁻ (y : X) in Metric.ball c r, ‖f y - ⨍ (z : X) in Metric.ball c r, f z ∂μ‖ₑ ∂μ ≤ a) : bmoSeminorm f μ ≤ a

A bound on the mean oscillation of f on every open ball bounds its BMO seminorm.

theorem TauCeti.bmoSeminorm_eq_iSup_sharpMaximalFunction {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : bmoSeminorm f μ = ⨆ (x : X), sharpMaximalFunction μ f x

The BMO seminorm is the supremum of the sharp maximal function.

theorem TauCeti.sharpMaximalFunction_le_bmoSeminorm {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) (x : X) : sharpMaximalFunction μ f x ≤ bmoSeminorm f μ

The sharp maximal function is bounded by the BMO seminorm.

@[simp]

theorem TauCeti.bmoSeminorm_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} [CompleteSpace F] (b : F) : bmoSeminorm (fun (x : X) => b) μ = 0

The BMO seminorm of a constant with values in a Banach space vanishes.

@[simp]

theorem TauCeti.bmoSeminorm_zero {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} : bmoSeminorm 0 μ = 0

The BMO seminorm of the zero function vanishes.

theorem TauCeti.bmoSeminorm_congr_ae {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (h : f =ᵐ[μ] g) : bmoSeminorm f μ = bmoSeminorm g μ

The BMO seminorm depends only on the a.e. class of f.

@[simp]

theorem TauCeti.bmoSeminorm_add_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} [CompleteSpace F] (hf : MeasureTheory.AEStronglyMeasurable f μ) (b : F) : bmoSeminorm (fun (y : X) => f y + b) μ = bmoSeminorm f μ

Adding a constant to an a.e. strongly measurable f does not change its BMO seminorm.

@[simp]

theorem TauCeti.bmoSeminorm_const_smul {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : 𝕜) : bmoSeminorm (k • f) μ = ‖k‖ₑ * bmoSeminorm f μ

The BMO seminorm is homogeneous: ‖k • f‖_{BMO} = ‖k‖ₑ ‖f‖_{BMO}.

@[simp]

theorem TauCeti.bmoSeminorm_neg {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} : bmoSeminorm (-f) μ = bmoSeminorm f μ

The BMO seminorm of -f is that of f.

theorem TauCeti.bmoSeminorm_add_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : bmoSeminorm (f + g) μ ≤ bmoSeminorm f μ + bmoSeminorm g μ

The BMO seminorm is subadditive on a.e. strongly measurable functions.

theorem TauCeti.bmoSeminorm_sub_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) : bmoSeminorm (f - g) μ ≤ bmoSeminorm f μ + bmoSeminorm g μ

The BMO seminorm of a difference of a.e. strongly measurable functions is at most the sum of their BMO seminorms.

theorem TauCeti.bmoSeminorm_le_two_mul_eLpNorm_top {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : bmoSeminorm f μ ≤ 2 * MeasureTheory.eLpNorm f ⊤ μ

Bounded functions have bounded mean oscillation: ‖f‖_{BMO} ≤ 2 ‖f‖_∞.

Functions of bounded mean oscillation

def TauCeti.MemBMO {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : Prop

A function f has bounded mean oscillation with respect to μ if it is locally integrable and its BMO seminorm is finite.

theorem TauCeti.memBMO_iff {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} : MemBMO f μ ↔ MeasureTheory.LocallyIntegrable f μ ∧ bmoSeminorm f μ < ⊤

theorem TauCeti.MemBMO.locallyIntegrable {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemBMO f μ) : MeasureTheory.LocallyIntegrable f μ

theorem TauCeti.MemBMO.bmoSeminorm_lt_top {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemBMO f μ) : bmoSeminorm f μ < ⊤

theorem TauCeti.MemBMO.bmoSeminorm_ne_top {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemBMO f μ) : bmoSeminorm f μ ≠ ⊤

theorem TauCeti.MemBMO.congr_ae {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (hf : MemBMO f μ) (h : f =ᵐ[μ] g) : MemBMO g μ

theorem TauCeti.memBMO_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace F] (b : F) : MemBMO (fun (x : X) => b) μ

theorem TauCeti.memBMO_zero {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} : MemBMO 0 μ

theorem TauCeti.MemBMO.const_smul {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [SMulCommClass ℝ 𝕜 F] (hf : MemBMO f μ) (k : 𝕜) : MemBMO (k • f) μ

theorem TauCeti.MemBMO.neg {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemBMO f μ) : MemBMO (-f) μ

theorem TauCeti.MemBMO.add {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} [SecondCountableTopology X] (hf : MemBMO f μ) (hg : MemBMO g μ) : MemBMO (f + g) μ

theorem TauCeti.MemBMO.sub {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} [SecondCountableTopology X] (hf : MemBMO f μ) (hg : MemBMO g μ) : MemBMO (f - g) μ

theorem MeasureTheory.MemLp.memBMO {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : Measure X} {f : X → F} [IsLocallyFiniteMeasure μ] (hf : MemLp f ⊤ μ) : TauCeti.MemBMO f μ

Essentially bounded functions have bounded mean oscillation.

Functions with vanishing BMO seminorm

theorem TauCeti.bmoSeminorm_eq_zero_iff {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [CompleteSpace F] (hf : MeasureTheory.LocallyIntegrable f μ) : bmoSeminorm f μ = 0 ↔ ∃ (b : F), f =ᵐ[μ] fun (x : X) => b

On a proper space with a measure finite on compact sets, the BMO seminorm of a locally integrable function vanishes exactly when the function is a.e. constant.

The VMO modulus

noncomputable def TauCeti.vmoModulus {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) (r : ℝ) : ENNReal

The VMO modulus of f with respect to μ: the supremum of the mean oscillations of f over the open balls of radius at most r. It vanishes for r ≤ 0.

theorem TauCeti.setLAverage_enorm_sub_setAverage_le_vmoModulus {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {r : ℝ} (f : X → F) (μ : MeasureTheory.Measure X) (c : X) {s : ℝ} (hs : s ≤ r) : ⨍⁻ (y : X) in Metric.ball c s, ‖f y - ⨍ (z : X) in Metric.ball c s, f z ∂μ‖ₑ ∂μ ≤ vmoModulus f μ r

The mean oscillation of f on a ball of radius at most r is at most η_f(r).

theorem TauCeti.vmoModulus_le_iff {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {a : ENNReal} {r : ℝ} : vmoModulus f μ r ≤ a ↔ ∀ (c : X), ∀ s ≤ r, ⨍⁻ (y : X) in Metric.ball c s, ‖f y - ⨍ (z : X) in Metric.ball c s, f z ∂μ‖ₑ ∂μ ≤ a

η_f(r) ≤ a exactly when the mean oscillation of f on every ball of radius at most r is at most a.

theorem TauCeti.vmoModulus_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {a : ENNReal} {r : ℝ} (h : ∀ (c : X), ∀ s ≤ r, ⨍⁻ (y : X) in Metric.ball c s, ‖f y - ⨍ (z : X) in Metric.ball c s, f z ∂μ‖ₑ ∂μ ≤ a) : vmoModulus f μ r ≤ a

A bound on the mean oscillation of f on every ball of radius at most r bounds η_f(r).

theorem TauCeti.vmoModulus_of_nonpos {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {r : ℝ} (hr : r ≤ 0) : vmoModulus f μ r = 0

theorem TauCeti.monotone_vmoModulus {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : Monotone (vmoModulus f μ)

theorem TauCeti.vmoModulus_le_bmoSeminorm {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) (r : ℝ) : vmoModulus f μ r ≤ bmoSeminorm f μ

theorem TauCeti.iSup_vmoModulus {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : ⨆ (r : ℝ), vmoModulus f μ r = bmoSeminorm f μ

The BMO seminorm is the supremum of the VMO modulus over all radii.

theorem TauCeti.vmoModulus_congr_ae {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (h : f =ᵐ[μ] g) (r : ℝ) : vmoModulus f μ r = vmoModulus g μ r

@[simp]

theorem TauCeti.vmoModulus_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} [CompleteSpace F] (b : F) (r : ℝ) : vmoModulus (fun (x : X) => b) μ r = 0

@[simp]

theorem TauCeti.vmoModulus_zero {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} (r : ℝ) : vmoModulus 0 μ r = 0

@[simp]

theorem TauCeti.vmoModulus_add_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} [CompleteSpace F] (hf : MeasureTheory.AEStronglyMeasurable f μ) (b : F) (r : ℝ) : vmoModulus (fun (y : X) => f y + b) μ r = vmoModulus f μ r

Adding a constant to an a.e. strongly measurable f does not change its VMO modulus.

@[simp]

theorem TauCeti.vmoModulus_const_smul {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : 𝕜) (r : ℝ) : vmoModulus (k • f) μ r = ‖k‖ₑ * vmoModulus f μ r

The VMO modulus is homogeneous: η_{k • f} = ‖k‖ₑ η_f.

@[simp]

theorem TauCeti.vmoModulus_neg {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (r : ℝ) : vmoModulus (-f) μ r = vmoModulus f μ r

The VMO modulus of -f is that of f.

theorem TauCeti.vmoModulus_add_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (r : ℝ) : vmoModulus (f + g) μ r ≤ vmoModulus f μ r + vmoModulus g μ r

The VMO modulus is subadditive on a.e. strongly measurable functions.

theorem TauCeti.vmoModulus_sub_le {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (r : ℝ) : vmoModulus (f - g) μ r ≤ vmoModulus f μ r + vmoModulus g μ r

The VMO modulus of a difference of a.e. strongly measurable functions is at most the sum of their VMO moduli.

theorem TauCeti.vmoModulus_le_of_forall_dist_lt {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {r : ℝ} [OpensMeasurableSpace X] [CompleteSpace F] (hf : MeasureTheory.AEStronglyMeasurable f μ) {ε : ℝ} (hε : ∀ (x y : X), dist x y < 2 * r → ‖f x - f y‖ ≤ ε) : vmoModulus f μ r ≤ 2 * ENNReal.ofReal ε

If f varies by at most ε between points at distance less than 2 r, then its mean oscillation on every ball of radius at most r is at most 2 ε.

Functions of vanishing mean oscillation

def TauCeti.MemVMO {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : X → F) (μ : MeasureTheory.Measure X) : Prop

A function f has vanishing mean oscillation with respect to μ if it has bounded mean oscillation and its VMO modulus η_f(r) tends to 0 as r → 0.

theorem TauCeti.memVMO_iff_tendsto {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} : MemVMO f μ ↔ MemBMO f μ ∧ Filter.Tendsto (vmoModulus f μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

A function has vanishing mean oscillation exactly when it has bounded mean oscillation and its VMO modulus η_f(r) tends to 0 as r → 0.

theorem TauCeti.MemVMO.memBMO {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemVMO f μ) : MemBMO f μ

theorem TauCeti.MemVMO.tendsto_vmoModulus {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemVMO f μ) : Filter.Tendsto (vmoModulus f μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

theorem TauCeti.memVMO_iff {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} : MemVMO f μ ↔ MemBMO f μ ∧ ∀ ε > 0, ∃ δ > 0, vmoModulus f μ δ ≤ ε

A function of bounded mean oscillation has vanishing mean oscillation exactly when for every ε > 0 its mean oscillation on all sufficiently small balls is at most ε.

theorem TauCeti.MemVMO.congr_ae {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} (hf : MemVMO f μ) (h : f =ᵐ[μ] g) : MemVMO g μ

theorem TauCeti.memVMO_const {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace F] (b : F) : MemVMO (fun (x : X) => b) μ

theorem TauCeti.memVMO_zero {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} : MemVMO 0 μ

theorem TauCeti.MemVMO.const_smul {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [SMulCommClass ℝ 𝕜 F] (hf : MemVMO f μ) (k : 𝕜) : MemVMO (k • f) μ

theorem TauCeti.MemVMO.neg {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} (hf : MemVMO f μ) : MemVMO (-f) μ

theorem TauCeti.MemVMO.add {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} [SecondCountableTopology X] (hf : MemVMO f μ) (hg : MemVMO g μ) : MemVMO (f + g) μ

theorem TauCeti.MemVMO.sub {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f g : X → F} [SecondCountableTopology X] (hf : MemVMO f μ) (hg : MemVMO g μ) : MemVMO (f - g) μ

theorem TauCeti.memVMO_of_tendsto_bmoSeminorm {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} [SecondCountableTopology X] {ι : Type u_3} {l : Filter ι} [l.NeBot] {g : ι → X → F} (hf : MeasureTheory.LocallyIntegrable f μ) (hg : ∀ (i : ι), MemVMO (g i) μ) (h : Filter.Tendsto (fun (i : ι) => bmoSeminorm (f - g i) μ) l (nhds 0)) : MemVMO f μ

VMO is closed in BMO. A locally integrable function that is a limit, in the BMO seminorm, of functions of vanishing mean oscillation has vanishing mean oscillation.

theorem UniformContinuous.memVMO {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} [SecondCountableTopology X] [OpensMeasurableSpace X] [CompleteSpace F] (hf : UniformContinuous f) (hb : TauCeti.MemBMO f μ) : TauCeti.MemVMO f μ

Uniformly continuous functions of bounded mean oscillation have vanishing mean oscillation.

theorem Continuous.memVMO_of_hasCompactSupport {X : Type u_1} {F : Type u_2} [PseudoMetricSpace X] [MeasurableSpace X] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure X} {f : X → F} [SecondCountableTopology X] [OpensMeasurableSpace X] [MeasureTheory.IsLocallyFiniteMeasure μ] [CompleteSpace F] (hf : Continuous f) (hfc : HasCompactSupport f) : TauCeti.MemVMO f μ

Continuous functions with compact support have vanishing mean oscillation.

Translation and dilation invariance

@[simp]

theorem TauCeti.bmoSeminorm_comp_add_right {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [SeminormedAddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant] (f : G → F) (b : G) : bmoSeminorm (fun (x : G) => f (x + b)) μ = bmoSeminorm f μ

The BMO seminorm is invariant under translation for a right-invariant measure.

@[simp]

theorem TauCeti.vmoModulus_comp_add_right {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_4} [SeminormedAddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant] (f : G → F) (b : G) (r : ℝ) : vmoModulus (fun (x : G) => f (x + b)) μ r = vmoModulus f μ r

The VMO modulus is invariant under translation for a right-invariant measure.

@[simp]

theorem TauCeti.bmoSeminorm_comp_smul {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (f : E → F) {t : ℝ} (ht : t ≠ 0) : bmoSeminorm (fun (x : E) => f (t • x)) μ = bmoSeminorm f μ

The BMO seminorm is invariant under dilation x ↦ t • x, t ≠ 0, for an additive Haar measure on a finite-dimensional real normed space.