Introduction to Measure Theory, Section 1.3.3: Unsigned Lebesgue integrals #
A companion to (the introduction to) Section 1.3.3 of the book "An introduction to Measure Theory".
Definition 1.3.12 (Lower unsigned Lebesgue integral)
Equations
- LowerUnsignedLebesgueIntegral f = sSup {R : EReal | ∃ (g : EuclideanSpace' d → EReal) (hg : UnsignedSimpleFunction g), ∀ (x : EuclideanSpace' d), g x ≤ f x ∧ R = hg.integ}
Instances For
Definition 1.3.12 (Upper unsigned Lebesgue integral)
Equations
- UpperUnsignedLebesgueIntegral f = sInf {R : EReal | ∃ (g : EuclideanSpace' d → EReal) (hg : UnsignedSimpleFunction g), ∀ (x : EuclideanSpace' d), g x ≥ f x ∧ R = hg.integ}
Instances For
theorem
LowerUnsignedLebesgueIntegral.eq
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : ∀ (x : EuclideanSpace' d), 0 ≤ f x)
:
LowerUnsignedLebesgueIntegral f = sSup
{R : EReal | ∃ (g : EuclideanSpace' d → EReal) (hg : UnsignedSimpleFunction g),
(AlmostAlways fun (x : EuclideanSpace' d) => g x ≤ f x) ∧ R = hg.integ}
theorem
LowerUnsignedLebesgueIntegral.eq_simpleIntegral
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedSimpleFunction f)
:
Exercise 1.3.10(i) (Compatibility with the simple integral)
theorem
LowerUnsignedLebesgueIntegral.mono
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
(hfg : AlmostAlways fun (x : EuclideanSpace' d) => f x ≤ g x)
:
Exercise 1.3.10(ii) (Monotonicity)
theorem
LowerUnsignedLebesgueIntegral.hom
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
{c : ℝ}
(hc : 0 ≤ c)
:
Exercise 1.3.10(iii) (Homogeneity)
theorem
LowerUnsignedLebesgueIntegral.integral_eq_integral_of_aeEqual
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
(heq : AlmostEverywhereEqual f g)
:
Exercise 1.3.10(iv) (Equivalence)
theorem
LowerUnsignedLebesgueIntegral.superadditive
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
:
Exercise 1.3.10(v) (Superadditivity)
theorem
UpperUnsignedLebesgueIntegral.subadditive
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
:
Exercise 1.3.10(vi) (Subadditivity of upper integral)
theorem
LowerUnsignedLebesgueIntegral.eq_add
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
{E : Set (EuclideanSpace' d)}
(hE : MeasurableSet E)
:
Exercise 1.3.10(vii) (Divisibility)
theorem
LowerUnsignedLebesgueIntegral.eq_lim_vert_trunc
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
:
Filter.Tendsto (fun (n : ℕ) => LowerUnsignedLebesgueIntegral fun (x : EuclideanSpace' d) => min (f x) ↑n) Filter.atTop
(nhds (LowerUnsignedLebesgueIntegral f))
Exercise 1.3.10(viii) (Vertical truncation)
def
UpperUnsignedLebesgueIntegral.eq_lim_vert_trunc :
Decidable
(∀ (d : ℕ) (f : EuclideanSpace' d → EReal),
UnsignedMeasurable f →
Filter.Tendsto (fun (n : ℕ) => UpperUnsignedLebesgueIntegral fun (x : EuclideanSpace' d) => min (f x) ↑n)
Filter.atTop (nhds (UpperUnsignedLebesgueIntegral f)))
Equations
Instances For
theorem
LowerUnsignedLebesgueIntegral.eq_lim_horiz_trunc
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
:
Filter.Tendsto (fun (n : ℕ) => LowerUnsignedLebesgueIntegral (f * Real.toEReal ∘ (Metric.ball 0 ↑n).indicator'))
Filter.atTop (nhds (LowerUnsignedLebesgueIntegral f))
Exercise 1.3.10(ix) (Horizontal truncation)
def
UpperUnsignedLebesgueIntegral.eq_lim_horiz_trunc :
Decidable
(∀ (d : ℕ) (f : EuclideanSpace' d → EReal),
UnsignedMeasurable f →
Filter.Tendsto (fun (n : ℕ) => UpperUnsignedLebesgueIntegral (f * Real.toEReal ∘ (Metric.ball 0 ↑n).indicator'))
Filter.atTop (nhds (UpperUnsignedLebesgueIntegral f)))
Equations
Instances For
theorem
LowerUnsignedLebesgueIntegral.sum_of_reflect_eq
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
(hfg : UnsignedSimpleFunction (f + g))
(hbound : EReal.BoundedFunction (f + g))
(hsupport : FiniteMeasureSupport (f + g))
:
Exercise 1.3.10(x) (Reflection)
Definition 1.3.13 (Unsigned Lebesgue integral). For Lean purposes it is convenient to assign a "junk" value to this integral when f is not unsigned measurable.
Equations
Instances For
Equations
Instances For
theorem
LowerUnsignedLebesgueIntegral.eq_upperIntegral
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hbound : EReal.BoundedFunction f)
(hsupp : FiniteMeasureSupport f)
:
Exercise 1.3.11
def
LowerUnsignedLebesgueIntegral.eq_upperIntegral_unbounded :
Decidable
(∀ (d : ℕ) (f : EuclideanSpace' d → EReal),
UnsignedMeasurable f → FiniteMeasureSupport f → LowerUnsignedLebesgueIntegral f = UpperUnsignedLebesgueIntegral f)
Equations
Instances For
def
LowerUnsignedLebesgueIntegral.eq_upperIntegral_infinite_supp :
Decidable
(∀ (d : ℕ) (f : EuclideanSpace' d → EReal),
UnsignedMeasurable f → EReal.BoundedFunction f → LowerUnsignedLebesgueIntegral f = UpperUnsignedLebesgueIntegral f)
Equations
Instances For
theorem
UnsignedMeasurable.mul_indicator_ball
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(n : ℕ)
:
UnsignedMeasurable (f * Real.toEReal ∘ (Metric.ball 0 ↑n).indicator')
Multiplying an unsigned measurable function by a ball indicator preserves measurability. This is a key helper for the horizontal truncation argument in Corollary 1.3.14.
theorem
FiniteMeasureSupport.mul_indicator_ball
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(n : ℕ)
:
FiniteMeasureSupport (f * Real.toEReal ∘ (Metric.ball 0 ↑n).indicator')
Helper: horizontal truncation produces functions with finite measure support.
theorem
LowerUnsignedLebesgueIntegral.add_of_finiteSupport
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
(hfg : UnsignedMeasurable (f + g))
(hf_supp : FiniteMeasureSupport f)
(hg_supp : FiniteMeasureSupport g)
:
Additivity of lower integral for finite-support functions. This is the key step where we can apply eq_upperIntegral and use the sandwich argument.
theorem
LowerUnsignedLebesgueIntegral.add
{d : ℕ}
{f g : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hg : UnsignedMeasurable g)
(hfg : UnsignedMeasurable (f + g))
:
Corollary 1.3.14 (Finite additivity of Lebesgue integral )
theorem
UpperUnsignedLebesgueIntegral.eq_outer_measure_integral
{d : ℕ}
{E : Set (EuclideanSpace' d)}
(hE : MeasurableSet E)
:
Exercise 1.3.12 (Upper Lebesgue integral and outer measure)
theorem
LowerUnsignedLebesgueIntegral.not_additive :
∃ (d : ℕ) (f : EuclideanSpace' d → EReal) (g : EuclideanSpace' d → EReal) (_ : Unsigned f) (_ : Unsigned g),
LowerUnsignedLebesgueIntegral (f + g) ≠ LowerUnsignedLebesgueIntegral f + LowerUnsignedLebesgueIntegral g
theorem
UpperUnsignedLebesgueIntegral.not_additive :
∃ (d : ℕ) (f : EuclideanSpace' d → EReal) (g : EuclideanSpace' d → EReal) (_ : Unsigned f) (_ : Unsigned g),
UpperUnsignedLebesgueIntegral (f + g) ≠ UpperUnsignedLebesgueIntegral f + UpperUnsignedLebesgueIntegral g
theorem
LowerUnsignedLebesgueIntegral.eq_area
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
:
LowerUnsignedLebesgueIntegral f = Lebesgue_measure
{p : EuclideanSpace' (d + 1) | ∃ (x : EuclideanSpace' d) (t : ℝ),
(EuclideanSpace'.prod_equiv d 1) p = (x, Real.equiv_EuclideanSpace' t) ∧ 0 ≤ t ∧ ↑t ≤ f x}
Exercise 1.3.13 (Area interpretation of integral)
theorem
UnsignedLebesgueIntegral.unique
{d : ℕ}
(integ : (EuclideanSpace' d → EReal) → EReal)
(hsimple : ∀ (f : EuclideanSpace' d → EReal) (hf : UnsignedSimpleFunction f), integ f = hf.integ)
(hadd :
∀ (f g : EuclideanSpace' d → EReal), UnsignedMeasurable f → UnsignedMeasurable g → integ (f + g) = integ f + integ g)
(hvert :
∀ (f : EuclideanSpace' d → EReal),
UnsignedMeasurable f →
Filter.Tendsto (fun (n : ℕ) => integ fun (x : EuclideanSpace' d) => min (f x) ↑n) Filter.atTop (nhds (integ f)))
(hhoriz :
∀ (f : EuclideanSpace' d → EReal),
UnsignedMeasurable f →
Filter.Tendsto (fun (n : ℕ) => integ (f * Real.toEReal ∘ (Metric.ball 0 ↑n).indicator')) Filter.atTop
(nhds (integ f)))
(f : EuclideanSpace' d → EReal)
:
UnsignedMeasurable f → integ f = UnsignedLebesgueIntegral f
Exercise 1.3.14 (Uniqueness)
theorem
UnsignedLebesgueIntegral.trans
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(a : EuclideanSpace' d)
:
Exercise 1.3.15 (Translation invariance)
theorem
UnsignedLebesgueIntegral.comp_linear
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(A : EuclideanSpace' d →ₗ[ℝ] EuclideanSpace' d)
(hA : LinearMap.det A ≠ 0)
:
(UnsignedLebesgueIntegral fun (x : EuclideanSpace' d) => f (A x)) = ↑|LinearMap.det A|⁻¹ * UnsignedMeasurable.integ f hf
Exercise 1.3.16 (Linear change of variables)
theorem
RiemannIntegral.eq_UnsignedLebesgueIntegral
{I : BoundedInterval}
{f : ℝ → ℝ}
(hf : RiemannIntegrableOn f I)
:
↑(riemannIntegral f I) = UnsignedLebesgueIntegral (Real.toEReal ∘ (fun (x : ℝ) => f x * (↑I).indicator' x) ∘ ⇑EuclideanSpace'.equiv_Real)
Exercise 1.3.17 (Compatibility with the Riemann integral)
theorem
UnsignedLebesgueIntegral.markov_inequality
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
{t : ℝ}
(ht : 0 < t)
:
Lemma 1.3.15 (Markov's inequality)
theorem
UnsignedLebesgueIntegral.ae_finite
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
(hfin : UnsignedLebesgueIntegral f < ⊤)
:
AlmostAlways fun (x : EuclideanSpace' d) => f x < ⊤
Exercise 1.3.18 (ii)
theorem
UnsignedLebesgueIntegral.ae_finite_no_converse :
∃ (d : ℕ) (f : EuclideanSpace' d → EReal) (_ : UnsignedMeasurable f) (_ :
AlmostAlways fun (x : EuclideanSpace' d) => f x < ⊤), UnsignedLebesgueIntegral f = ⊤
theorem
UnsignedLebesgueIntegral.eq_zero_aeZero
{d : ℕ}
{f : EuclideanSpace' d → EReal}
(hf : UnsignedMeasurable f)
:
Exercise 1.3.18 (ii)