Documentation

TauCeti.Analysis.BoundedVariation.Translation

Translation of distributional total variation and perimeter #

Distributional total variation is unchanged when the function and its open domain are translated by the same vector. More generally, translating a function from an open set Ω back to an open set V does not increase its variation whenever V + h ⊆ Ω. The equality follows when the two open sets are exact translates. The corresponding statements for perimeter transport sets by the same translation.

The proof translates each admissible compactly supported test vector field in the opposite direction. Translation preserves both its pointwise norm and its divergence, and a right-invariant measure, such as an additive Haar measure, makes the resulting distributional pairings equal.

These results give the translation part of affine-isometric transport for BV functions and sets of finite perimeter. No integrability, measurability, boundedness, or finiteness assumption is needed.

The file also proves the translation estimate ∫_V |u (x + h) - u x| dx ≤ ‖h‖ |Du|(Ω) for u locally integrable on Ω, when the segments x + [0, 1] h starting in V lie in Ω. By the duality ∫_V |w| = sup ∫ w g over scalar test functions |g| ≤ 1 on V, it suffices to bound ∫ (u (x + h) - u x) g x dx. Translation invariance turns this into ∫ u (g (· - h) - g), and g (y - h) - g y = -∂_h Φ y for the test function Φ y = ∫₀¹ g (y - t h) dt, and ∂_h Φ is the divergence of the test vector field Φ h, of norm at most ‖h‖.

The same identity shows that a function whose distributional derivative in the direction h is nonnegative is nondecreasing along h: u x ≤ u (x + h) for almost every x ∈ V. Indeed Φ is nonnegative when g is, so u (· + h) - u has nonnegative pairings with nonnegative test functions.

Main declarations #

References #

source
theorem TauCeti.totalVariationOn_comp_add_right_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {u : E → ℝ} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Ω) :
(totalVariationOn μ V fun (x : E) => u (x + h)) ≤ totalVariationOn μ Ω u

Translating a function from Ω back to V does not increase its total variation when V + h ⊆ Ω.

source
theorem TauCeti.totalVariationOn_comp_add_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {u : E → ℝ} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Ω) (hOV : Set.MapsTo (fun (x : E) => x - h) ↑Ω ↑V) :
(totalVariationOn μ V fun (x : E) => u (x + h)) = totalVariationOn μ Ω u

Translation invariance of total variation. If translation by h maps V into Ω and translation by -h maps Ω back into V, then translating the function and its domain together does not change its total variation.

source
theorem TauCeti.totalVariationOn_comap_add_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {u : E → ℝ} :
(totalVariationOn μ ((TopologicalSpace.Opens.comap (ContinuousMap.addRight h)) Ω) fun (x : E) => u (x + h)) = totalVariationOn μ Ω u

Total variation is invariant when the translated domain is written canonically as the preimage open set.

source
theorem TauCeti.perimeter_preimage_add_right_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Ω) :
perimeter μ V ((fun (x : E) => x + h) ⁻¹' s) ≤ perimeter μ Ω s

Translating a set and an open domain together cannot increase perimeter when the translated domain lies in the original domain.

source
theorem TauCeti.perimeter_preimage_add_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} (hVO : Set.MapsTo (fun (x : E) => x + h) ↑V ↑Ω) (hOV : Set.MapsTo (fun (x : E) => x - h) ↑Ω ↑V) :
perimeter μ V ((fun (x : E) => x + h) ⁻¹' s) = perimeter μ Ω s

Translation invariance of perimeter. If translation by h identifies V with Ω, then the perimeter in V of the translate by -h of s equals the perimeter of s in Ω.

source
theorem TauCeti.perimeter_comap_add_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} :
perimeter μ ((TopologicalSpace.Opens.comap (ContinuousMap.addRight h)) Ω) ((fun (x : E) => x + h) ⁻¹' s) = perimeter μ Ω s

Perimeter is invariant when a set and its ambient open set are both pulled back by the same translation.

The translation estimate #

source
theorem TauCeti.setLIntegral_enorm_comp_add_sub_le_mul_totalVariationOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hVΩ : ∀ t ∈ Set.Icc 0 1, Set.MapsTo (fun (x : E) => x + t • h) ↑V ↑Ω) :
∫⁻ (x : E) in ↑V, ‖u (x + h) - u x‖ₑ ∂μ ≤ ‖h‖ₑ * totalVariationOn μ Ω u

The translation estimate for functions of bounded variation. If the segments x + [0, 1] h starting at the points x ∈ V lie in Ω, then every u locally integrable on Ω satisfies ∫_V |u (x + h) - u x| dx ≤ ‖h‖ |Du|(Ω), finite or infinite.

source
theorem TauCeti.ae_le_comp_add_of_forall_integral_lineDeriv_mul_nonpos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {Ω V : TopologicalSpace.Opens E} {h : E} [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hVΩ : ∀ t ∈ Set.Icc 0 1, Set.MapsTo (fun (x : E) => x + t • h) ↑V ↑Ω) (H : ∀ (φ : TestFunction Ω ℝ ⊤), (∀ (x : E), 0 ≤ φ x) → ∫ (x : E), lineDeriv ℝ (⇑φ) x h * u x ∂μ ≤ 0) :
∀ᵐ (x : E) ∂μ.restrict ↑V, u x ≤ u (x + h)

Monotonicity from a nonnegative directional derivative. Let u be locally integrable on Ω, and suppose that its distributional derivative in the direction h is nonnegative: ∫ u ∂_h φ ≤ 0 for every nonnegative test function φ on Ω. Then u x ≤ u (x + h) for almost every x ∈ V, as soon as the segments x + [0, 1] h starting in V lie in Ω.

source
theorem TauCeti.lintegral_enorm_comp_add_sub_le_mul_totalVariationOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrable u μ) (h : E) :
∫⁻ (x : E), ‖u (x + h) - u x‖ₑ ∂μ ≤ ‖h‖ₑ * totalVariationOn μ ⊤ u

The translation estimate on the whole space. Every locally integrable u satisfies ∫ |u (x + h) - u x| dx ≤ ‖h‖ |Du|(E), finite or infinite.