Documentation

TauCeti.MeasureTheory.Integral.Average

Norms of averages #

The extended norm of the average of a function is at most the average of its extended norm, and consequently the measure of a set times the norm of the average over it is at most the integral of the norm over it. These are the estimates used to bound a function that has been replaced by its averages on the pieces of a partition, as in the Calderón–Zygmund decomposition.

Both hold without any integrability or finiteness assumption: when the average is not defined it is 0 by convention.

Measuring the mean oscillation of a function about its own average rather than about a constant c costs at most a factor 2: ⨍_s ‖f - f_s‖ ≤ 2 ⨍_s ‖f - c‖. So a bound on the oscillation about any convenient constant gives one about the average, the form used by the John–Nirenberg inequality.

The average of a function over a set s is also controlled by its average over a larger set t ⊇ s, at the cost of the ratio μ t / μ s of their measures; together with the factor-2 bound above this compares mean oscillations on nested sets, as in the theory of functions of bounded mean oscillation. In square mean the comparison with a constant reads ∫_s ‖f - f_s‖² ≤ 4 ∫_s ‖f - c‖² on a set of finite measure; in an inner product space the factor 4 drops to 1, by the orthogonal splitting ∫_s ‖f - c‖² = ∫_s ‖f - f_s‖² + μ s ‖f_s - c‖². Consequently, on nested sets s ⊆ t, the square mean oscillation of f inherits any decay from t to s of the square mean oscillation of a comparison function H, up to the distance ∫_t ‖f - H‖²; this is the comparison step of Campanato's method. For a function with values in the Euclidean product ℝ × E, the same splitting in the first coordinate shows that among the constants (c, 0) the best one is the first coordinate of the average.

Averages are unchanged when the measure is multiplied by a positive finite scalar. They are also unchanged by a change of variables that rescales the measure by a constant factor, such as an affine homothety of a finite-dimensional space with its Haar measure: if a measurable equivalence e pushes μ forward to a • ν with 0 < a < ∞, then the average of f ∘ e over e ⁻¹' s with respect to μ is the average of f over s with respect to ν.

Along an increasing sequence of sets V n covering a set s of finite measure, the measures of the pieces s ∩ V n converge to that of s, and so do the averages of an integrable function, as used when an inequality proved on each set of an exhaustion is passed to the whole domain.

Since some point of a set lies at or above the average, a set of measure below δ / c, with c > 0, over which a real function has integral at least δ contains a point where the function exceeds c. No integrability assumption is needed, since otherwise the integral is 0.

Hölder's inequality also bounds the average by the Lᵖ seminorm on the set, with the normalizing factor μ s ^ (-1/p), and bounds its q-th power by (μ s)⁻¹ ∫⁻_s ‖f‖ₑ ^ q. These estimates hold for arbitrary sets, including zero or infinite measure, with only the exponent restrictions 1 ≤ p < ∞ or 1 ≤ q.

Main results #

source
theorem TauCeti.enorm_average_le_laverage {α : Type u_1} {E : Type u_2} {x✝ : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (f : α → E) :
‖⨍ (x : α), f x ∂μ‖ₑ ≤ ⨍⁻ (x : α), ‖f x‖ₑ ∂μ

The extended norm of an average is at most the average of the extended norm.

source
theorem TauCeti.enorm_setAverage_le_setLAverage {α : Type u_1} {E : Type u_2} {x✝ : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (f : α → E) (s : Set α) :
‖⨍ (x : α) in s, f x ∂μ‖ₑ ≤ ⨍⁻ (x : α) in s, ‖f x‖ₑ ∂μ

The extended norm of an average over a set is at most the average of the extended norm over the set.

source
theorem TauCeti.measure_mul_enorm_setAverage_le {α : Type u_1} {E : Type u_2} {x✝ : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (f : α → E) (s : Set α) :
μ s * ‖⨍ (x : α) in s, f x ∂μ‖ₑ ≤ ∫⁻ (x : α) in s, ‖f x‖ₑ ∂μ

The measure of a set times the extended norm of the average over it is at most the integral of the extended norm over it.

source
theorem TauCeti.setLAverage_enorm_eq_ofReal_setAverage_norm {α : Type u_1} {E : Type u_2} {x✝ : MeasurableSpace α} [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {s : Set α} {g : α → E} (hg : MeasureTheory.IntegrableOn g s μ) :
⨍⁻ (x : α) in s, ‖g x‖ₑ ∂μ = ENNReal.ofReal (⨍ (x : α) in s, ‖g x‖ ∂μ)

The mean of the extended norm of an integrable function over a set is the ENNReal.ofReal of the mean of its norm.

source
theorem TauCeti.enorm_setAverage_rpow_le {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {mu : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → F} {s : Set α} {q : ℝ} (hq : 1 ≤ q) :
‖⨍ (y : α) in s, f y ∂mu‖ₑ ^ q ≤ (mu s)⁻¹ * ∫⁻ (y : α) in s, ‖f y‖ₑ ^ q ∂mu

Hölder's bound on an average, in ∫⁻ form: the q-th power of the average of f over a set s is at most (μ s)⁻¹ times the integral of ‖f‖ ^ q over s. The single factor (μ s)⁻¹ is what survives after the q-th power of the normalization (μ s)⁻¹ cancels against the (μ s) ^ (q - 1) of Hölder's inequality. No measurability or integrability hypothesis is needed, since a function not integrable on s has average zero.

source
theorem TauCeti.enorm_setAverage_le {α : Type u_1} {F : Type u_2} [MeasurableSpace α] {mu : MeasureTheory.Measure α} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → F} {p : ENNReal} {s : Set α} (hp : 1 ≤ p) (hp' : p ≠ ⊤) :
‖⨍ (y : α) in s, f y ∂mu‖ₑ ≤ mu s ^ (-p.toReal⁻¹) * MeasureTheory.eLpNorm f p (mu.restrict s)

Hölder's bound on an average: the average of f over a set s is at most μ s ^ (-1/p) times the Lᵖ seminorm of f on s. At p = 1 this is the bound by the average of ‖f‖, and the volume factor sharpens as p grows because a larger exponent controls the mass of s more efficiently. No measurability or integrability hypothesis is needed, since a function not integrable on s has average zero.

source
theorem TauCeti.setLAverage_enorm_sub_setAverage_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s : Set X} (hf : MeasureTheory.IntegrableOn f s μ) (c : F) :
⨍⁻ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ₑ ∂μ ≤ 2 * ⨍⁻ (x : X) in s, ‖f x - c‖ₑ ∂μ

The mean oscillation of f on s about its own average is at most twice its mean oscillation about any constant c: ⨍_s ‖f - f_s‖ ≤ 2 ⨍_s ‖f - c‖.

source
theorem TauCeti.eLpNorm_sub_setAverage_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s : Set X} (hs : μ s ≠ ⊤) {p : ENNReal} (hp : 1 ≤ p) (hp' : p ≠ ⊤) (c : F) :
MeasureTheory.eLpNorm (fun (x : X) => f x - ⨍ (y : X) in s, f y ∂μ) p (μ.restrict s) ≤ 2 * MeasureTheory.eLpNorm (fun (x : X) => f x - c) p (μ.restrict s)

The Lᵖ deviation of f from its average over a set s of finite measure is at most twice its Lᵖ deviation from any constant c: ‖f - f_s‖_{Lᵖ(s)} ≤ 2 ‖f - c‖_{Lᵖ(s)} for 1 ≤ p < ∞.

source
theorem TauCeti.setLAverage_enorm_sub_const_eq_top {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] {f : X → F} {s : Set X} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (hs : μ s ≠ ⊤) (hfs : ¬MeasureTheory.IntegrableOn f s μ) (b : F) :
⨍⁻ (y : X) in s, ‖f y - b‖ₑ ∂μ = ⊤

On a set of finite measure, the average of ‖f - b‖ₑ is infinite for an f that is a.e. strongly measurable but not integrable there, whatever the constant b.

source
theorem TauCeti.setLAverage_enorm_add_const_sub {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s : Set X} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (b : F) :
⨍⁻ (y : X) in s, ‖f y + b - ⨍ (z : X) in s, f z + b ∂μ‖ₑ ∂μ = ⨍⁻ (y : X) in s, ‖f y - ⨍ (z : X) in s, f z ∂μ‖ₑ ∂μ

The mean oscillation of f + b on a set is that of f, for a constant b.

source
theorem TauCeti.setLAverage_enorm_add_sub_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : X → F} {s : Set X} {g : X → F} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (hg : MeasureTheory.AEStronglyMeasurable g (μ.restrict s)) :
⨍⁻ (y : X) in s, ‖f y + g y - ⨍ (z : X) in s, f z + g z ∂μ‖ₑ ∂μ ≤ ⨍⁻ (y : X) in s, ‖f y - ⨍ (z : X) in s, f z ∂μ‖ₑ ∂μ + ⨍⁻ (y : X) in s, ‖g y - ⨍ (z : X) in s, g z ∂μ‖ₑ ∂μ

The mean oscillation of f + g on a set is at most the sum of those of f and g.

source
theorem TauCeti.setLAverage_enorm_sub_setAverage_congr_ae {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {f g : X → F} (h : f =ᵐ[μ] g) (s : Set X) :
⨍⁻ (y : X) in s, ‖f y - ⨍ (z : X) in s, f z ∂μ‖ₑ ∂μ = ⨍⁻ (y : X) in s, ‖g y - ⨍ (z : X) in s, g z ∂μ‖ₑ ∂μ

The mean oscillation of f on a set depends only on the a.e. class of f.

source
theorem TauCeti.setLAverage_enorm_const_smul_sub_setAverage {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : X → F} {𝕜 : Type u_3} [NormedDivisionRing 𝕜] [Module 𝕜 F] [NormSMulClass 𝕜 F] [SMulCommClass ℝ 𝕜 F] (k : 𝕜) (s : Set X) :
⨍⁻ (y : X) in s, ‖k • f y - ⨍ (z : X) in s, k • f z ∂μ‖ₑ ∂μ = ‖k‖ₑ * ⨍⁻ (y : X) in s, ‖f y - ⨍ (z : X) in s, f z ∂μ‖ₑ ∂μ

The mean oscillation of k • f on a set is ‖k‖ₑ times that of f.

source
theorem TauCeti.ae_restrict_eq_setAverage_of_setLAverage_enorm_sub_setAverage_eq_zero {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : X → F} {s : Set X} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (hs : μ s ≠ ⊤) (h : ⨍⁻ (y : X) in s, ‖f y - ⨍ (z : X) in s, f z ∂μ‖ₑ ∂μ = 0) :
∀ᵐ (y : X) ∂μ.restrict s, f y = ⨍ (z : X) in s, f z ∂μ

On a set of finite measure, an a.e. strongly measurable f with zero mean oscillation agrees a.e. on the set with its average.

source
theorem TauCeti.sq_setAverage_norm_le_setAverage_norm_sq {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] {g : X → F} {s : Set X} (hs0 : μ s ≠ 0) (hs : μ s ≠ ⊤) (hg : MeasureTheory.IntegrableOn g s μ) (hg2 : MeasureTheory.IntegrableOn (fun (x : X) => ‖g x‖ ^ 2) s μ) :
(⨍ (x : X) in s, ‖g x‖ ∂μ) ^ 2 ≤ ⨍ (x : X) in s, ‖g x‖ ^ 2 ∂μ

Jensen's inequality for the square of a mean. On a set s of finite nonzero measure, the square of the mean of ‖g‖ is at most the mean of ‖g‖².

source
theorem TauCeti.laverage_const_mul {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {c : ENNReal} (hc : c ≠ ⊤) (f : X → ENNReal) :
⨍⁻ (x : X), c * f x ∂μ = c * ⨍⁻ (x : X), f x ∂μ

A finite constant factor comes out of the lower average, as it does out of the average (MeasureTheory.average_const_mul).

source
theorem TauCeti.laverage_rpow_enorm_rpow_inv_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {F : Type u_2} [NormedAddCommGroup F] {f : X → F} {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f μ) :
(⨍⁻ (x : X), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = MeasureTheory.eLpNorm f p μ / μ Set.univ ^ p.toReal⁻¹

For 0 < p < ∞, the p-th root of the lower average of ‖f‖ₑ ^ p is the Lᵖ seminorm of f divided by the p-th root of the total mass.

source
theorem TauCeti.setLAverage_enorm_sq_le_of_setIntegral_le {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {V : Type u_2} {W : Type u_3} {Y : Type u_4} [NormedAddCommGroup V] [NormedAddCommGroup W] [NormedAddCommGroup Y] {g : X → V} {f : X → W} {G : X → Y} {s t : Set X} {k : ENNReal} {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (hst : μ t = k * μ s) (ht : μ t ≠ ⊤) (hg : MeasureTheory.IntegrableOn (fun (x : X) => ‖g x‖ ^ 2) s μ) (hf : MeasureTheory.IntegrableOn (fun (x : X) => ‖f x‖ ^ 2) t μ) (hG : MeasureTheory.IntegrableOn (fun (x : X) => ‖G x‖ ^ 2) t μ) (h : ∫ (x : X) in s, ‖g x‖ ^ 2 ∂μ ≤ α * ∫ (x : X) in t, ‖f x‖ ^ 2 ∂μ + β * ∫ (x : X) in t, ‖G x‖ ^ 2 ∂μ) :
⨍⁻ (x : X) in s, ‖g x‖ₑ ^ 2 ∂μ ≤ k * (ENNReal.ofReal α * ⨍⁻ (x : X) in t, ‖f x‖ₑ ^ 2 ∂μ + ENNReal.ofReal β * ⨍⁻ (x : X) in t, ‖G x‖ₑ ^ 2 ∂μ)

An estimate ∫_s ‖g‖² ≤ α ∫_t ‖f‖² + β ∫_t ‖G‖² between Bochner integrals, read as one between averages in ℝ≥0∞, when the measure of t is finite and k times that of s.

source
theorem TauCeti.ofReal_div_sq_mul_setLAverage_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {S : Set X} (f : X → ENNReal) {lam : ℝ} (hlam : 0 < lam) (c : ℝ) :
ENNReal.ofReal (c / lam ^ 2) * ⨍⁻ (x : X) in S, f x ^ 2 ∂μ = ENNReal.ofReal c * ⨍⁻ (x : X) in S, (f x / ENNReal.ofReal lam) ^ 2 ∂μ

A factor 1 / λ² in front of the average of f² moves inside it as (f / λ)².

source
theorem TauCeti.rpow_laverage_le_laverage_rpow {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {u : X → ENNReal} (hu : AEMeasurable u μ) {r : ℝ} (hr : 1 ≤ r) :
(⨍⁻ (x : X), u x ∂μ) ^ r ≤ ⨍⁻ (x : X), u x ^ r ∂μ

Jensen's inequality for the average of a nonnegative function: for r ≥ 1, the r-th power of the average of u is at most the average of u ^ r. No finiteness is assumed: if the measure is zero or infinite, both averages vanish.

source
theorem TauCeti.setLAverage_le_div_mul_setLAverage_of_subset {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {s t : Set X} {g : X → ENNReal} (hst : s ⊆ t) (ht : μ t ≠ ⊤) :
⨍⁻ (x : X) in s, g x ∂μ ≤ μ t / μ s * ⨍⁻ (x : X) in t, g x ∂μ

The average of a nonnegative function over a subset s of t is at most μ t / μ s times its average over t.

source
theorem TauCeti.enorm_setAverage_sub_le_of_subset {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s t : Set X} (hst : s ⊆ t) (hs : μ s ≠ 0) (ht : μ t ≠ ⊤) (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (c : F) :
‖⨍ (x : X) in s, f x ∂μ - c‖ₑ ≤ μ t / μ s * ⨍⁻ (x : X) in t, ‖f x - c‖ₑ ∂μ

The average of f over a subset s of t differs from a constant c by at most μ t / μ s times the average of ‖f - c‖ₑ over t. This is the extended-norm form of TauCeti.norm_setAverage_sub_le_of_subset. No integrability is assumed: if f is not integrable on s, the right-hand side is infinite.

source
theorem TauCeti.enorm_setAverage_sub_le_setLAverage {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s : Set X} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) (hs : μ s ≠ 0) (hs' : μ s ≠ ⊤) (c : F) :
‖⨍ (x : X) in s, f x ∂μ - c‖ₑ ≤ ⨍⁻ (x : X) in s, ‖f x - c‖ₑ ∂μ

On a set of finite positive measure, the average of an almost everywhere strongly measurable f differs from a constant c by at most the average of ‖f - c‖ₑ. No integrability is assumed: if f is not integrable on s, the right-hand side is infinite.

source
theorem TauCeti.norm_setAverage_sub_le_of_subset {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s t : Set X} (hst : s ⊆ t) (hs : μ s ≠ 0) (ht : μ t ≠ ⊤) (hf : MeasureTheory.IntegrableOn f t μ) (c : F) :
‖⨍ (x : X) in s, f x ∂μ - c‖ ≤ μ.real t / μ.real s * ⨍ (x : X) in t, ‖f x - c‖ ∂μ

The average of f over a subset s of t differs from a constant c by at most μ t / μ s times the average of ‖f - c‖ over t.

source
theorem TauCeti.setLAverage_enorm_sub_setAverage_le_setLAverage_setLAverage {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s : Set X} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict s)) :
⨍⁻ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ₑ ∂μ ≤ ⨍⁻ (x : X) in s, ⨍⁻ (y : X) in s, ‖f x - f y‖ₑ ∂μ ∂μ

The mean oscillation of f on s is at most the average of ‖f x - f y‖ₑ over pairs of points of s. No integrability is assumed.

source
theorem TauCeti.setLAverage_setLAverage_enorm_sub_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : X → F} {s : Set X} :
⨍⁻ (x : X) in s, ⨍⁻ (y : X) in s, ‖f x - f y‖ₑ ∂μ ∂μ ≤ 2 * ⨍⁻ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ₑ ∂μ

The average of ‖f x - f y‖ₑ over pairs of points of s is at most twice the mean oscillation of f on s.

source
theorem TauCeti.setIntegral_norm_sub_setAverage_sq_le {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : X → F} {s : Set X} (hs : μ s ≠ ⊤) (hf : MeasureTheory.IntegrableOn f s μ) {c : F} (hfc : MeasureTheory.IntegrableOn (fun (x : X) => ‖f x - c‖ ^ 2) s μ) :
∫ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ ^ 2 ∂μ ≤ 4 * ∫ (x : X) in s, ‖f x - c‖ ^ 2 ∂μ

The square mean oscillation of f on a set s of finite measure about its own average is at most four times its square mean oscillation about any constant c: ∫_s ‖f - f_s‖² ≤ 4 ∫_s ‖f - c‖².

source
theorem TauCeti.setIntegral_norm_sub_sq_eq_setIntegral_norm_sub_setAverage_sq_add {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {s : Set X} {f : X → F} (hs : μ s ≠ ⊤) (hf : MeasureTheory.IntegrableOn f s μ) {c : F} (hfc : MeasureTheory.IntegrableOn (fun (x : X) => ‖f x - c‖ ^ 2) s μ) :
∫ (x : X) in s, ‖f x - c‖ ^ 2 ∂μ = ∫ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ ^ 2 ∂μ + μ.real s * ‖⨍ (y : X) in s, f y ∂μ - c‖ ^ 2

In a real inner product space, the square mean oscillation of f on a set s of finite measure about a constant c splits orthogonally: ∫_s ‖f - c‖² = ∫_s ‖f - f_s‖² + μ s ‖f_s - c‖².

source
theorem TauCeti.setIntegral_norm_sub_setAverage_sq_le_setIntegral_norm_sub_sq {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {s : Set X} {f : X → F} (hs : μ s ≠ ⊤) (hf : MeasureTheory.IntegrableOn f s μ) {c : F} (hfc : MeasureTheory.IntegrableOn (fun (x : X) => ‖f x - c‖ ^ 2) s μ) :
∫ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ ^ 2 ∂μ ≤ ∫ (x : X) in s, ‖f x - c‖ ^ 2 ∂μ

In a real inner product space, the average of f over a set s of finite measure minimizes the square mean oscillation: ∫_s ‖f - f_s‖² ≤ ∫_s ‖f - c‖² for every constant c.

source
theorem TauCeti.setIntegral_norm_sub_setAverage_sq_le_add_of_subset {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {s t : Set X} {f H : X → F} (hst : s ⊆ t) (ht : μ t ≠ ⊤) (hf : MeasureTheory.MemLp f 2 (μ.restrict t)) (hH : MeasureTheory.MemLp H 2 (μ.restrict t)) {K : ℝ} (hK : 0 ≤ K) (hdecay : ∫ (x : X) in s, ‖H x - ⨍ (y : X) in s, H y ∂μ‖ ^ 2 ∂μ ≤ K * ∫ (x : X) in t, ‖H x - ⨍ (y : X) in t, f y ∂μ‖ ^ 2 ∂μ) :
∫ (x : X) in s, ‖f x - ⨍ (y : X) in s, f y ∂μ‖ ^ 2 ∂μ ≤ 4 * K * ∫ (x : X) in t, ‖f x - ⨍ (y : X) in t, f y ∂μ‖ ^ 2 ∂μ + (4 * K + 2) * ∫ (x : X) in t, ‖f x - H x‖ ^ 2 ∂μ

Comparison of square mean oscillations on nested sets. Let s ⊆ t with μ t < ∞, let f and H be square integrable on t, and suppose the square mean oscillation of H decays from t to s with factor K ≥ 0, measured about the average of f on t: ∫_s ‖H - H_s‖² ≤ K ∫_t ‖H - f_t‖². Then the square mean oscillation of f decays with the same factor, up to the distance between f and H: ∫_s ‖f - f_s‖² ≤ 4K ∫_t ‖f - f_t‖² + (4K + 2) ∫_t ‖f - H‖².

source
theorem TauCeti.setIntegral_norm_sub_toLp_fst_setAverage_sq_le {X : Type u_1} {E : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {s : Set X} (hs : μ s ≠ ⊤) {f : X → WithLp 2 (ℝ × E)} (hf : MeasureTheory.MemLp f 2 (μ.restrict s)) (c : ℝ) :
∫ (x : X) in s, ‖f x - WithLp.toLp 2 ((⨍ (y : X) in s, f y ∂μ).fst, 0)‖ ^ 2 ∂μ ≤ ∫ (x : X) in s, ‖f x - WithLp.toLp 2 (c, 0)‖ ^ 2 ∂μ

The best normal constant. Among the vectors (c, 0) of the Euclidean product ℝ × E, the first coordinate ((f_s).fst, 0) of the average f_s of f over a set s of finite measure minimizes the square mean distance to f on s.

source
theorem TauCeti.setLIntegral_comp_preimage_of_map_eq_smul {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {e : X ≃ᵐ Y} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑e) μ = a • ν) (g : Y → ENNReal) (s : Set Y) :
∫⁻ (x : X) in ⇑e ⁻¹' s, g (e x) ∂μ = a * ∫⁻ (y : Y) in s, g y ∂ν

If a measurable equivalence e pushes μ forward to a • ν, then the lower integral of g ∘ e over e ⁻¹' s with respect to μ is a times the lower integral of g over s with respect to ν.

source
theorem TauCeti.setLAverage_comp_preimage_of_map_eq_smul {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {e : X ≃ᵐ Y} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑e) μ = a • ν) (ha : a ≠ 0) (ha' : a ≠ ⊤) (g : Y → ENNReal) (s : Set Y) :
⨍⁻ (x : X) in ⇑e ⁻¹' s, g (e x) ∂μ = ⨍⁻ (y : Y) in s, g y ∂ν

Averages of nonnegative functions are invariant under a measurable equivalence e that pushes μ forward to a positive finite multiple of ν.

source
theorem TauCeti.setIntegral_comp_preimage_of_map_eq_smul {X : Type u_1} {Y : Type u_2} {F : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [NormedAddCommGroup F] [NormedSpace ℝ F] {e : X ≃ᵐ Y} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑e) μ = a • ν) (f : Y → F) (s : Set Y) :
∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ = a.toReal • ∫ (y : Y) in s, f y ∂ν

If a measurable equivalence e pushes μ forward to a • ν, then the integral of f ∘ e over e ⁻¹' s with respect to μ is a.toReal times the integral of f over s with respect to ν.

source
theorem TauCeti.setAverage_comp_preimage_of_map_eq_smul {X : Type u_1} {Y : Type u_2} {F : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [NormedAddCommGroup F] [NormedSpace ℝ F] {e : X ≃ᵐ Y} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑e) μ = a • ν) (ha : a ≠ 0) (ha' : a ≠ ⊤) (f : Y → F) (s : Set Y) :
⨍ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ = ⨍ (y : Y) in s, f y ∂ν

Averages are invariant under a measurable equivalence e that pushes μ forward to a positive finite multiple of ν.

source
theorem TauCeti.setLAverage_enorm_sub_setAverage_comp_preimage_of_map_eq_smul {X : Type u_1} {Y : Type u_2} {F : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [NormedAddCommGroup F] [NormedSpace ℝ F] {e : X ≃ᵐ Y} {a : ENNReal} (he : MeasureTheory.Measure.map (⇑e) μ = a • ν) (ha : a ≠ 0) (ha' : a ≠ ⊤) (f : Y → F) (s : Set Y) :
⨍⁻ (x : X) in ⇑e ⁻¹' s, ‖f (e x) - ⨍ (z : X) in ⇑e ⁻¹' s, f (e z) ∂μ‖ₑ ∂μ = ⨍⁻ (y : Y) in s, ‖f y - ⨍ (z : Y) in s, f z ∂ν‖ₑ ∂ν

Mean oscillations are invariant under a measurable equivalence e that pushes μ forward to a positive finite multiple of ν: the mean oscillation of f ∘ e on e ⁻¹' s is that of f on s.

source
@[simp]
theorem TauCeti.laverage_smul_measure {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {a : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) (g : X → ENNReal) :
⨍⁻ (x : X), g x ∂a • μ = ⨍⁻ (x : X), g x ∂μ

The lower average is unchanged when the measure is multiplied by a positive finite scalar.

source
theorem TauCeti.setLAverage_smul_measure {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {a : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) (g : X → ENNReal) (s : Set X) :
⨍⁻ (x : X) in s, g x ∂a • μ = ⨍⁻ (x : X) in s, g x ∂μ

The lower average over a set is unchanged when the measure is multiplied by a positive finite scalar.

source
@[simp]
theorem TauCeti.average_smul_measure {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {a : ENNReal} [NormedAddCommGroup F] [NormedSpace ℝ F] (ha : a ≠ 0) (ha' : a ≠ ⊤) (f : X → F) :
⨍ (x : X), f x ∂a • μ = ⨍ (x : X), f x ∂μ

The average is unchanged when the measure is multiplied by a positive finite scalar.

source
theorem TauCeti.setAverage_smul_measure {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {a : ENNReal} [NormedAddCommGroup F] [NormedSpace ℝ F] (ha : a ≠ 0) (ha' : a ≠ ⊤) (f : X → F) (s : Set X) :
⨍ (x : X) in s, f x ∂a • μ = ⨍ (x : X) in s, f x ∂μ

The average over a set is unchanged when the measure is multiplied by a positive finite scalar.

source
theorem TauCeti.tendsto_measureReal_inter_of_monotone {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {s : Set X} {V : ℕ → Set X} (hV : Monotone V) (hsV : s ⊆ ⋃ (n : ℕ), V n) (hs : μ s ≠ ⊤) :
Filter.Tendsto (fun (n : ℕ) => μ.real (s ∩ V n)) Filter.atTop (nhds (μ.real s))

Along an increasing sequence of sets V n whose union contains s, the measures of the pieces s ∩ V n converge to the measure of s, if it is finite.

source
theorem TauCeti.tendsto_setAverage_inter_of_monotone {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : X → F} {s : Set X} {V : ℕ → Set X} (hV : Monotone V) (hsV : s ⊆ ⋃ (n : ℕ), V n) (hm : ∀ (n : ℕ), MeasureTheory.NullMeasurableSet (s ∩ V n) μ) (hs : μ s ≠ ⊤) (hf : MeasureTheory.IntegrableOn f s μ) :
Filter.Tendsto (fun (n : ℕ) => ⨍ (x : X) in s ∩ V n, f x ∂μ) Filter.atTop (nhds (⨍ (x : X) in s, f x ∂μ))

Along an increasing sequence of sets V n whose union contains s, the averages of a function integrable on s over the pieces s ∩ V n converge to its average over s, if s has finite measure.

source
theorem TauCeti.exists_lt_of_measure_lt_of_le_setIntegral {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} {f : α → ℝ} {S : Set α} {δ c : ℝ} (hc : 0 < c) (hS : ν S < ENNReal.ofReal (δ / c)) (hδS : δ ≤ ∫ (y : α) in S, f y ∂ν) :
∃ y ∈ S, c < f y

Large energy on a small set forces a large density. If a set S of measure less than δ / c, with c > 0, carries energy ∫_S f ≥ δ, then f exceeds c at some point of S. No integrability, measurability or sign condition on f is needed.

source
theorem TauCeti.integrable_and_average_rpow_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} {δ s : ℝ} (hs : 0 < s) (hδ : 0 ≤ δ) (hf : MeasureTheory.AEStronglyMeasurable f μ) (hf0 : ∀ᵐ (y : α) ∂μ, 0 ≤ f y) (hint' : MeasureTheory.Integrable (fun (y : α) => (f y + δ) ^ s) μ) :
MeasureTheory.Integrable (fun (y : α) => f y ^ s) μ ∧ ⨍ (y : α), f y ^ s ∂μ ≤ ⨍ (y : α), (f y + δ) ^ s ∂μ

If f ≥ 0 and (f + δ)^s is integrable, with δ ≥ 0 and s > 0, then so is f^s, and its average is at most that of (f + δ)^s.

source
theorem TauCeti.tendsto_average_add_rpow {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ} {p : ℝ} {δ : ℕ → ℝ} (hp : 0 < p) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ) (hf0 : ∀ᵐ (y : α) ∂μ, 0 ≤ f y) (hδ0 : ∀ (k : ℕ), 0 ≤ δ k) (hδ : Filter.Tendsto δ Filter.atTop (nhds 0)) :
Filter.Tendsto (fun (k : ℕ) => ⨍ (y : α), (f y + δ k) ^ p ∂μ) Filter.atTop (nhds (⨍ (y : α), f y ^ p ∂μ))

Dominated convergence for the averages of (f + δ k)^p, for f ≥ 0 in Lᵖ on a finite measure space, 0 < p and δ k ≥ 0 tending to 0: ⨍ (f + δ k)^p → ⨍ f^p.

source
theorem TauCeti.ae_eq_zero_of_setAverage_rpow_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {p : ℝ} {q : ENNReal} {g : α → ℝ} (hp : 0 < p) (hpq : ENNReal.ofReal p ≤ q) (hs0 : μ s ≠ 0) (hs : μ s ≠ ⊤) (hg : MeasureTheory.MemLp g q (μ.restrict s)) (hg0 : ∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x) (havg : ⨍ (x : α) in s, g x ^ p ∂μ = 0) :
∀ᵐ (x : α) ∂μ.restrict s, g x = 0

If a nonnegative function in Lᵠ of a set of finite positive measure has vanishing average of its p-th power, for 0 < p ≤ q, then it vanishes almost everywhere on the set.

source
theorem TauCeti.average_rpow_le_average_add_const_rpow {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure m] {f : α → ℝ} {p δ : ℝ} (hp : 0 < p) (hδ : 0 ≤ δ) (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) m) (hf0 : ∀ᵐ (y : α) ∂m, 0 ≤ f y) :
⨍ (y : α), f y ^ p ∂m ≤ ⨍ (y : α), (f y + δ) ^ p ∂m

For f ≥ 0 in Lᵖ on a finite measure space and p > 0, the average of f ^ p is at most that of (f + δ) ^ p for δ ≥ 0.

source
theorem ContinuousLinearMap.average_apply {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] {H : X → E →L[𝕜] F} (hH : MeasureTheory.Integrable H μ) (v : E) :
(⨍ (y : X), H y ∂μ) v = ⨍ (y : X), (H y) v ∂μ

Applying an average of continuous linear maps to a vector is the average of the applications.

source
theorem TauCeti.setAverage_mul_setAverage_le_of_setLIntegral_mul_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {B : Set α} {f₁ f₂ : α → ℝ} {C : NNReal} (h₁ : ∀ᵐ (x : α) ∂μ.restrict B, 0 ≤ f₁ x) (h₂ : ∀ᵐ (x : α) ∂μ.restrict B, 0 ≤ f₂ x) (h : (∫⁻ (x : α) in B, ENNReal.ofReal (f₁ x) ∂μ) * ∫⁻ (x : α) in B, ENNReal.ofReal (f₂ x) ∂μ ≤ ↑C * μ B ^ 2) :
(⨍ (x : α) in B, f₁ x ∂μ) * ⨍ (x : α) in B, f₂ x ∂μ ≤ ↑C

If two almost everywhere nonnegative functions on B have a product of integrals at most C μ(B)², then the product of their averages over B is at most C. A function which is not almost everywhere strongly measurable on B has average zero.

source
theorem TauCeti.setLIntegral_enorm_sub_setAverage_le_add_of_integrableOn {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] {u : X → F} {U T A : Set X} (huU : MeasureTheory.IntegrableOn u U μ) {v : X → F} (hvU : MeasureTheory.IntegrableOn v U μ) (hT : T ⊆ U) (hA : A ⊆ U) :
∫⁻ (x : X) in A, ‖u x - ⨍ (y : X) in T, u y ∂μ‖ₑ ∂μ ≤ ∫⁻ (x : X) in U, ‖v x - u x‖ₑ ∂μ + μ U / μ T * ∫⁻ (x : X) in U, ‖v x - u x‖ₑ ∂μ + ∫⁻ (x : X) in A, ‖v x - ⨍ (y : X) in T, v y ∂μ‖ₑ ∂μ

The deviation of u from its mean over T on A ⊆ U is at most that of an approximation v, plus (1 + μ(U) / μ(T)) times the L¹(U) distance from v to u, for u and v integrable on U.

source
theorem TauCeti.enorm_sub_setAverage_eq_zero_of_subsingleton {X : Type u_1} {F : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {u : X → F} {S : Set X} [Subsingleton X] (x : X) (hS₀ : μ S ≠ 0) (hS_top : μ S ≠ ⊤) :
‖u x - ⨍ (y : X) in S, u y ∂μ‖ₑ = 0

On a subsingleton domain a function is constant, so its deviation from its mean over any set S of finite positive measure vanishes.