Documentation

Mathlib.MeasureTheory.Measure.Stieltjes

Stieltjes measures on the real line #

Consider a function f : ℝ → ℝ which is monotone and right-continuous. Then one can define a corresponding measure, giving mass f b - f a to the interval (a, b].

Main definitions #

Basic properties of Stieltjes functions #

Bundled monotone right-continuous real functions, used to construct Stieltjes measures.

Instances For
    theorem StieltjesFunction.ext_iff {f : StieltjesFunction} {g : StieltjesFunction} :
    f = g ∀ (x : ), f x = g x
    theorem StieltjesFunction.ext {f : StieltjesFunction} {g : StieltjesFunction} (h : ∀ (x : ), f x = g x) :
    f = g
    theorem StieltjesFunction.iInf_Ioi_eq (f : StieltjesFunction) (x : ) :
    ⨅ (r : (Set.Ioi x)), f r = f x
    theorem StieltjesFunction.iInf_rat_gt_eq (f : StieltjesFunction) (x : ) :
    ⨅ (r : { r' : // x < r' }), f r = f x

    The identity of as a Stieltjes function, used to construct Lebesgue measure.

    Equations
    Instances For

      Constant functions are Stieltjes function.

      Equations
      Instances For
        @[simp]

        The sum of two Stieltjes functions is a Stieltjes function.

        Equations
        • f.add g = { toFun := fun (x : ) => f x + g x, mono' := , right_continuous' := }
        Instances For
          @[simp]
          theorem StieltjesFunction.add_apply (f : StieltjesFunction) (g : StieltjesFunction) (x : ) :
          (f + g) x = f x + g x
          noncomputable def Monotone.stieltjesFunction {f : } (hf : Monotone f) :

          If a function f : ℝ → ℝ is monotone, then the function mapping x to the right limit of f at x is a Stieltjes function, i.e., it is monotone and right-continuous.

          Equations
          • hf.stieltjesFunction = { toFun := Function.rightLim f, mono' := , right_continuous' := }
          Instances For
            theorem Monotone.stieltjesFunction_eq {f : } (hf : Monotone f) (x : ) :
            hf.stieltjesFunction x = Function.rightLim f x

            The outer measure associated to a Stieltjes function #

            Length of an interval. This is the largest monotone function which correctly measures all intervals.

            Equations
            Instances For
              @[simp]
              theorem StieltjesFunction.length_Ioc (f : StieltjesFunction) (a : ) (b : ) :
              f.length (Set.Ioc a b) = ENNReal.ofReal (f b - f a)
              theorem StieltjesFunction.length_mono (f : StieltjesFunction) {s₁ : Set } {s₂ : Set } (h : s₁ s₂) :
              f.length s₁ f.length s₂

              The Stieltjes outer measure associated to a Stieltjes function.

              Equations
              Instances For
                theorem StieltjesFunction.outer_le_length (f : StieltjesFunction) (s : Set ) :
                f.outer s f.length s
                theorem StieltjesFunction.length_subadditive_Icc_Ioo (f : StieltjesFunction) {a : } {b : } {c : } {d : } (ss : Set.Icc a b ⋃ (i : ), Set.Ioo (c i) (d i)) :
                ENNReal.ofReal (f b - f a) ∑' (i : ), ENNReal.ofReal (f (d i) - f (c i))

                If a compact interval [a, b] is covered by a union of open interval (c i, d i), then f b - f a ≤ ∑ f (d i) - f (c i). This is an auxiliary technical statement to prove the same statement for half-open intervals, the point of the current statement being that one can use compactness to reduce it to a finite sum, and argue by induction on the size of the covering set.

                @[simp]
                theorem StieltjesFunction.outer_Ioc (f : StieltjesFunction) (a : ) (b : ) :
                f.outer (Set.Ioc a b) = ENNReal.ofReal (f b - f a)
                theorem StieltjesFunction.outer_trim (f : StieltjesFunction) :
                f.outer.trim = f.outer

                The measure associated to a Stieltjes function #

                @[irreducible]

                The measure associated to a Stieltjes function, giving mass f b - f a to the interval (a, b].

                Equations
                Instances For
                  theorem StieltjesFunction.measure_def (f : StieltjesFunction) :
                  f.measure = { toOuterMeasure := f.outer, m_iUnion := , trim_le := }
                  @[simp]
                  theorem StieltjesFunction.measure_Ioc (f : StieltjesFunction) (a : ) (b : ) :
                  f.measure (Set.Ioc a b) = ENNReal.ofReal (f b - f a)
                  @[simp]
                  theorem StieltjesFunction.measure_singleton (f : StieltjesFunction) (a : ) :
                  f.measure {a} = ENNReal.ofReal (f a - Function.leftLim (↑f) a)
                  @[simp]
                  theorem StieltjesFunction.measure_Icc (f : StieltjesFunction) (a : ) (b : ) :
                  f.measure (Set.Icc a b) = ENNReal.ofReal (f b - Function.leftLim (↑f) a)
                  @[simp]
                  theorem StieltjesFunction.measure_Ioo (f : StieltjesFunction) {a : } {b : } :
                  f.measure (Set.Ioo a b) = ENNReal.ofReal (Function.leftLim (↑f) b - f a)
                  @[simp]
                  theorem StieltjesFunction.measure_Ico (f : StieltjesFunction) (a : ) (b : ) :
                  f.measure (Set.Ico a b) = ENNReal.ofReal (Function.leftLim (↑f) b - Function.leftLim (↑f) a)
                  theorem StieltjesFunction.measure_Iic (f : StieltjesFunction) {l : } (hf : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (x : ) :
                  f.measure (Set.Iic x) = ENNReal.ofReal (f x - l)
                  theorem StieltjesFunction.measure_Ici (f : StieltjesFunction) {l : } (hf : Filter.Tendsto (↑f) Filter.atTop (nhds l)) (x : ) :
                  f.measure (Set.Ici x) = ENNReal.ofReal (l - Function.leftLim (↑f) x)
                  theorem StieltjesFunction.measure_univ (f : StieltjesFunction) {l : } {u : } (hfl : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (hfu : Filter.Tendsto (↑f) Filter.atTop (nhds u)) :
                  f.measure Set.univ = ENNReal.ofReal (u - l)
                  theorem StieltjesFunction.isFiniteMeasure (f : StieltjesFunction) {l : } {u : } (hfl : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (hfu : Filter.Tendsto (↑f) Filter.atTop (nhds u)) :
                  theorem StieltjesFunction.isProbabilityMeasure (f : StieltjesFunction) (hf_bot : Filter.Tendsto (↑f) Filter.atBot (nhds 0)) (hf_top : Filter.Tendsto (↑f) Filter.atTop (nhds 1)) :
                  theorem StieltjesFunction.eq_of_measure_of_tendsto_atBot (f : StieltjesFunction) (g : StieltjesFunction) {l : } (hfg : f.measure = g.measure) (hfl : Filter.Tendsto (↑f) Filter.atBot (nhds l)) (hgl : Filter.Tendsto (↑g) Filter.atBot (nhds l)) :
                  f = g
                  theorem StieltjesFunction.eq_of_measure_of_eq (f : StieltjesFunction) (g : StieltjesFunction) {y : } (hfg : f.measure = g.measure) (hy : f y = g y) :
                  f = g
                  @[simp]
                  theorem StieltjesFunction.measure_add (f : StieltjesFunction) (g : StieltjesFunction) :
                  (f + g).measure = f.measure + g.measure
                  @[simp]
                  theorem StieltjesFunction.measure_smul (c : NNReal) (f : StieltjesFunction) :
                  (c f).measure = c f.measure