Variation and perimeter on the real line

On the real line the variational total variation |Du|(Ω) bounds the classical variation of the Lebesgue values of u. If x₀ ≤ x₁ ≤ ⋯ ≤ xₘ are Lebesgue points of u with values v₀, …, vₘ, in the sense that the mean oscillation ⨍_{B(xᵢ, r)} |u - vᵢ| tends to zero, and [x₀, xₘ] ⊆ Ω, then

∑ᵢ |vᵢ₊₁ - vᵢ| ≤ |Du|(Ω)

(TauCeti.Real.ofReal_sum_abs_sub_le_totalVariationOn). The test function is a combination ∑ᵢ εᵢ (ψ (c (y - xᵢ)) - ψ (c (y - xᵢ₊₁))) of smooth steps ψ = Real.smoothTransition with signs εᵢ = sign (vᵢ - vᵢ₊₁). Since the steps decrease along the points, the combination is bounded by the telescoping sum ψ (c (y - x₀)) - ψ (c (y - xₘ)) ≤ 1. Its derivative is a combination of approximate identities concentrating to the right of the points, so its pairing with u converges to ∑ᵢ |vᵢ₊₁ - vᵢ| as c → ∞.

For the indicator of a set s, almost every point is a Lebesgue point with value 0 or 1. Counting alternations between points of s and of its complement gives the sharp one-dimensional isoperimetric inequality and its rigidity:

• a null-measurable s ⊆ ℝ of positive finite measure has perimeter at least 2 (TauCeti.Real.two_le_perimeter);
• if s has finite measure and does not agree almost everywhere with any interval, then it has perimeter at least 4 (TauCeti.Real.four_le_perimeter);
• a bounded open interval has perimeter 2 (TauCeti.Real.perimeter_Ioo), and a set of finite measure has perimeter 2 exactly when it agrees almost everywhere with a nonempty such interval (TauCeti.Real.perimeter_eq_two_iff).

These are the statements about almost every line section that slicing arguments for sets of finite perimeter in higher dimensions apply: a section of perimeter less than 4 is an interval up to a null set.

Main results

• TauCeti.Real.ofReal_sum_abs_sub_le_totalVariationOn: the variation of u along Lebesgue points in Ω is at most |Du|(Ω).
• TauCeti.Real.two_le_perimeter, TauCeti.Real.four_le_perimeter, TauCeti.Real.perimeter_Ioo and TauCeti.Real.perimeter_eq_two_iff.

References

• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, revised edition, §5.10 (functions of bounded variation of one variable).
• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §3.2 (pointwise and essential variation in one variable).

theorem TauCeti.Real.ofReal_sum_abs_sub_le_totalVariationOn {Ω : TopologicalSpace.Opens ℝ} {u : ℝ → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) MeasureTheory.volume) {m : ℕ} {x v : Fin (m + 1) → ℝ} (hx : Monotone x) (hΩ : Set.Icc (x 0) (x (Fin.last m)) ⊆ ↑Ω) (hv : ∀ (i : Fin (m + 1)), Filter.Tendsto (fun (r : ℝ) => ⨍ (y : ℝ) in Metric.closedBall (x i) r, ‖u y - v i‖) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) : ENNReal.ofReal (∑ i : Fin m, |v i.succ - v i.castSucc|) ≤ totalVariationOn MeasureTheory.volume Ω u

The variation along Lebesgue points is bounded by the total variation. Let x₀ ≤ x₁ ≤ ⋯ ≤ xₘ be points with [x₀, xₘ] ⊆ Ω at which u has Lebesgue values vᵢ, that is, the mean oscillation ⨍_{B(xᵢ, r)} |u - vᵢ| tends to zero as r → 0. Then ∑ᵢ |vᵢ₊₁ - vᵢ| ≤ |Du|(Ω).

theorem TauCeti.Real.two_le_perimeter {s : Set ℝ} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (h0 : MeasureTheory.volume s ≠ 0) (hfin : MeasureTheory.volume s ≠ ⊤) : 2 ≤ perimeter MeasureTheory.volume ⊤ s

The isoperimetric inequality on the line. A null-measurable set of positive finite measure in ℝ has perimeter at least two.

theorem TauCeti.Real.four_le_perimeter {s : Set ℝ} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hfin : MeasureTheory.volume s ≠ ⊤) (h : ∀ (I : Set ℝ), I.OrdConnected → ¬s =ᵐ[MeasureTheory.volume] I) : 4 ≤ perimeter MeasureTheory.volume ⊤ s

A null-measurable set of finite measure in ℝ that does not agree almost everywhere with any interval has perimeter at least four.

theorem TauCeti.Real.perimeter_Ioo {a b : ℝ} (hab : a < b) : perimeter MeasureTheory.volume ⊤ (Set.Ioo a b) = 2

A bounded open interval of ℝ has perimeter two.

theorem TauCeti.Real.perimeter_eq_two_iff {s : Set ℝ} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hfin : MeasureTheory.volume s ≠ ⊤) : perimeter MeasureTheory.volume ⊤ s = 2 ↔ ∃ (a : ℝ) (b : ℝ), a < b ∧ s =ᵐ[MeasureTheory.volume] Set.Ioo a b

Equality in the isoperimetric inequality on the line. A null-measurable set of finite measure in ℝ has perimeter two exactly when it agrees almost everywhere with a nonempty bounded open interval.