Rigidity at an upper bound equal to the average

Proved

MeasureTheory.eqOn_of_le_setAverage

by Mazecto · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

maximum-principlemean-value-propertymeasure-theory

Let μ be a measure that assigns positive measure to every nonempty open set. Let s be an open set of finite measure and let f be a continuous, integrable real function on s. If f(x) is at most its normalized average over s for every x in s, then f is identically equal to that average on s. This includes the empty set. The conclusion follows because the nonnegative continuous deficit from the average has integral zero.

Preamble

import Mathlib.MeasureTheory.Integral.Average
import Mathlib.MeasureTheory.Measure.OpenPos

open MeasureTheory MeasureTheory.Measure Set
open scoped ENNReal
set_option autoImplicit false

Formal statement

theorem MeasureTheory.eqOn_of_le_setAverage {X : Type*} [TopologicalSpace X] [MeasurableSpace X]
    [OpensMeasurableSpace X] {μ : Measure X} [IsOpenPosMeasure μ]
    {s : Set X} {f : X → ℝ} (hs : IsOpen s) (hfinite : μ s ≠ ∞)
    (hc : ContinuousOn f s) (hi : IntegrableOn f s μ)
    (hle : ∀ x ∈ s, f x ≤ ⨍ y in s, f y ∂μ) :
    EqOn f (fun _ => ⨍ y in s, f y ∂μ) s  := by sorry

Source

Hunter, Notes on Partial Differential Equations, revised 6/18/2014, https://math.ucdavis.edu/~hunter/pdes/pde_notes.pdf, p. 26, proof of Theorem 2.13: equality in the mean-value bound forces constancy on a ball. This theorem isolates that measure-theoretic argument and generalizes it to finite-measure open sets and measures positive on nonempty open sets.

View graph