The perimeter of a set in an open set #
The perimeter of a set s in an open set Ω of a finite-dimensional real inner product space
is the total variation of its indicator on Ω (TauCeti.perimeter). For a measurable s this is
De Giorgi's extended perimeter
P(s; Ω) = ⨆ { ∫_s div φ | φ ∈ 𝓓(Ω, E), ‖φ x‖ ≤ 1 for all x }
(TauCeti.perimeter_eq_iSup), defined without any regularity of its topological boundary. It is
the measure-theoretic notion of boundary area: a measurable set has finite perimeter in Ω
exactly when P(s; Ω) < ∞, which does not require s to have finite volume. The perimeter is
meaningful when s ∩ Ω is null-measurable; otherwise the integrals in the supremum may be
Mathlib's junk value 0 for non-integrable functions, and the perimeter may then be a junk value
carrying no geometric meaning.
The perimeter only sees s up to null sets (TauCeti.perimeter_congr_ae), so topological
frontier and perimeter can differ, and it only sees s ∩ Ω
(TauCeti.perimeter_congr_of_inter_eq). Against an additive Haar measure, complements have the same
perimeter (TauCeti.perimeter_compl), since their indicators differ by a constant. Lower
semicontinuity under local convergence in measure (TauCeti.perimeter_le_liminf) supplies
the semicontinuity half of the direct method for perimeter problems.
Main declarations #
TauCeti.perimeter μ Ω s: the perimeter ofsinΩ.TauCeti.perimeter_eq_iSup: the perimeter of a null-measurable set as a supremum of∫_s div φ.TauCeti.perimeter_congr_ae,TauCeti.perimeter_congr_of_inter_eq,TauCeti.perimeter_monoandTauCeti.perimeter_iSup: invariance under null modification insideΩand locality, and monotonicity and inner continuity inΩ.TauCeti.perimeter_compl,TauCeti.perimeter_emptyandTauCeti.perimeter_univ.TauCeti.perimeter_le_liminf: lower semicontinuity of the perimeter.
References #
- F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, §12.1 and Proposition 12.15.
The perimeter of a set s in the open set Ω, relative to the measure μ: the total
variation of the indicator of s on Ω. For a null-measurable s it is the extended supremum
of ∫_s div φ ∂μ over test vector fields φ ∈ 𝓓(Ω, E) with ‖φ x‖ ≤ 1 everywhere
(TauCeti.perimeter_eq_iSup).
Instances For
The perimeter is the total variation of the indicator.
The perimeter by duality. For a null-measurable set s,
P(s; Ω) = ⨆ { ∫_s div φ ∂μ | φ ∈ 𝓓(Ω, E), ‖φ‖ ≤ 1 }.
Locality. Modifying a set by a null set inside Ω does not change its perimeter in
Ω.
Locality of the perimeter. Sets that agree on Ω have the same perimeter in Ω.
The perimeter grows with the open set.
Inner continuity in the open set. The perimeter in the union of a directed family of open sets is the supremum of the perimeters in its members.
The empty set has perimeter zero.
Complements have the same perimeter, against an additive Haar measure. No measurability
of s is needed: the indicators of s and sᶜ differ by a constant up to sign.
The whole space has perimeter zero, against an additive Haar measure.
Lower semicontinuity #
Lower semicontinuity of the perimeter. If the sets s i converge to s₀ locally in
measure in Ω, that is μ ((s i ∆ s₀) ∩ K) → 0 for every compact K ⊆ Ω, then
P(s₀; Ω) ≤ liminf P(s i; Ω).