Geometric measure theory: rectifiability, BV, and finite perimeter

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe weighted area formula with multiplicity#

Integrating the geometric Jacobian of a Lipschitz map against a nonnegative measurable weight equals the normalized Hausdorff integral of the sum of the weights over each fiber. The parameter set may be Lebesgue measurable rather than Borel, and infinite fibers use extended sums.

LipschitzWith.lintegral_normDet_fderiv_mul_eq_lintegral_tsum.{u_1, u_2} {U : Type u_1}
  {V : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace U]
  [BorelSpace U] [MeasurableSpace V] [BorelSpace V] {f : U → V} {s : Set U} {g : U → ENNReal}
  {K : NNReal} (hf : LipschitzWith K f)
  (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (hg : Measurable g) :
  ∫⁻ (x : U) in s, ENNReal.ofReal (↑(fderiv ℝ f x)).normDet * g x =
    ∫⁻ (y : V),
      ∑' (x : ↑(s ∩ f ⁻¹' {y})),
        g ↑x ∂MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ U)

Lean

Formalized in Tau Ceti as LipschitzWith.lintegral_normDet_fderiv_mul_eq_lintegral_tsum.

Sources

• Tau Ceti documentation: LipschitzWith.lintegral_normDet_fderiv_mul_eq_lintegral_tsum
• Source of LipschitzWith.lintegral_normDet_fderiv_mul_eq_lintegral_tsum in TauCeti/MeasureTheory/Function/AreaFormula/Multiplicity.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanLipschitzWith.lintegral_normDet_fderiv_mul_eq_lintegral_tsum

TheoremThe coarea formula for total variation#

For u locally integrable on Ω, against an additive Haar measure, the total variation of u is the integral of the perimeters of its superlevel sets: |Du|(Ω) = ∫_ℝ P({u > t}; Ω) dt, finite or infinite.

TauCeti.totalVariationOn_eq_lintegral_perimeter.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {Ω : TopologicalSpace.Opens E} {u : E → ℝ}
  (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) :
  TauCeti.totalVariationOn μ Ω u = ∫⁻ (t : ℝ), TauCeti.perimeter μ Ω {x | t < u x}

Lean

Formalized in Tau Ceti as TauCeti.totalVariationOn_eq_lintegral_perimeter.

Sources

• Tau Ceti documentation: TauCeti.totalVariationOn_eq_lintegral_perimeter
• Source of TauCeti.totalVariationOn_eq_lintegral_perimeter in TauCeti/Analysis/BoundedVariation/Coarea.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.totalVariationOn_eq_lintegral_perimeter

Uses 3 · Used by 1

Statement usesTauCeti.perimeter · TauCeti.totalVariationOn

Proof usesRademacher's theorem for locally Lipschitz functions

Used byThe sharp BV Sobolev bound

TheoremBanach indicatrix formula#

The variation of a continuous curve on [a, b] is the raw one-dimensional Hausdorff integral of the extended cardinality of its fibers. No Lipschitz or bounded-variation hypothesis is needed: both sides are infinite together. Pauses and repeated traversals are allowed, and infinite fibers have infinite multiplicity.

ContinuousOn.eVariationOn_eq_lintegral_encard.{u_1} {X : Type u_1} [EMetricSpace X]
  [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) :
  eVariationOn γ (Set.Icc a b) =
    ∫⁻ (y : X), ↑(Set.Icc a b ∩ γ ⁻¹' {y}).encard ∂MeasureTheory.Measure.hausdorffMeasure 1

Lean

Formalized in Tau Ceti as ContinuousOn.eVariationOn_eq_lintegral_encard.

Sources

• Tau Ceti documentation: ContinuousOn.eVariationOn_eq_lintegral_encard
• Source of ContinuousOn.eVariationOn_eq_lintegral_encard in TauCeti/Topology/EMetricSpace/CurveLength.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanContinuousOn.eVariationOn_eq_lintegral_encard

Uses 1

Proof usesBanach indicatrix inequality

TheoremTauCeti.euclideanHausdorffMeasure_sphere#

A sphere of radius r > 0 in an n-dimensional real inner product space has (n - 1)-dimensional Hausdorff measure n ω_n r ^ (n - 1), where ω_n is the volume of the unit ball.

TauCeti.euclideanHausdorffMeasure_sphere.{u_2} {E : Type u_2} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (c : E) {r : ℝ}
  (hr : 0 < r) :
  (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ E - 1)) (Metric.sphere c r) =
    ↑(Module.finrank ℝ E) * MeasureTheory.volume (Metric.ball 0 1) *
      ENNReal.ofReal r ^ (Module.finrank ℝ E - 1)

Lean

Formalized in Tau Ceti as TauCeti.euclideanHausdorffMeasure_sphere.

Sources

• Tau Ceti documentation: TauCeti.euclideanHausdorffMeasure_sphere
• Source of TauCeti.euclideanHausdorffMeasure_sphere in TauCeti/Geometry/Euclidean/Volume/Sphere.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.euclideanHausdorffMeasure_sphere

TheoremThe Sobolev inequality for functions of bounded variation#

Let E have dimension n ≥ 2 and let p = n / (n - 1). Every integrable u : E → ℝ satisfies ‖u‖_p ≤ C |Du|(E), where |Du|(E) is the total variation of u on the whole space, finite or infinite, and C is the constant MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the C¹ Gagliardo–Nirenberg– Sobolev inequality MeasureTheory.eLpNorm_le_eLpNorm_fderiv_one.

TauCeti.eLpNorm_le_totalVariationOn.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {p : NNReal} {u : E → ℝ}
  (hu : MeasureTheory.Integrable u μ) (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) :
  MeasureTheory.eLpNorm u (↑p) μ ≤
    ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * TauCeti.totalVariationOn μ ⊤ u

Lean

Formalized in Tau Ceti as TauCeti.eLpNorm_le_totalVariationOn.

Sources

• Tau Ceti documentation: TauCeti.eLpNorm_le_totalVariationOn
• Source of TauCeti.eLpNorm_le_totalVariationOn in TauCeti/Analysis/BoundedVariation/Sobolev/Basic.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.eLpNorm_le_totalVariationOn

Uses 3 · Used by 1

Statement usesTauCeti.totalVariationOn

Proof usesThe Gagliardo–Nirenberg–Sobolev inequality for integrable functions · Rademacher's theorem for locally Lipschitz functions

Used byThe nonsharp isoperimetric inequality

TheoremThe nonsharp isoperimetric inequality#

Let E have dimension n ≥ 2 and let p = n / (n - 1). Every null-measurable set s of finite measure satisfies μ(s) ^ (1/p) ≤ C P(s; E), where 1/p = 1 - 1/n, P(s; E) is the perimeter of s in the whole space, finite or infinite, and C is the constant MeasureTheory.eLpNormLESNormFDerivOneConst μ p of the Gagliardo–Nirenberg–Sobolev inequality.

TauCeti.measure_rpow_le_perimeter.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {p : NNReal} {s : Set E}
  (hs : MeasureTheory.NullMeasurableSet s μ) (hμs : μ s ≠ ⊤)
  (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) :
  μ s ^ (↑p)⁻¹ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * TauCeti.perimeter μ ⊤ s

Lean

Formalized in Tau Ceti as TauCeti.measure_rpow_le_perimeter.

Sources

• Tau Ceti documentation: TauCeti.measure_rpow_le_perimeter
• Source of TauCeti.measure_rpow_le_perimeter in TauCeti/Analysis/BoundedVariation/Sobolev/Basic.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.measure_rpow_le_perimeter

Uses 3

Statement usesTauCeti.perimeter

Proof usesThe Sobolev inequality for functions of bounded variation · TauCeti.totalVariationOn

DefinitionTauCeti.totalVariationOn#

The total variation of u : E → ℝ on the open set Ω, relative to the measure μ: the extended supremum of ∫ div φ * u ∂μ over test vector fields φ ∈ 𝓓(Ω, E) with ‖φ x‖ ≤ 1 everywhere. For μ an additive Haar measure this is the variation |Du|(Ω) of the distributional derivative of u on Ω, defined by duality.

TauCeti.totalVariationOn.{u_1} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E)
  (Ω : TopologicalSpace.Opens E) (u : E → ℝ) : ENNReal

Lean

Formalized in Tau Ceti as TauCeti.totalVariationOn.

Sources

• Tau Ceti documentation: TauCeti.totalVariationOn
• Source of TauCeti.totalVariationOn in TauCeti/Analysis/BoundedVariation/TotalVariation.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.totalVariationOn

Used by 11

Used byLebesgue decomposition of the BV derivative · The Gauss–Green formula, Dχ_s = -ν_s |Dχ_s| · The Poincaré inequality for functions of bounded variation on a ball · The Poincaré–Wirtinger inequality for functions of bounded variation, localized to a subset · TauCeti.perimeter · The coarea formula for total variation · The directional derivatives of a function of locally finite variation are signed Radon measures · The nonsharp isoperimetric inequality · The sharp BV Sobolev bound · The Sobolev inequality for functions of bounded variation · The isoperimetric inequality on the line

DefinitionTauCeti.perimeter#

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).

TauCeti.perimeter.{u_1} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] (μ : MeasureTheory.Measure E)
  (Ω : TopologicalSpace.Opens E) (s : Set E) : ENNReal

Lean

Formalized in Tau Ceti as TauCeti.perimeter.

Sources

• Tau Ceti documentation: TauCeti.perimeter
• Source of TauCeti.perimeter in TauCeti/Analysis/BoundedVariation/Perimeter.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.perimeter

Uses 1 · Used by 4

Statement usesTauCeti.totalVariationOn

Used byThe coarea formula for total variation · The nonsharp isoperimetric inequality · The sharp BV Sobolev bound · The isoperimetric inequality on the line

TheoremBoundedVariationOn.exists_arclength_factorization#

A continuous rectifiable curve factors through a 1-Lipschitz curve on its length interval. The factor has exactly the parameter difference as variation on every subinterval, including when the original curve has pauses or zero length. Values of the factor outside its length interval are unspecified.

BoundedVariationOn.exists_arclength_factorization.{u_1} {X : Type u_1} [MetricSpace X] {γ : ℝ → X}
  {a b : ℝ} (hγ : BoundedVariationOn γ (Set.Icc a b)) (hcont : ContinuousOn γ (Set.Icc a b))
  (hab : a ≤ b) :
  ∃ g,
    LipschitzOnWith 1 g (Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal) ∧
      Set.EqOn (g ∘ variationOnFromTo γ (Set.Icc a b) a) γ (Set.Icc a b) ∧
        ∀ u ∈ Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal,
          ∀ v ∈ Set.Icc 0 (eVariationOn γ (Set.Icc a b)).toReal,
            u ≤ v → eVariationOn g (Set.Icc u v) = ENNReal.ofReal (v - u)

Lean

Formalized in Tau Ceti as BoundedVariationOn.exists_arclength_factorization.

Sources

• Tau Ceti documentation: BoundedVariationOn.exists_arclength_factorization
• Source of BoundedVariationOn.exists_arclength_factorization in TauCeti/Topology/MetricSpace/Arclength/Basic.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanBoundedVariationOn.exists_arclength_factorization

TheoremThe directional derivatives of a function of locally finite variation are signed Radon measures#

If every compact K ⊆ Ω has an open neighbourhood U on which u has finite total variation, then for every direction v there are regular measures ν₁ and ν₂ on Ω with ∂_v u (φ) = ∫ φ dν₁ - ∫ φ dν₂ for every test function φ, where ∂_v u is the derivative of the distribution Distribution.ofFun Ω u μ ⊤. If u is locally integrable on Ω, this is the distributional derivative of u, ∂_v u (φ) = -∫ ∂_v φ * u; otherwise Distribution.ofFun is zero by convention and the statement is trivial. The measures are finite on compact subsets of Ω but need not be finite.

TauCeti.exists_regular_lineDeriv_ofFun_apply_eq.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E}
  {Ω : TopologicalSpace.Opens E} {u : E → ℝ} [BorelSpace E]
  (hu : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ U, K ⊆ ↑U ∧ TauCeti.totalVariationOn μ U u ≠ ⊤)
  (v : E) :
  ∃ ν₁ ν₂,
    ν₁.Regular ∧
      ν₂.Regular ∧
        ∀ (φ : TestFunction Ω ℝ ⊤),
          (LineDeriv.lineDerivOp v (Distribution.ofFun Ω u μ ⊤)) φ =
            ∫ (x : ↥Ω), φ ↑x ∂ν₁ - ∫ (x : ↥Ω), φ ↑x ∂ν₂

Lean

Formalized in Tau Ceti as TauCeti.exists_regular_lineDeriv_ofFun_apply_eq.

Sources

• Tau Ceti documentation: TauCeti.exists_regular_lineDeriv_ofFun_apply_eq
• Source of TauCeti.exists_regular_lineDeriv_ofFun_apply_eq in TauCeti/Analysis/BoundedVariation/DerivativeMeasure.lean
• Tau Ceti roadmap status: Geometric measure theory: rectifiability, BV, and finite perimeter

LeanTauCeti.exists_regular_lineDeriv_ofFun_apply_eq

Uses 1 · Used by 2

Statement usesTauCeti.totalVariationOn

Used byLebesgue decomposition of the BV derivative · The Gauss–Green formula, Dχ_s = -ν_s |Dχ_s|

TheoremBanach indicatrix inequality#

The variation of a continuous curve on [a, b] is at most the raw one-dimensional Hausdorff integral of the extended cardinality of its fibers. No injectivity or rectifiability hypothesis is needed; repeated traversals are counted by the fiber cardinality.

ContinuousOn.eVariationOn_le_lintegral_encard.{u_1} {X : Type u_1} [EMetricSpace X]
  [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) :
  eVariationOn γ (Set.Icc a b) ≤
    ∫⁻ (y : X), ↑(Set.Icc a b ∩ γ ⁻¹' {y}).encard ∂MeasureTheory.Measure.hausdorffMeasure 1

Lean

Formalized in Tau Ceti as ContinuousOn.eVariationOn_le_lintegral_encard.

Sources

• Tau Ceti documentation: ContinuousOn.eVariationOn_le_lintegral_encard
• Source of ContinuousOn.eVariationOn_le_lintegral_encard in TauCeti/Topology/EMetricSpace/CurveLength.lean

LeanContinuousOn.eVariationOn_le_lintegral_encard

Used by 1

Used byBanach indicatrix formula

TheoremThe sharp BV Sobolev bound#

In dimension n ≥ 2, every integrable real-valued function satisfies ‖u‖ₚ ≤ (n ωₙ^(1/n))⁻¹ |Du|(E) for p = n / (n - 1). The total variation may be infinite.

TauCeti.eLpNorm_le_inv_mul_totalVariationOn.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {u : E → ℝ}
  {p : NNReal} (hu : MeasureTheory.Integrable u MeasureTheory.volume)
  (hp : (↑(Module.finrank ℝ E)).HolderConjugate p) :
  MeasureTheory.eLpNorm u (↑p) MeasureTheory.volume ≤
    (ENNReal.ofReal
          (↑(Module.finrank ℝ E) *
            MeasureTheory.volume.real (Metric.ball 0 1) ^ (↑(Module.finrank ℝ E))⁻¹))⁻¹ *
      TauCeti.totalVariationOn MeasureTheory.volume ⊤ u

Lean

Formalized in Tau Ceti as TauCeti.eLpNorm_le_inv_mul_totalVariationOn.

Sources

• Tau Ceti documentation: TauCeti.eLpNorm_le_inv_mul_totalVariationOn
• Source of TauCeti.eLpNorm_le_inv_mul_totalVariationOn in TauCeti/Analysis/BoundedVariation/Sobolev/Sharp.lean

LeanTauCeti.eLpNorm_le_inv_mul_totalVariationOn

Uses 7

Statement usesTauCeti.totalVariationOn

Proof usesBrunn–Minkowski for a shell · The coarea formula for total variation · Minkowski's integral inequality · The Morse--Sard theorem · Rademacher's theorem for locally Lipschitz functions · TauCeti.perimeter

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.