noncomputable def LowerUnsignedLebesgueIntegral {d : ℕ} (f : EuclideanSpace' d → EReal) : EReal

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}

noncomputable def UpperUnsignedLebesgueIntegral {d : ℕ} (f : EuclideanSpace' d → EReal) : EReal

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}

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) : LowerUnsignedLebesgueIntegral f = hf.integ

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) : LowerUnsignedLebesgueIntegral f ≤ LowerUnsignedLebesgueIntegral g

Exercise 1.3.10(ii) (Monotonicity)

theorem LowerUnsignedLebesgueIntegral.hom {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) {c : ℝ} (hc : 0 ≤ c) : LowerUnsignedLebesgueIntegral (↑c • f) = ↑c * LowerUnsignedLebesgueIntegral f

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) : LowerUnsignedLebesgueIntegral f = LowerUnsignedLebesgueIntegral g

Exercise 1.3.10(iv) (Equivalence)

theorem LowerUnsignedLebesgueIntegral.superadditive {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) (hg : UnsignedMeasurable g) : LowerUnsignedLebesgueIntegral (f + g) ≥ LowerUnsignedLebesgueIntegral f + LowerUnsignedLebesgueIntegral g

Exercise 1.3.10(v) (Superadditivity)

theorem UpperUnsignedLebesgueIntegral.subadditive {d : ℕ} {f g : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) (hg : UnsignedMeasurable g) : UpperUnsignedLebesgueIntegral (f + g) ≤ UpperUnsignedLebesgueIntegral f + UpperUnsignedLebesgueIntegral 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 : LebesgueMeasurable E) : LowerUnsignedLebesgueIntegral f = LowerUnsignedLebesgueIntegral (f * Real.toEReal ∘ E.indicator') + LowerUnsignedLebesgueIntegral (f * Real.toEReal ∘ Eᶜ.indicator')

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

• UpperUnsignedLebesgueIntegral.eq_lim_vert_trunc = sorry

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

• UpperUnsignedLebesgueIntegral.eq_lim_horiz_trunc = sorry

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)) : hfg.integ = LowerUnsignedLebesgueIntegral f + LowerUnsignedLebesgueIntegral g

Exercise 1.3.10(x) (Reflection)

noncomputable def UnsignedLebesgueIntegral {d : ℕ} (f : EuclideanSpace' d → EReal) : EReal

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

• UnsignedLebesgueIntegral f = LowerUnsignedLebesgueIntegral f

noncomputable def UnsignedMeasurable.integ {d : ℕ} (f : EuclideanSpace' d → EReal) : UnsignedMeasurable f → EReal

Equations

• UnsignedMeasurable.integ f x✝ = UnsignedLebesgueIntegral f

theorem LowerUnsignedLebesgueIntegral.eq_upperIntegral {d : ℕ} {f : EuclideanSpace' d → EReal} (hf : UnsignedMeasurable f) (hbound : EReal.BoundedFunction f) (hsupp : FiniteMeasureSupport f) : LowerUnsignedLebesgueIntegral f = UpperUnsignedLebesgueIntegral 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

• LowerUnsignedLebesgueIntegral.eq_upperIntegral_unbounded = sorry

def LowerUnsignedLebesgueIntegral.eq_upperIntegral_infinite_supp : Decidable (∀ (d : ℕ) (f : EuclideanSpace' d → EReal), UnsignedMeasurable f → EReal.BoundedFunction f → LowerUnsignedLebesgueIntegral f = UpperUnsignedLebesgueIntegral f)

Equations

• LowerUnsignedLebesgueIntegral.eq_upperIntegral_infinite_supp = sorry

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) : LowerUnsignedLebesgueIntegral (f + g) = LowerUnsignedLebesgueIntegral f + LowerUnsignedLebesgueIntegral 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)) : LowerUnsignedLebesgueIntegral (f + g) = LowerUnsignedLebesgueIntegral f + LowerUnsignedLebesgueIntegral g

Corollary 1.3.14 (Finite additivity of Lebesgue integral ).

theorem UpperUnsignedLebesgueIntegral.eq_outer_measure_integral {d : ℕ} {E : Set (EuclideanSpace' d)} (hE : LebesgueMeasurable E) : UpperUnsignedLebesgueIntegral (Real.toEReal ∘ E.indicator') = Lebesgue_outer_measure 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) : (UnsignedLebesgueIntegral fun (x : EuclideanSpace' d) => f (x + a)) = UnsignedMeasurable.integ f hf

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) : Lebesgue_measure {x : EuclideanSpace' d | f x ≥ ↑t} ≤ UnsignedMeasurable.integ f hf / ↑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) : UnsignedMeasurable.integ f hf = 0 ↔ AlmostAlways fun (x : EuclideanSpace' d) => f x = 0

Exercise 1.3.18 (iii)