The polar decomposition of the derivative of a function of locally bounded variation #
Let Ω be an open set of a finite-dimensional real inner product space E and let u : E → ℝ be
locally integrable on Ω, with locally finite variation: every compact K ⊆ Ω has an open
neighbourhood U with |Du|(U) < ∞. The distributional derivative Du is then a vector-valued
Radon measure on Ω, absolutely continuous with respect to its variation measure |Du|
(TauCeti.variationMeasure) with a density of norm one:
Du = σ_u |Du|, that is, ∫ u div φ dμ = -∫ ⟪φ, σ_u⟫ d|Du| for every φ ∈ 𝓓(Ω, E),
with ‖σ_u‖ = 1 at |Du|-almost every point. This is the structure theorem for functions of
locally bounded variation. The polar density σ_u is TauCeti.polarDensity. It is unique
|Du|-almost everywhere (TauCeti.ae_eq_polarDensity). For the indicator χ_E of a set of
locally finite perimeter, the sign convention Dχ_E = -ν_E |Dχ_E| makes -σ_{χ_E} the
measure-theoretic outer unit normal ν_E.
The proof assembles the directional derivatives ∂_{bᵢ} u along an orthonormal basis, each a
difference of two regular measures (TauCeti.exists_regular_lineDeriv_ofFun_apply_eq). With
respect to a common reference measure ρ, which also dominates |Du|
(MeasureTheory.Measure.exists_common_density_sub), their densities form a vector field g with
∫ u div φ dμ = -∫ ⟪φ, g⟫ dρ. A pairing with a test vector field of norm at most one supported in
U is bounded by |Du|(U), so ‖g‖ is at most the density of |Du| with respect to ρ
(TauCeti.ae_enorm_le_of_forall_enorm_integral_inner_le), and σ_u = g / (d|Du|/dρ) has norm at
most one. Testing the definition of |Du|(U) as a supremum against this representation gives
|Du|(U) ≤ ∫_U ‖σ_u‖ d|Du|, hence ‖σ_u‖ = 1 (TauCeti.ae_eq_one_of_measure_le_setLIntegral).
Main declarations #
TauCeti.polarDensity μ Ω u: the polar densityσ_u : Ω → EofDuwith respect to|Du|.TauCeti.integral_divergenceCLM_mul_eq_neg_integral_inner_polarDensity: the representation∫ u div φ dμ = -∫ ⟪φ, σ_u⟫ d|Du|.TauCeti.integral_lineDeriv_mul_eq_neg_integral_mul_inner_polarDensity: its directional form∫ ∂_v φ · u dμ = -∫ φ ⟪v, σ_u⟫ d|Du|for scalar test functions.TauCeti.ae_norm_polarDensity_eq_one:‖σ_u‖ = 1at|Du|-almost every point.TauCeti.locallyIntegrable_polarDensity:σ_uis locally integrable with respect to|Du|.TauCeti.ae_eq_polarDensity: a locally integrable vector field representingDuagainst|Du|isσ_ualmost everywhere.TauCeti.enorm_integral_divergenceCLM_mul_le_lintegral_enorm: the pairing is bounded by∫ ‖φ‖ d|Du|.TauCeti.integrable_inner_polarDensityandTauCeti.dist_integral_inner_polarDensity_le: continuous compactly supported fields pair integrably withDu, with uniform error controlled by the variation measure of a common compact support.TauCeti.integral_trace_fderiv_mul_eq_neg_integral_inner_polarDensity: the representation extends to everyC¹vector fieldφwith compact support inΩ, withdiv φ = tr (Dφ). Mollification gives test fields converging toφuniformly together with their derivatives (ContDiff.exists_testFunction_dist_le_and_dist_fderiv_le), and both sides are continuous for this convergence (TauCeti.dist_integral_trace_fderiv_mul_leandTauCeti.dist_integral_inner_polarDensity_le).TauCeti.polarDensity_congr_aeandTauCeti.polarDensity_const_sub:σ_uonly depends onualmost everywhere onΩ, andσ_{c - u} = -σ_uagainst an additive Haar measure.
References #
- L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.1, Theorem 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.4 (polar decomposition) and §3.1.
The polar density σ_u of the derivative of u on Ω with respect to its variation
measure |Du|: if u is locally integrable on Ω with locally finite variation there, it is a
measurable vector field σ_u : Ω → E with ‖σ_u‖ = 1 at |Du|-almost every point
(TauCeti.ae_norm_polarDensity_eq_one) such that Du = σ_u |Du|, that is,
∫ u div φ dμ = -∫ ⟪φ, σ_u⟫ d|Du| for every test vector field φ on Ω
(TauCeti.integral_divergenceCLM_mul_eq_neg_integral_inner_polarDensity). It is determined
|Du|-almost everywhere (TauCeti.ae_eq_polarDensity). If no such field exists it is 0 by
convention.
Instances For
The polar density is measurable.
The polar decomposition Du = σ_u |Du|. For u locally integrable on Ω with locally
finite variation, ∫ u div φ dμ = -∫ ⟪φ, σ_u⟫ d|Du| for every test vector field φ on Ω.
The directional derivative ⟪v, Du⟫ = ⟪v, σ_u⟫ |Du|. For u locally integrable on Ω
with locally finite variation, ∫ ∂_v φ · u dμ = -∫ φ ⟪v, σ_u⟫ d|Du| for every scalar test
function φ on Ω and every vector v.
The polar density of a function of locally finite variation has norm one at |Du|-almost
every point.
The polar density is locally integrable with respect to |Du|. (If u is not locally
integrable with locally finite variation, |Du| = 0.)
Uniqueness of the polar density. A locally integrable vector field σ on Ω with
∫ u div φ dμ = -∫ ⟪φ, σ⟫ d|Du| for every test vector field φ agrees with σ_u at
|Du|-almost every point.
The pairing of u with a test vector field φ on Ω is bounded by ∫ ‖φ‖ d|Du|.
Locality of the polar density. If u = v almost everywhere on Ω, then σ_u = σ_v at
|Du|-almost every point.
Against an additive Haar measure, the polar density of c - u is -σ_u at |Du|-almost
every point. In particular the polar densities of the indicators of a set and of its complement
are opposite.
A continuous field compactly supported in the domain pairs integrably with the derivative of a locally BV function, represented by its polar density against its variation measure.
Uniformly close continuous fields supported in a fixed compact set have close derivative pairings, with constant the variation measure of that compact set.
Integration by parts against C¹ vector fields. For u locally integrable on Ω with
locally finite variation, the polar decomposition Du = σ_u |Du| represents the distributional
derivative against every C¹ vector field φ with compact support in Ω:
∫ u div φ dμ = -∫ ⟪φ, σ_u⟫ d|Du|, where div φ = tr (Dφ).