Lipschitz composition of functions of bounded variation

For a real function locally integrable on an arbitrary Euclidean open set and a C-Lipschitz scalar map g, composition satisfies |D(g ∘ u)|(Ω) ≤ C |Du|(Ω). This is a variation inequality; it allows jumps and does not assert the classical chain rule for the derivative measure.

The estimate uses the variational total variation TauCeti.totalVariationOn. Local mollification, its variation bound, and lower semicontinuity extend the derivative estimate from smooth inner functions to locally integrable functions. Neither finite variation nor finite volume is required for the inequality. BV membership additionally needs integrability of the composite; the condition g 0 = 0 supplies it on domains of arbitrary volume.

The central formal inputs are TauCeti.exists_mollifier_seq_of_isCompact_closure and TauCeti.totalVariationOn_le_liminf. The shared compact localization lemma extracts the mollification argument from TauCeti.Analysis.BoundedVariation.Coarea.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, Chapter 3 (approximation and composition).

theorem TauCeti.totalVariationOn_comp_lipschitz_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → ℝ} {g : ℝ → ℝ} {C : NNReal} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hg : LipschitzWith C g) : totalVariationOn μ Ω (g ∘ u) ≤ ↑C * totalVariationOn μ Ω u

Lipschitz composition bounds distributional variation. For locally integrable u on an open set, |D(g ∘ u)|(Ω) ≤ C |Du|(Ω) whenever g is C-Lipschitz. This includes infinite variation, arbitrary open domains, and scalar maps that do not vanish at zero.

theorem TauCeti.MemBV.comp_lipschitz_of_integrable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → ℝ} {g : ℝ → ℝ} {C : NNReal} (hu : MemBV μ Ω u) (hg : LipschitzWith C g) (hint : MeasureTheory.IntegrableOn (g ∘ u) (↑Ω) μ) : MemBV μ Ω (g ∘ u)

Lipschitz composition preserves BV provided the composite is integrable. This hypothesis allows scalar maps with arbitrary value at zero on domains of infinite volume.

theorem TauCeti.MemBV.comp_lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → ℝ} {g : ℝ → ℝ} {C : NNReal} (hu : MemBV μ Ω u) (hg : LipschitzWith C g) (hg0 : g 0 = 0) : MemBV μ Ω (g ∘ u)

A Lipschitz scalar map vanishing at zero preserves BV, without a finite-volume assumption on the domain.