Bounded Variation

Results named in Tau Ceti's TauCeti.Analysis.BoundedVariation modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Gauss–Green formula, Dχ_s = -ν_s |Dχ_s|#

For a set s of locally finite perimeter in Ω, the outer normal ν_s represents the distributional derivative of the indicator against the perimeter measure: ∫_s div φ dμ = ∫ ⟪φ, ν_s⟫ d|Dχ_s| for every C¹ vector field φ with compact support in Ω, where div φ = tr (Dφ).

TauCeti.integral_trace_fderiv_mul_indicator_eq_integral_inner_outerNormal.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {s : Set E}
  (hu : MeasureTheory.LocallyIntegrableOn (s.indicator 1) (↑Ω) μ)
  (hfin :
    ∀ (K : Set E),
      IsCompact K → K ⊆ ↑Ω → ∃ U, K ⊆ ↑U ∧ TauCeti.totalVariationOn μ U (s.indicator 1) ≠ ⊤)
  {φ : E → E} (hφ : ContDiff ℝ 1 φ) (hc : HasCompactSupport φ) (hs : tsupport φ ⊆ ↑Ω) :
  ∫ (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ φ x) * s.indicator 1 x ∂μ =
    ∫ (y : ↥Ω),
      inner ℝ (φ ↑y) (TauCeti.outerNormal μ Ω s ↑y) ∂TauCeti.variationMeasure μ Ω (s.indicator 1)
Lean

Formalized in Tau Ceti as TauCeti.integral_trace_fderiv_mul_indicator_eq_integral_inner_outerNormal.

Sources
LeanTauCeti.integral_trace_fderiv_mul_indicator_eq_integral_inner_outerNormal
Uses 3
Statement usesTauCeti.totalVariationOn
Proof usesThe directional derivatives of a function of locally finite variation are signed Radon measures · Lebesgue's differentiation theorem

TheoremLebesgue decomposition of the BV derivative#

The distributional derivative is the sum of the density acDerivativeDensity μ Ω u ν against ν and the polar field against the singular part of |Du|. Both pairings are integrable because the test field has compact support.

TauCeti.integral_divergenceCLM_mul_eq_neg_integral_inner_acDerivativeDensity_sub_singularPart.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E}
  {u : E → ℝ} (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ)
  (hfin : ∀ (K : Set E), IsCompact K → K ⊆ ↑Ω → ∃ U, K ⊆ ↑U ∧ TauCeti.totalVariationOn μ U u ≠ ⊤)
  (ν : MeasureTheory.Measure ↥Ω) [MeasureTheory.SigmaFinite ν] (φ : TestFunction Ω E ⊤) :
  ∫ (x : E), (TestFunction.divergenceCLM φ) x * u x ∂μ =
    -∫ (x : ↥Ω), inner ℝ (φ ↑x) (TauCeti.acDerivativeDensity μ Ω u ν x) ∂ν -
      ∫ (x : ↥Ω),
        inner ℝ (φ ↑x)
          (TauCeti.polarDensity μ Ω u x) ∂(TauCeti.variationMeasure μ Ω u).singularPart ν
Lean

Formalized in Tau Ceti as TauCeti.integral_divergenceCLM_mul_eq_neg_integral_inner_acDerivativeDensity_sub_singularPart.

Sources
LeanTauCeti.integral_divergenceCLM_mul_eq_neg_integral_inner_acDerivativeDensity_sub_singularPart
Uses 2
Statement usesTauCeti.totalVariationOn
Proof usesThe directional derivatives of a function of locally finite variation are signed Radon measures

TheoremThe Poincaré inequality for functions of bounded variation on a ball#

A function locally integrable on a ball of radius R in a space of dimension n deviates from its mean over the ball in L¹ by at most 2 ^ (n + 1) R times its total variation on the ball. The constant is proportional to R, as the scaling of both sides forces.

TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn_of_eq_ball.{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 → ℝ} {c : E} {R : ℝ} (hΩ : ↑Ω = Metric.ball c R)
  (hu : MeasureTheory.LocallyIntegrableOn u (Metric.ball c R) μ) :
  ∫⁻ (x : E) in Metric.ball c R, ‖u x - ⨍ (y : E) in Metric.ball c R, u y ∂μ‖ₑ ∂μ ≤
    ENNReal.ofReal (2 ^ (Module.finrank ℝ E + 1) * R) * TauCeti.totalVariationOn μ Ω u
Lean

Formalized in Tau Ceti as TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn_of_eq_ball.

Other forms

The Poincaré inequality for functions of bounded variation on a bounded convex set. Formalized in Tau Ceti as TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn_of_convex.

TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn_of_convex.{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 → ℝ} {S : Set E} (hconv : Convex ℝ ↑Ω) (hb : Bornology.IsBounded ↑Ω)
  (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hS : S ⊆ ↑Ω) (hS₀ : μ S ≠ 0) :
  ∫⁻ (x : E) in ↑Ω, ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ∂μ ≤
    ENNReal.ofReal
        (μ.real (Metric.ball 0 1) * Metric.diam ↑Ω ^ (Module.finrank ℝ E + 1) / μ.real S) *
      TauCeti.totalVariationOn μ Ω u

The Poincaré inequality for functions of bounded variation on a convex set. Formalized in Tau Ceti as TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn.

TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn.{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 → ℝ} {S : Set E} (hconv : Convex ℝ ↑Ω) (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ)
  (hS : S ⊆ ↑Ω) (hS₀ : μ S ≠ 0) (hS_top : μ S ≠ ⊤) :
  ∫⁻ (x : E) in ↑Ω, ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ∂μ ≤
    (∫⁻ (h : E) in ↑Ω - ↑Ω, ‖h‖ₑ ∂μ) / μ S * TauCeti.totalVariationOn μ Ω u
Sources
LeanTauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn_of_eq_ball · TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn_of_convex · TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_totalVariationOn
Uses 1 · Used by 1
Statement usesTauCeti.totalVariationOn
Used byThe Poincaré–Wirtinger inequality for functions of bounded variation, localized to a subset

TheoremThe Poincaré–Wirtinger inequality for functions of bounded variation, localized to a subset#

Let Ω be a bounded convex open set in a finite-dimensional real inner product space of dimension n, and let S ⊆ Ω have positive measure. For every u locally integrable on Ω and every A ⊆ Ω, the integral over A of the deviation of u from its mean over S is at most μ(B(0, 1)) ^ (1 - 1/n) * (diam Ω) ^ n / μ(S) * μ(A) ^ (1/n) times the total variation |Du|(Ω), finite or infinite.

TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_measure_rpow_mul_totalVariationOn_of_convex.{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 → ℝ} {S A : Set E} (hΩc : Convex ℝ ↑Ω)
  (hb : Bornology.IsBounded ↑Ω) (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hS : S ⊆ ↑Ω)
  (hS₀ : μ S ≠ 0) (hA : A ⊆ ↑Ω) :
  ∫⁻ (x : E) in A, ‖u x - ⨍ (y : E) in S, u y ∂μ‖ₑ ∂μ ≤
    ENNReal.ofReal
          (μ.real (Metric.ball 0 1) ^ (1 - (↑(Module.finrank ℝ E))⁻¹) *
              Metric.diam ↑Ω ^ Module.finrank ℝ E /
            μ.real S) *
        μ A ^ (↑(Module.finrank ℝ E))⁻¹ *
      TauCeti.totalVariationOn μ Ω u
Lean

Formalized in Tau Ceti as TauCeti.setLIntegral_enorm_sub_setAverage_le_mul_measure_rpow_mul_totalVariationOn_of_convex.

Sources
LeanTauCeti.setLIntegral_enorm_sub_setAverage_le_mul_measure_rpow_mul_totalVariationOn_of_convex
Uses 4
Statement usesTauCeti.totalVariationOn
Proof usesThe Poincaré inequality for functions of bounded variation on a ball · The Poincaré–Wirtinger inequality on a ball · Rademacher's theorem for locally Lipschitz functions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.