The total variation of a function on an open set #
Let Ω be an open set of a finite-dimensional real inner product space E. The
total variation of a function u : E → ℝ on Ω is the extended supremum
|Du|(Ω) = ⨆ { ∫ u div φ | φ ∈ 𝓓(Ω, E), ‖φ x‖ ≤ 1 for all x }
over smooth vector fields compactly supported in Ω with pointwise norm at most one
(TauCeti.totalVariationOn). The functions of bounded variation on Ω are the
u ∈ L¹(Ω) for which it is finite, and the perimeter of a set is the total variation of its
indicator. When the distributional derivative Du is a vector-valued Radon measure, this
supremum is the total variation measure |Du| evaluated on Ω; that comparison is not proved
here. The definition by duality is meaningful for every locally integrable function, with no
differentiability assumption, which is what lower semicontinuity and compactness arguments need.
The measure μ is a parameter, as in TauCeti.HasWeakFDerivOn. The pairing ∫ u div φ ∂μ is
the distributional pairing for an additive Haar measure μ, and that hypothesis is carried by
the results that need it: a constant function has total variation zero only against a
translation-invariant measure.
For u not locally integrable on Ω the integrals in the supremum may be Mathlib's junk value
0 for non-integrable functions, so the results that split integrals assume local integrability.
Main declarations #
TauCeti.totalVariationOn μ Ω u: the total variation ofuonΩ.TauCeti.ofReal_abs_integral_le_totalVariationOn: every admissible pairing is bounded by the total variation, andTauCeti.totalVariationOn_le_iffcharacterises upper bounds.TauCeti.ofReal_abs_integral_le_ofReal_mul_totalVariationOn: a test vector field bounded bycpairs to at mostc |Du|(Ω).TauCeti.totalVariationOn_congr_ae: the total variation only seesualmost everywhere onΩ.TauCeti.totalVariationOn_monoandTauCeti.totalVariationOn_iSup: monotonicity and inner continuity in the open set.TauCeti.totalVariationOn_iSup_le_tsum,TauCeti.totalVariationOn_sup_leandTauCeti.totalVariationOn_sup_of_disjoint: countable subadditivity in the open set, by a smooth partition of unity, and additivity on disjoint open sets. These make the total variation the restriction to open sets of a measure (TauCeti.variationMeasure).TauCeti.totalVariationOn_neg,TauCeti.totalVariationOn_smulandTauCeti.totalVariationOn_add_le: the total variation is a seminorm.TauCeti.totalVariationOn_add_constandTauCeti.totalVariationOn_const: against an additive Haar measure, constants have no variation.TauCeti.totalVariationOn_le_liminf_of_tendsto_integralandTauCeti.totalVariationOn_le_liminf: lower semicontinuity under distributional convergence and under convergence inL¹_loc(Ω).TauCeti.tendsto_totalVariationOn_of_le_add: variations converge along anL¹_loc(Ω)approximation whose variations exceed the limit's by amounts tending to zero.TauCeti.totalVariationOn_le_of_tendsto_L1: a total-variation bound holding frequently along a filter is preserved under convergence inL¹(Ω)along it.TauCeti.HasWeakFDerivOn.totalVariationOn_le_setLIntegral_enorm: a weakly differentiable function has total variation at most the integral of the norm of its weak derivative, hence locally finite variation (TauCeti.HasWeakFDerivOn.exists_totalVariationOn_ne_top).TauCeti.HasWeakFDerivOn.totalVariationOn_eq_setLIntegral_enorm: against an additive Haar measure this is an equality, so aW^{1,1}(Ω)function has bounded variation onΩ, with variation theL¹norm of its weak derivative (TauCeti.HasWeakFDerivOn.totalVariationOn_lt_top_iff_integrableOn).LocallyLipschitzOn.totalVariationOn_eq_setLIntegral_enorm_fderiv: for a locally Lipschitz function, in particular aC¹one, the total variation is∫_Ω ‖Du‖for its classical derivative.HasCompactSupport.totalVariationOn_lt_top: a compactly supported Lipschitz function, in particular a compactly supportedC¹one, has finite total variation on every open set.
References #
- L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, Definition 3.4 and Remark 3.5.
- F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, §12.1.
The total variation of u : E → ℝ on the open set Ω, relative to the measure μ:
the extended supremum of ∫ div φ * u ∂μ over test vector fields φ ∈ 𝓓(Ω, E) with
‖φ x‖ ≤ 1 everywhere. For μ an additive Haar measure this is the variation |Du|(Ω) of the
distributional derivative of u on Ω, defined by duality.
Instances For
The defining supremum of TauCeti.totalVariationOn.
An admissible test vector field bounds the total variation from below.
Upper bounds for the total variation are tested on admissible test vector fields.
Every admissible pairing is bounded in absolute value by the total variation.
The total variation of the zero function vanishes.
Locality. The total variation on Ω only depends on u almost everywhere on Ω.
An admissible test vector field on Ω whose support lies in another open set Ω' is
admissible on Ω', so its pairing is bounded by the total variation on Ω'.
Monotonicity in the open set. A test vector field on a smaller open set is one on the larger set, so the total variation grows with the open set.
Inner continuity in the open set. The total variation on the union of a directed family of open sets is the supremum of the total variations on its members.
Countable subadditivity in the open set. For u locally integrable on ⋃ Ωᵢ,
|Du|(⋃ Ωᵢ) ≤ ∑ |Du|(Ωᵢ).
Subadditivity in the open set. For u locally integrable on Ω ∪ Ω',
|Du|(Ω ∪ Ω') ≤ |Du|(Ω) + |Du|(Ω').
Additivity on disjoint open sets. For u locally integrable on Ω ∪ Ω' with Ω and Ω'
disjoint, |Du|(Ω ∪ Ω') = |Du|(Ω) + |Du|(Ω').
The total variation of -u is that of u.
The total variation is positively homogeneous: |D(c u)|(Ω) = c |Du|(Ω) for c ≥ 0.
The total variation is absolutely homogeneous: |D(c u)|(Ω) = |c| |Du|(Ω).
A test vector field bounded by c pairs to at most c |Du|(Ω).
Subadditivity. For u locally integrable on Ω,
|D(u + v)|(Ω) ≤ |Du|(Ω) + |Dv|(Ω). No integrability of v is needed: when div φ * v is not
integrable, neither is div φ * (u + v), and its pairing is 0.
Against an additive Haar measure, adding a constant does not change the total variation.
No integrability of u is needed.
Against an additive Haar measure, c - u has the same total variation as u. No
integrability of u is needed.
Against an additive Haar measure, a constant function has total variation zero.
Lower semicontinuity #
Lower semicontinuity under distributional convergence. If u i → u₀ as distributions
on Ω, that is ∫ ψ * u i → ∫ ψ * u₀ for every scalar test function ψ on Ω, then
|Du₀|(Ω) ≤ liminf |Du i|(Ω).
Lower semicontinuity under L¹_loc convergence. If u i → u₀ in L¹_loc(Ω), that is
∫_K |u i - u₀| → 0 for every compact K ⊆ Ω, then |Du₀|(Ω) ≤ liminf |Du i|(Ω).
Convergence of variations from an upper bound. If w i → u in L¹_loc(Ω) and the
variations of the w i exceed that of u by amounts tending to zero, then the variations converge.
Lower semicontinuity (totalVariationOn_le_liminf) gives the lower bound.
A bound on the total variation holding frequently along l is preserved under convergence
in L¹(Ω) along l.
Weakly differentiable functions #
A weakly differentiable function has variation at most ∫_Ω ‖Du‖. If u has weak
derivative U on Ω, then |Du|(Ω) ≤ ∫_Ω ‖U‖. In particular a function in W^{1,1}(Ω) has
bounded variation on Ω.
A weakly differentiable function has locally finite variation. If u has a weak
derivative on Ω, every compact K ⊆ Ω has an open neighbourhood on which the variation of u
is finite.
The total variation of a weakly differentiable function. If u has weak derivative U
on Ω, then against an additive Haar measure |Du|(Ω) = ∫_Ω ‖U‖. In particular a function in
W^{1,1}(Ω) has bounded variation on Ω, and its variation is the L¹(Ω) norm of its weak
derivative.
A weakly differentiable function has finite total variation on Ω, against an additive Haar
measure, exactly when its weak derivative is integrable on Ω.
The total variation of a locally Lipschitz function, in particular of a C¹ function,
is the integral of the norm of its classical derivative: |Du|(Ω) = ∫_Ω ‖Du‖, against an
additive Haar measure.
A compactly supported Lipschitz function, in particular a compactly supported C¹ function,
has finite total variation on every open set, against an additive Haar measure.