The variation measure of a function of locally finite variation #
Let Ω be an open set of a finite-dimensional real inner product space E and let u : E → ℝ
be locally integrable on Ω. The variational total variation |Du|(U) of u on open sets
U ⊆ Ω (TauCeti.totalVariationOn) is the restriction to open sets of a regular Borel measure
on Ω, the variation measure |Du| (TauCeti.variationMeasure), provided u has locally
finite variation on Ω: every compact K ⊆ Ω has an open neighbourhood U with
|Du|(U) < ∞. No global finiteness of the variation is needed, so this covers functions of
locally bounded variation on unbounded open sets, and perimeter measures of sets of locally
finite perimeter.
The construction is the De Giorgi–Letta criterion in the form of Mathlib's contents. As a
function of the open set, the total variation is countably subadditive
(TauCeti.totalVariationOn_iSup_le_tsum) and additive on disjoint open sets
(TauCeti.totalVariationOn_sup_of_disjoint). The set function
K ↦ inf { |Du|(U) | K ⊆ U ⊆ Ω open } on the compact subsets of Ω is therefore a content
(TauCeti.contentOfOpens), whose measure agrees with |Du| on open sets because a test vector
field is admissible on every open neighbourhood of its compact support. Uniqueness among outer
regular measures follows from MeasureTheory.Measure.OuterRegular.ext_isOpen.
Main declarations #
TauCeti.forall_isCompact_exists_totalVariationOn_ne_top_iff: along an exhaustion ofΩby relatively compact open sets, the variation is locally finite onΩexactly when it is finite on each of them.TauCeti.variationMeasure μ Ω u: the variation measure|Du|onΩ, a regular measure.TauCeti.variationMeasure_preimage_coe:|Du|(U) = totalVariationOn μ U ufor every openU ⊆ Ω, andTauCeti.variationMeasure_univ:|Du|(Ω) = totalVariationOn μ Ω u.TauCeti.forall_isCompact_exists_totalVariationOn_ne_top_of_tendsto_integral: distributional limits of locally BV functions with eventually bounded variation measures on compact subsets have locally finite variation.TauCeti.enorm_integral_divergenceCLM_mul_le_variationMeasure: a test vector field of norm at most one supported in an openU ⊆ Ωpairs withuto at most|Du|(U).TauCeti.eq_variationMeasure: an outer regular measure with these values on open sets is the variation measure.TauCeti.variationMeasure_eq_comap_inclusionandTauCeti.map_inclusion_variationMeasure: for openU ⊆ Ω, the variation measure onUis that onΩpulled back toU, and pushes forward to its restriction toU.TauCeti.variationMeasure_congr_ae: the variation measure only depends onualmost everywhere onΩ.TauCeti.variationMeasure_const_sub: against an additive Haar measure,c - uhas the same variation measure asu.
References #
- L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.1 (the structure theorem for functions of locally bounded variation).
- L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §1.5 (the De Giorgi–Letta criterion) and §3.1.
The variation content #
Local finiteness of the variation #
Along an exhaustion V of Ω by open sets with compact closures in Ω, a function has locally
finite variation on Ω exactly when it has finite variation on every V j.
The variation measure #
The variation measure |Du| of u on the open set Ω: if u is locally integrable on
Ω and has locally finite variation there, meaning that every compact K ⊆ Ω has an open
neighbourhood U with totalVariationOn μ U u < ∞, it is the regular measure on Ω whose value
on every open U ⊆ Ω is the total variation of u on U
(TauCeti.variationMeasure_preimage_coe). Otherwise it is 0 by convention.
Instances For
The variation measure is a regular measure.
The total variation is a measure. The variation measure of a function of locally finite
variation on Ω gives every open set U ⊆ Ω its total variation |Du|(U).
A distributional limit of locally BV functions whose variation measures are eventually bounded on every compact subset of the domain has locally finite variation.
A test vector field on Ω supported in an open set U with norm at most one pairs with
u to at most |Du|(U).
The total mass of the variation measure of a function of locally finite variation on Ω is
its total variation |Du|(Ω).
The variation measure is 0 for a function which is not locally integrable on Ω or does
not have locally finite variation there.
Uniqueness of the variation measure. An outer regular measure on Ω which gives every
open set U ⊆ Ω the total variation |Du|(U) is the variation measure.
Restriction to an open subset. For U ⊆ Ω open, the variation measure on U is the
pullback of the variation measure on Ω along the inclusion U → Ω.
For U ⊆ Ω open, the pushforward of the variation measure on U along the inclusion
U → Ω is the restriction of the variation measure on Ω to the trace of U.
The variation measure on Ω only depends on local integrability on Ω and on the total
variations on open subsets of Ω.
Locality. The variation measure on Ω only depends on u almost everywhere on Ω.
Against an additive Haar measure, c - u has the same variation measure as u. In
particular the indicators of a set and of its complement have the same variation measure.