Lebesgue decomposition of the BV derivative

For a locally integrable function of locally finite variation, write Du = σ |Du| using polarDensity. Relative to a σ-finite reference measure ν on the open domain, the absolutely continuous part of Du has density acDerivativeDensity μ Ω u ν = (d|Du|/dν) σ. The remaining part is σ (|Du|.singularPart ν). We prove the distributional identity for their sum and the splitting of the variation measure, including local integrability of the density. Taking ν = μ.comap Subtype.val gives the usual absolutely continuous/singular decomposition on the domain. No global finiteness of |Du| or integrability of u is required.

The variation measure satisfies |Du| = ν.withDensity (fun x => ‖acDerivativeDensity μ Ω u ν x‖ₑ) + |Du|.singularPart ν (withDensity_enorm_acDerivativeDensity_add_singularPart). The second measure is mutually singular to ν by Mathlib's Measure.mutuallySingular_singularPart. The distributional identity describes the derivative through its action on test fields; no globally finite vector measure is imposed on an unbounded domain. The density is unique ν-almost everywhere among locally integrable densities in such a decomposition (ae_eq_acDerivativeDensity), including when the competing singular reference measure is not σ-finite.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §3.1 (Lebesgue decomposition of the derivative).

noncomputable def TauCeti.acDerivativeDensity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) (Ω : TopologicalSpace.Opens E) (u : E → ℝ) (ν : MeasureTheory.Measure ↥Ω) : ↥Ω → E

The density of the absolutely continuous part of Du relative to ν on Ω. It is the Radon–Nikodym density of |Du| multiplied by its polar field.

theorem TauCeti.acDerivativeDensity_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (ν : MeasureTheory.Measure ↥Ω) (x : ↥Ω) : acDerivativeDensity μ Ω u ν x = ((variationMeasure μ Ω u).rnDeriv ν x).toReal • polarDensity μ Ω u x

The defining formula for the absolutely continuous derivative density.

theorem TauCeti.measurable_acDerivativeDensity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (ν : MeasureTheory.Measure ↥Ω) : Measurable (acDerivativeDensity μ Ω u ν)

The absolutely continuous derivative density is measurable.

theorem TauCeti.ae_enorm_acDerivativeDensity_eq_rnDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (ν : MeasureTheory.Measure ↥Ω) : (fun (x : ↥Ω) => ‖acDerivativeDensity μ Ω u ν x‖ₑ) =ᵐ[ν] (variationMeasure μ Ω u).rnDeriv ν

The norm of the absolutely continuous derivative density is exactly d|Du|/dν, including where this Radon–Nikodym derivative vanishes.

theorem TauCeti.withDensity_enorm_acDerivativeDensity_add_singularPart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (ν : MeasureTheory.Measure ↥Ω) [MeasureTheory.SigmaFinite ν] : (ν.withDensity fun (x : ↥Ω) => ‖acDerivativeDensity μ Ω u ν x‖ₑ) + (variationMeasure μ Ω u).singularPart ν = variationMeasure μ Ω u

The variation measure splits into the norm of the absolutely continuous derivative and the singular variation measure. The latter is mutually singular to ν.

theorem TauCeti.lintegral_enorm_acDerivativeDensity_add_singularPart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (ν : MeasureTheory.Measure ↥Ω) [MeasureTheory.SigmaFinite ν] (s : Set ↥Ω) : ∫⁻ (x : ↥Ω) in s, ‖acDerivativeDensity μ Ω u ν x‖ₑ ∂ν + ((variationMeasure μ Ω u).singularPart ν) s = (variationMeasure μ Ω u) s

On every subset, variation is the integral of the norm of the absolutely continuous derivative plus the singular variation, as an extended-valued identity.

theorem TauCeti.locallyIntegrable_acDerivativeDensity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (ν : MeasureTheory.Measure ↥Ω) : MeasureTheory.LocallyIntegrable (acDerivativeDensity μ Ω u ν) ν

The absolutely continuous derivative density is locally integrable even when the whole derivative has infinite variation.

theorem TauCeti.integrable_acDerivativeDensity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (ν : MeasureTheory.Measure ↥Ω) (hvar : totalVariationOn μ Ω u ≠ ⊤) : MeasureTheory.Integrable (acDerivativeDensity μ Ω u ν) ν

Finite total variation implies integrability of the absolutely continuous derivative density. Global integrability of the original function is not required.

theorem TauCeti.integral_divergenceCLM_mul_eq_neg_integral_inner_acDerivativeDensity_sub_singularPart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (ν : MeasureTheory.Measure ↥Ω) [MeasureTheory.SigmaFinite ν] (φ : TestFunction Ω E ⊤) : ∫ (x : E), (TestFunction.divergenceCLM φ) x * u x ∂μ = -∫ (x : ↥Ω), inner ℝ (φ ↑x) (acDerivativeDensity μ Ω u ν x) ∂ν - ∫ (x : ↥Ω), inner ℝ (φ ↑x) (polarDensity μ Ω u x) ∂(variationMeasure μ Ω u).singularPart ν

Lebesgue decomposition of the BV derivative. The distributional derivative is the sum of the density acDerivativeDensity μ Ω u ν against ν and the polar field against the singular part of |Du|. Both pairings are integrable because the test field has compact support.

theorem TauCeti.ae_eq_acDerivativeDensity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ (U : TopologicalSpace.Opens E), K ⊆ ↑U ∧ totalVariationOn μ U u ≠ ⊤) (ν : MeasureTheory.Measure ↥Ω) [MeasureTheory.SigmaFinite ν] {g τ : ↥Ω → E} {ξ : MeasureTheory.Measure ↥Ω} (hg : MeasureTheory.LocallyIntegrable g ν) (hτ : MeasureTheory.LocallyIntegrable τ ξ) (hξ : ξ.MutuallySingular ν) (h : ∀ (φ : TestFunction Ω E ⊤), ∫ (x : E), (TestFunction.divergenceCLM φ) x * u x ∂μ = -∫ (x : ↥Ω), inner ℝ (φ ↑x) (g x) ∂ν - ∫ (x : ↥Ω), inner ℝ (φ ↑x) (τ x) ∂ξ) : g =ᵐ[ν] acDerivativeDensity μ Ω u ν

Uniqueness of the absolutely continuous derivative density. Any locally integrable g representing Du together with a locally integrable density against a measure singular to ν agrees with acDerivativeDensity at ν-almost every point.

theorem TauCeti.acDerivativeDensity_congr_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (ν : MeasureTheory.Measure ↥Ω) {v : E → ℝ} (h : u =ᵐ[μ.restrict ↑Ω] v) : acDerivativeDensity μ Ω u ν =ᵐ[ν] acDerivativeDensity μ Ω v ν

The absolutely continuous derivative density is unchanged almost everywhere if the original function is changed on a null subset of its domain.