Documentation

TauCeti.Analysis.BoundedVariation.Space

The Banach space of functions of bounded variation #

TauCeti.MemBV μ Ω u means that u is integrable on Ω and its variational total variation is finite. TauCeti.BV μ Ω is the corresponding space of almost-everywhere classes, with norm ‖u‖₁ + |Du|(Ω). It is built from Mathlib's L¹ space, so equality is equality almost everywhere on the domain, rather than equality of representatives.

The BV norm is complete, and the inclusion into L¹ is a continuous injective linear map. The domain and measure are parameters; total variation is defined by duality relative to this measure. For additive Haar measures this is the classical distributional variation. In particular the construction applies to Lebesgue measure on any open subset of a finite-dimensional real inner product space.

References #

L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §3.1.

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

A function is globally of bounded variation on Ω when it is integrable there and has finite variational total variation.

Instances For
    source
    theorem TauCeti.memBV_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} :
    MemBV μ Ω u ↔ MeasureTheory.IntegrableOn u (↑Ω) μ ∧ totalVariationOn μ Ω u < ⊤

    The integrability and finite-variation characterization of BV membership.

    source
    theorem TauCeti.MemBV.integrableOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MemBV μ Ω u) :
    MeasureTheory.IntegrableOn u (↑Ω) μ

    A BV function is integrable on its domain.

    source
    theorem TauCeti.MemBV.totalVariationOn_lt_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MemBV μ Ω u) :
    totalVariationOn μ Ω u < ⊤

    A BV function has finite total variation on its domain.

    source
    theorem TauCeti.MemBV.mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω U : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MemBV μ Ω u) (hU : U ≤ Ω) :
    MemBV μ U u

    Restriction to an open subset preserves BV membership.

    source
    theorem TauCeti.memBV_congr_ae {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u v : E → ℝ} (h : u =ᵐ[μ.restrict ↑Ω] v) :
    MemBV μ Ω u ↔ MemBV μ Ω v

    BV membership is unchanged by equality almost everywhere on the domain.

    source
    @[simp]
    theorem TauCeti.MemBV.zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} :
    MemBV μ Ω 0

    The zero function belongs to BV.

    source
    theorem TauCeti.MemBV.neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MemBV μ Ω u) :
    MemBV μ Ω (-u)

    Negation preserves BV membership.

    source
    @[simp]
    theorem TauCeti.memBV_neg_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} :
    MemBV μ Ω (-u) ↔ MemBV μ Ω u

    BV membership is unchanged by negation.

    source
    theorem TauCeti.MemBV.smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → ℝ} (hu : MemBV μ Ω u) (c : ℝ) :
    MemBV μ Ω (c • u)

    Multiplication by a real scalar preserves BV membership.

    source
    theorem TauCeti.MemBV.add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] {u v : E → ℝ} (hu : MemBV μ Ω u) (hv : MemBV μ Ω v) :
    MemBV μ Ω (u + v)

    The sum of two BV functions belongs to BV.

    source
    theorem TauCeti.MemBV.sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] {u v : E → ℝ} (hu : MemBV μ Ω u) (hv : MemBV μ Ω v) :
    MemBV μ Ω (u - v)

    The difference of two BV functions belongs to BV.

    source
    def TauCeti.bvSubmodule {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) (Ω : TopologicalSpace.Opens E) :
    Submodule ℝ ↥(MeasureTheory.Lp ℝ 1 (μ.restrict ↑Ω))

    The submodule of L¹(Ω) consisting of classes of finite total variation. Its inherited L¹ norm is distinct from the BV norm on BV μ Ω.

    Instances For
      source
      structure TauCeti.BV {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : MeasureTheory.Measure E) (Ω : TopologicalSpace.Opens E) :
      Type u_1

      Almost-everywhere classes of integrable functions with finite total variation on Ω. The wrapper gives this space its BV norm, independently of the weaker inherited L¹ norm.

      • toSubmodule : ↥(bvSubmodule μ Ω)

        The underlying finite-variation L¹ class.

      Instances For
        source
        @[simp]
        theorem TauCeti.mem_bvSubmodule_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : ↥(MeasureTheory.Lp ℝ 1 (μ.restrict ↑Ω))) :
        u ∈ bvSubmodule μ Ω ↔ totalVariationOn μ Ω ↑↑u < ⊤

        Membership in the finite-variation submodule is finiteness of total variation.

        source
        def TauCeti.BV.toL1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
        ↥(MeasureTheory.Lp ℝ 1 (μ.restrict ↑Ω))

        The underlying L¹ class of a BV function.

        Instances For
          source
          @[instance_reducible]
          noncomputable instance TauCeti.BV.instCoeFunForallReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
          CoeFun (BV μ Ω) fun (x : BV μ Ω) => E → ℝ
          source
          theorem TauCeti.BV.toL1_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
          Function.Injective toL1

          BV classes are determined by their L¹ classes.

          source
          theorem TauCeti.BV.ext {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] {u v : BV μ Ω} (h : ↑↑u.toL1 =ᵐ[μ.restrict ↑Ω] ↑↑v.toL1) :
          u = v

          Equality of BV classes is equality almost everywhere on Ω.

          source
          theorem TauCeti.BV.ext_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] {u v : BV μ Ω} :
          u = v ↔ ↑↑u.toL1 =ᵐ[μ.restrict ↑Ω] ↑↑v.toL1
          source
          theorem TauCeti.BV.integrableOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
          MeasureTheory.IntegrableOn (↑↑u.toL1) (↑Ω) μ

          Every representative selected from a BV class is integrable on its domain.

          source
          theorem TauCeti.BV.totalVariationOn_lt_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
          totalVariationOn μ Ω ↑↑u.toL1 < ⊤

          Every BV class has finite total variation.

          source
          theorem TauCeti.BV.memBV {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
          MemBV μ Ω ↑↑u.toL1

          The selected representative of a BV class belongs to the unbundled BV predicate.

          source
          noncomputable def TauCeti.BV.ofFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : E → ℝ) (hu : MemBV μ Ω u) :
          BV μ Ω

          Form the almost-everywhere class of an integrable function of finite variation.

          Instances For
            source
            theorem TauCeti.BV.toL1_ofFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : E → ℝ) (hu : MemBV μ Ω u) :
            (ofFunction u hu).toL1 = MeasureTheory.Integrable.toL1 u ⋯

            The L¹ class of the BV class constructed from a function.

            source
            theorem TauCeti.BV.coeFn_ofFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : E → ℝ) (hu : MemBV μ Ω u) :
            ↑↑(ofFunction u hu).toL1 =ᵐ[μ.restrict ↑Ω] u

            Forming a BV class preserves the function almost everywhere on Ω.

            source
            @[simp]
            theorem TauCeti.BV.totalVariationOn_ofFunction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : E → ℝ) (hu : MemBV μ Ω u) :
            totalVariationOn μ Ω ↑↑(ofFunction u hu).toL1 = totalVariationOn μ Ω u

            Construction of a BV class preserves its total variation.

            source
            @[simp]
            theorem TauCeti.BV.ofFunction_coeFn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
            ofFunction ↑↑u.toL1 ⋯ = u

            Reconstructing a BV class from its representative gives the original class.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instZero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            Zero (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instAdd {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            Add (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instNeg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            Neg (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instSub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            Sub (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instSMulReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            SMul ℝ (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instSMulNat {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            SMul ℕ (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instSMulInt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            SMul ℤ (BV μ Ω)
            source
            @[simp]
            theorem TauCeti.BV.toL1_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            toL1 0 = 0
            source
            @[simp]
            theorem TauCeti.BV.toL1_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u v : BV μ Ω) :
            (u + v).toL1 = u.toL1 + v.toL1
            source
            @[simp]
            theorem TauCeti.BV.toL1_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
            (-u).toL1 = -u.toL1
            source
            @[simp]
            theorem TauCeti.BV.toL1_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u v : BV μ Ω) :
            (u - v).toL1 = u.toL1 - v.toL1
            source
            @[simp]
            theorem TauCeti.BV.toL1_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (c : ℝ) (u : BV μ Ω) :
            (c • u).toL1 = c • u.toL1
            source
            @[simp]
            theorem TauCeti.BV.toL1_nsmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (c : ℕ) (u : BV μ Ω) :
            (c • u).toL1 = c • u.toL1
            source
            @[simp]
            theorem TauCeti.BV.toL1_zsmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (c : ℤ) (u : BV μ Ω) :
            (c • u).toL1 = c • u.toL1
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instAddCommGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            AddCommGroup (BV μ Ω)
            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instModuleReal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            Module ℝ (BV μ Ω)
            source
            theorem TauCeti.BV.coeFn_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            ↑↑(toL1 0) =ᵐ[μ.restrict ↑Ω] 0

            The zero BV class is represented by zero almost everywhere.

            source
            theorem TauCeti.BV.coeFn_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
            ↑↑(-u).toL1 =ᵐ[μ.restrict ↑Ω] -↑↑u.toL1

            Negation of a BV class negates its representative almost everywhere.

            source
            theorem TauCeti.BV.coeFn_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u v : BV μ Ω) :
            ↑↑(u - v).toL1 =ᵐ[μ.restrict ↑Ω] ↑↑u.toL1 - ↑↑v.toL1

            Subtraction of BV classes subtracts their representatives almost everywhere.

            source
            theorem TauCeti.BV.coeFn_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u v : BV μ Ω) :
            ↑↑(u + v).toL1 =ᵐ[μ.restrict ↑Ω] ↑↑u.toL1 + ↑↑v.toL1

            The representative of a sum is almost everywhere the sum of the representatives.

            source
            theorem TauCeti.BV.coeFn_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (c : ℝ) (u : BV μ Ω) :
            ↑↑(c • u).toL1 =ᵐ[μ.restrict ↑Ω] c • ↑↑u.toL1

            The representative of a scalar multiple is almost everywhere the scaled representative.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instNorm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            Norm (BV μ Ω)

            The BV norm is the sum of the L¹ norm and the real-valued total variation.

            source
            theorem TauCeti.BV.norm_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
            ‖u‖ = ‖u.toL1‖ + (totalVariationOn μ Ω ↑↑u.toL1).toReal

            The characteristic formula for the BV norm.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instNormedAddCommGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            NormedAddCommGroup (BV μ Ω)

            The L¹-plus-variation norm makes BV a normed additive commutative group.

            source
            @[instance_reducible]
            noncomputable instance TauCeti.BV.instNormedSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            NormedSpace ℝ (BV μ Ω)

            BV is a normed real vector space for its L¹-plus-variation norm.

            source
            theorem TauCeti.BV.norm_toL1_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
            ‖u.toL1‖ ≤ ‖u‖

            The inclusion into L¹ decreases the norm.

            source
            noncomputable def TauCeti.BV.toL1CLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
            BV μ Ω →L[ℝ] ↥(MeasureTheory.Lp ℝ 1 (μ.restrict ↑Ω))

            Forgetting finite variation gives a continuous linear inclusion into L¹(Ω).

            Instances For
              source
              @[simp]
              theorem TauCeti.BV.toL1CLM_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] (u : BV μ Ω) :
              toL1CLM u = u.toL1
              source
              theorem TauCeti.BV.toL1CLM_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
              Function.Injective ⇑toL1CLM

              The continuous linear inclusion into L¹ is injective.

              source
              instance TauCeti.BV.instCompleteSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} [OpensMeasurableSpace E] :
              CompleteSpace (BV μ Ω)

              The BV norm is complete: every Cauchy sequence for the sum of the L¹ norm and total variation converges in that norm.