def IsAbsolutelyIntegrableOn {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : ↑Ω → EReal) : Prop

Definition 8.8: let Ω ⊆ ℝ^n be measurable. A measurable function f is absolutely integrable on Ω iff the Lebesgue integral over Ω of |f| is finite.

Equations

• IsAbsolutelyIntegrableOn Ω f = (MeasurableSet Ω ∧ Measurable f ∧ ∫⁻ (x : { x : Fin n → ℝ // x ∈ Ω }), (f x).abs ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume < ⊤)

def positiveNegativeParts {α : Type u_1} (f : α → ℝ) : (α → ℝ) × (α → ℝ)

Definition 8.9: for a real-valued function f, define its positive and negative parts by f⁺ x = max (f x) 0 and f⁻ x = -min (f x) 0.

Equations

• positiveNegativeParts f = (fun (x : α) => max (f x) 0, fun (x : α) => -min (f x) 0)

theorem helperForProposition_8_9_posPart_nonneg {α : Type u_1} (f : α → ℝ) (x : α) : 0 ≤ max (f x) 0

Helper for Proposition 8.9: the positive part max (f x) 0 is nonnegative.

theorem helperForProposition_8_9_negPart_nonneg {α : Type u_1} (f : α → ℝ) (x : α) : 0 ≤ -min (f x) 0

Helper for Proposition 8.9: the negative part -min (f x) 0 is nonnegative.

theorem helperForProposition_8_9_self_eq_posPart_sub_negPart_pointwise {α : Type u_1} (f : α → ℝ) (x : α) : f x = max (f x) 0 - -min (f x) 0

Helper for Proposition 8.9: pointwise decomposition f = f⁺ - f⁻ using max/min.

theorem helperForProposition_8_9_abs_eq_posPart_add_negPart_pointwise {α : Type u_1} (f : α → ℝ) (x : α) : |f x| = max (f x) 0 + -min (f x) 0

Helper for Proposition 8.9: pointwise decomposition |f| = f⁺ + f⁻ using max/min.

theorem proposition_8_9 {α : Type u_1} (f : α → ℝ) : (∀ (x : α), 0 ≤ max (f x) 0) ∧ (∀ (x : α), 0 ≤ -min (f x) 0) ∧ (∀ (x : α), f x = max (f x) 0 - -min (f x) 0) ∧ ∀ (x : α), |f x| = max (f x) 0 + -min (f x) 0

Proposition 8.9: for a real-valued function f, defining f⁺ x := max (f x) 0 and f⁻ x := -min (f x) 0, one has f⁺ ≥ 0, f⁻ ≥ 0, f = f⁺ - f⁻, and |f| = f⁺ + f⁻ pointwise.

noncomputable def erealPositivePart {Ω : Type u_1} (f : Ω → EReal) : Ω → EReal

The positive part of an extended-real-valued function, f⁺ = max (f, 0).

Equations

• erealPositivePart f x = max (f x) 0

noncomputable def erealNegativePart {Ω : Type u_1} (f : Ω → EReal) : Ω → EReal

The negative part of an extended-real-valued function, f⁻ = max (-f, 0).

Equations

• erealNegativePart f x = max (-f x) 0

def HasFiniteAbsIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Ω → EReal) : Prop

Predicate asserting that an extended-real-valued function has finite absolute Lebesgue integral.

Equations

• HasFiniteAbsIntegral μ f = (∫⁻ (x : Ω), (f x).abs ∂μ < ⊤)

noncomputable def lebesgueIntegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f : Ω → EReal) (hf_measurable : Measurable f) (hf_abs : HasFiniteAbsIntegral μ f) : EReal

Definition 8.10 (Lebesgue integral): for a measurable f : Ω → EReal with ∫ |f| dμ < ∞, define f⁺ := max (f, 0), f⁻ := max (-f, 0), and set ∫ f dμ := ∫ f⁺ dμ - ∫ f⁻ dμ.

Equations

• One or more equations did not get rendered due to their size.

theorem proposition_8_10_1 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f g : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) (_hg : MeasureTheory.Integrable g μ) (c : ℝ) : MeasureTheory.Integrable (fun (x : Ω) => c * f x) μ ∧ ∫ (x : Ω), c * f x ∂μ = c * ∫ (x : Ω), f x ∂μ

Proposition 8.10.1: if f,g : Ω → ℝ are absolutely integrable, then for every c : ℝ, cf is absolutely integrable and ∫ cf dμ = c ∫ f dμ.

theorem proposition_8_10_2 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f g : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) : MeasureTheory.Integrable (fun (x : Ω) => f x + g x) μ ∧ ∫ (x : Ω), f x + g x ∂μ = ∫ (x : Ω), f x ∂μ + ∫ (x : Ω), g x ∂μ

Proposition 8.10.2: if f,g : Ω → ℝ are absolutely integrable (equivalently, integrable), then f + g is absolutely integrable and ∫ (f + g) dμ = ∫ f dμ + ∫ g dμ.

theorem proposition_8_10_3 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f g : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : ∀ (x : Ω), f x ≤ g x) : ∫ (x : Ω), f x ∂μ ≤ ∫ (x : Ω), g x ∂μ

Proposition 8.10.3: let (Ω, 𝒜, μ) be a measure space and let f, g : Ω → ℝ be absolutely integrable (∫ |f| dμ < ∞ and ∫ |g| dμ < ∞). If f x ≤ g x for all x ∈ Ω, then ∫ f dμ ≤ ∫ g dμ.

theorem proposition_8_10_4 {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (f g : Ω → ℝ) (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hfg : f =ᵐ[μ] g) : ∫ (x : Ω), f x ∂μ = ∫ (x : Ω), g x ∂μ

Proposition 8.10.4: let (Ω, 𝒜, μ) be a measure space and let f, g : Ω → ℝ be absolutely integrable (∫ |f| dμ < ∞ and ∫ |g| dμ < ∞). If f(x) = g(x) for μ-almost every x ∈ Ω, then ∫ f dμ = ∫ g dμ.

theorem helperForTheorem_8_5_measurableLimitFromPointwiseTendsto {Ω : Type u_1} [MeasurableSpace Ω] (fSeq : ℕ → Ω → EReal) (f : Ω → EReal) (h_measurable : ∀ (n : ℕ), Measurable (fSeq n)) (h_tendsto : ∀ (x : Ω), Filter.Tendsto (fun (n : ℕ) => fSeq n x) Filter.atTop (nhds (f x))) : Measurable f

Helper for Theorem 8.5: measurability of a pointwise limit in EReal.

theorem helperForTheorem_8_5_posPartToENNReal_le_abs (z : EReal) : (max z 0).toENNReal ≤ z.abs

Helper for Theorem 8.5: the positive-part ENNReal map is bounded by absolute value.

theorem helperForTheorem_8_5_negPartToENNReal_le_abs (z : EReal) : (max (-z) 0).toENNReal ≤ z.abs

Helper for Theorem 8.5: the negative-part ENNReal map is bounded by absolute value.

theorem helperForTheorem_8_5_abs_eq_posPartAddNegPart (z : EReal) : z.abs = (max z 0).toENNReal + (max (-z) 0).toENNReal

Helper for Theorem 8.5: decomposition of absolute value into positive and negative ENNReal parts.

theorem helperForTheorem_8_5_abs_le_posPartAddNegPart (z : EReal) : z.abs ≤ (max z 0).toENNReal + (max (-z) 0).toENNReal

Helper for Theorem 8.5: absolute value is bounded by positive and negative ENNReal parts.

theorem helperForTheorem_8_5_hasFiniteAbsIntegral_of_domination {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (g : Ω → EReal) (F : Ω → ENNReal) (hF_integrable : ∫⁻ (x : Ω), F x ∂μ < ⊤) (h_dom : ∀ (x : Ω), ↑(g x).abs ≤ ↑(F x)) : HasFiniteAbsIntegral μ g

Helper for Theorem 8.5: domination by an integrable bound yields finite absolute integral.

theorem lebesgue_dominated_convergence_on_subtype {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : MeasurableSet Ω) (fSeq : ℕ → ↑Ω → EReal) (f : ↑Ω → EReal) (h_measurable : ∀ (n_1 : ℕ), Measurable (fSeq n_1)) (h_tendsto : ∀ (x : ↑Ω), Filter.Tendsto (fun (n : ℕ) => fSeq n x) Filter.atTop (nhds (f x))) (F : ↑Ω → ENNReal) (hF_measurable : Measurable F) (hF_integrable : ∫⁻ (x : { x : Fin n → ℝ // x ∈ Ω }), F x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume < ⊤) (h_dom : ∀ (n_1 : ℕ) (x : ↑Ω), ↑(fSeq n_1 x).abs ≤ ↑(F x)) : ∃ (hf_measurable : Measurable f) (hf_abs : HasFiniteAbsIntegral (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) f) (hfSeq_abs : ∀ (n_1 : ℕ), HasFiniteAbsIntegral (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) (fSeq n_1)), Filter.Tendsto (fun (n_1 : ℕ) => lebesgueIntegral (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) (fSeq n_1) ⋯ ⋯) Filter.atTop (nhds (lebesgueIntegral (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) f hf_measurable hf_abs))

Theorem 8.5 (Lebesgue dominated convergence theorem): let Ω ⊆ ℝ^n be measurable, let fₙ : Ω → EReal be measurable with pointwise limit f, and suppose there is a measurable F : Ω → [0, ∞] with finite integral such that |fₙ x| ≤ F x for all x and all n. Then f is measurable, ∫ |f| < ∞, and ∫ f is the limit of ∫ fₙ.

noncomputable def upperLowerLebesgueIntegralsOn {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : MeasurableSet Ω) (f : ↑Ω → ℝ) : EReal × EReal

Definition 8.11 (Upper and lower Lebesgue integrals): let Ω ⊆ ℝ^n be measurable and f : Ω → ℝ. The upper integral is the infimum of integrals of absolutely integrable majorants of f, and the lower integral is the supremum of integrals of absolutely integrable minorants of f.

Equations

• One or more equations did not get rendered due to their size.

theorem helperForLemma_8_9_negUpperCandidate_iff_lowerCandidate {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : ↑Ω → ℝ) (I : EReal) : I ∈ {J : EReal | ∃ (g : ↑Ω → ℝ), MeasureTheory.Integrable g (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧ (∀ (x : ↑Ω), -f x ≤ g x) ∧ J = ↑(∫ (x : { x : Fin n → ℝ // x ∈ Ω }), g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)} ↔ -I ∈ {J : EReal | ∃ (g : ↑Ω → ℝ), MeasureTheory.Integrable g (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧ (∀ (x : ↑Ω), g x ≤ f x) ∧ J = ↑(∫ (x : { x : Fin n → ℝ // x ∈ Ω }), g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)}

Helper for Lemma 8.9: upper-candidate membership for -f is equivalent to lower-candidate membership for f after negating the candidate value.

theorem helperForLemma_8_9_negLowerCandidate_iff_upperCandidate {n : ℕ} (Ω : Set (Fin n → ℝ)) (f : ↑Ω → ℝ) (I : EReal) : I ∈ {J : EReal | ∃ (g : ↑Ω → ℝ), MeasureTheory.Integrable g (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧ (∀ (x : ↑Ω), g x ≤ -f x) ∧ J = ↑(∫ (x : { x : Fin n → ℝ // x ∈ Ω }), g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)} ↔ -I ∈ {J : EReal | ∃ (g : ↑Ω → ℝ), MeasureTheory.Integrable g (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧ (∀ (x : ↑Ω), f x ≤ g x) ∧ J = ↑(∫ (x : { x : Fin n → ℝ // x ∈ Ω }), g x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume)}

Helper for Lemma 8.9: lower-candidate membership for -f is equivalent to upper-candidate membership for f after negating the candidate value.

theorem helperForLemma_8_9_upperLower_neg_components {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : MeasurableSet Ω) (f : ↑Ω → ℝ) : (upperLowerLebesgueIntegralsOn Ω hΩ fun (x : ↑Ω) => -f x).1 = -(upperLowerLebesgueIntegralsOn Ω hΩ f).2 ∧ (upperLowerLebesgueIntegralsOn Ω hΩ fun (x : ↑Ω) => -f x).2 = -(upperLowerLebesgueIntegralsOn Ω hΩ f).1

Helper for Lemma 8.9: the upper/lower components for -f are the negations of the lower/upper components for f.

theorem helperForLemma_8_9_finalize_from_component_equalities {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : MeasurableSet Ω) (f : ↑Ω → ℝ) (A : ℝ) (hUpper : (upperLowerLebesgueIntegralsOn Ω hΩ f).1 = ↑A) (hLower : (upperLowerLebesgueIntegralsOn Ω hΩ f).2 = ↑A) : (upperLowerLebesgueIntegralsOn Ω hΩ f).1 = ↑A ∧ (upperLowerLebesgueIntegralsOn Ω hΩ f).2 = ↑A ∧ (upperLowerLebesgueIntegralsOn Ω hΩ fun (x : ↑Ω) => -f x).1 = -↑A ∧ (upperLowerLebesgueIntegralsOn Ω hΩ fun (x : ↑Ω) => -f x).2 = -↑A

Helper for Lemma 8.9: from equal upper/lower component values at A, conclude the same equalities for f and the corresponding sign-flipped values for -f.

theorem lemma_8_9 {n : ℕ} (Ω : Set (Fin n → ℝ)) (hΩ : MeasurableSet Ω) (f : ↑Ω → ℝ) (A : ℝ) (hUpper : (upperLowerLebesgueIntegralsOn Ω hΩ f).1 = ↑A) (hLower : (upperLowerLebesgueIntegralsOn Ω hΩ f).2 = ↑A) : (upperLowerLebesgueIntegralsOn Ω hΩ f).1 = (upperLowerLebesgueIntegralsOn Ω hΩ f).2 ∧ MeasureTheory.Integrable f (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (x : ↑Ω) => |f x|) (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume) ∧ ∫ (x : { x : Fin n → ℝ // x ∈ Ω }), f x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume = A ∧ (let Ωneg := (fun (x : Fin n → ℝ) => -x) ⁻¹' Ω; have fneg := fun (x : ↑Ωneg) => f ⟨-↑x, ⋯⟩; ∫ (x : { x : Fin n → ℝ // x ∈ Ωneg }), fneg x ∂MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume = A) ∧ (upperLowerLebesgueIntegralsOn Ω hΩ f).1 = ↑A ∧ (upperLowerLebesgueIntegralsOn Ω hΩ f).2 = ↑A ∧ (upperLowerLebesgueIntegralsOn Ω hΩ fun (x : ↑Ω) => -f x).1 = -↑A ∧ (upperLowerLebesgueIntegralsOn Ω hΩ fun (x : ↑Ω) => -f x).2 = -↑A

Lemma 8.9: let Ω ⊆ ℝ^n be measurable and f : Ω → ℝ. If the upper and lower Lebesgue-integral components of f are both equal to a finite value A : ℝ, then f is integrable (hence absolutely integrable) on the subtype measure, the integral of f is A, the upper/lower components for f are A, and the upper/lower components for -f are -A. In particular, the usual integral agrees with both upper and lower components.

theorem ae_eq_of_integrable_le_and_integral_eq_on_real (f g : ℝ → ℝ) (hf_measurable : Measurable f) (hg_measurable : Measurable g) (hf_integrable : MeasureTheory.Integrable f MeasureTheory.volume) (hg_integrable : MeasureTheory.Integrable g MeasureTheory.volume) (hfg_le : ∀ (x : ℝ), f x ≤ g x) (h_integral_eq : ∫ (x : ℝ), f x = ∫ (x : ℝ), g x) : f =ᵐ[MeasureTheory.volume] g

Proposition 8.11: if measurable real-valued functions f and g on ℝ are integrable, satisfy f x ≤ g x for all x, and have equal integrals, then f = g almost everywhere with respect to Lebesgue measure.

theorem proposition_8_12 : have f := fun (n : ℕ) (x : ℝ) => (Set.Ico (↑n) (↑n + 1)).indicator (fun (x : ℝ) => 1) x - (Set.Ico (↑n + 1) (↑n + 2)).indicator (fun (x : ℝ) => 1) x; have g := fun (x : ℝ) => (Set.Ico 1 2).indicator (fun (x : ℝ) => 1) x; (∀ (x : ℝ), Filter.Tendsto (fun (N : ℕ) => ∑ n ∈ Finset.range N, f (n + 1) x) Filter.atTop (nhds (g x))) ∧ ∫ (x : ℝ), ∑' (n : ℕ), f (n + 1) x ≠ ∑' (n : ℕ), ∫ (x : ℝ), f (n + 1) x

Proposition 8.12: defining fₙ = χ_[n,n+1) - χ_[n+1,n+2) on ℝ, the partial sums from n = 1 converge pointwise to g = χ_[1,2), and integration does not commute with this series: ∫ (∑_{n=1}^∞ fₙ) dm ≠ ∑_{n=1}^∞ ∫ fₙ dm.