測度論と積分

5.3. 実数値関数の積分🔗

X を可測空間とし、\mu を X 上の測度、f : X \to \mathbb{R} を実数値関数とします。

定義.

f が 可積分 であるとは、f が可測であり、 \underline{\int}_{x \in X} |f(x)|\,d\mu < \infty が成り立つことをいう。

Lean code
/-- A real-valued function has finite integral if the lower integral of its absolute value is finite. -/ @[fun_prop] def HasFiniteIntegral (f : X → ℝ) (μ : Measure X) : Prop := ∫⁻ x, ENNReal.ofReal |f x| ∂μ < ∞
/-- A real-valued function is integrable if it is measurable and has finite integral. -/ structure Integrable (f : X → ℝ) (μ : Measure X) : Prop where measurable : Measurable f hasFiniteIntegral : HasFiniteIntegral f μ
定義.

f の 正部分 と 負部分 を f^+(x) \coloneqq \max(f(x), 0), \qquad f^-(x) \coloneqq \max(-f(x), 0) で定める。

Lean code
/-- The positive part of a real-valued function, regarded as an `ℝ≥0∞`-valued function. -/ def posPart (f : X → ℝ) : X → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
/-- The negative part of a real-valued function, regarded as an `ℝ≥0∞`-valued function. -/ def negPart (f : X → ℝ) : X → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (-f x)
補題.

f が可積分ならば、正部分と負部分はどちらも有限な下積分をもつ: \underline{\int}_{x \in X} f^+(x)\,d\mu < \infty, \qquad \underline{\int}_{x \in X} f^-(x)\,d\mu < \infty.

Lean code
theorem Integrable.posPart_ne_top {f : X → ℝ} (hf : Integrable f μ) : ∫⁻ x, posPart f x ∂μ ≠ ∞ := hf.hasFiniteIntegral.pos_ne_top
theorem Integrable.negPart_ne_top {f : X → ℝ} (hf : Integrable f μ) : ∫⁻ x, negPart f x ∂μ ≠ ∞ := hf.hasFiniteIntegral.neg_ne_top
定義.

可積分な実数値関数 f : X \to \mathbb{R} に対して、その ルベーグ積分 を \int_{x \in X} f(x)\,d\mu \coloneqq \underline{\int}_{x \in X} f^+(x)\,d\mu - \underline{\int}_{x \in X} f^-(x)\,d\mu で定める。

Lean code
open Classical in /-- The Lebesgue integral of a real-valued function, defined using any integrable representative in its almost-everywhere class, and `0` if no such representative exists. -/ def integral (μ : Measure X) (f : X → ℝ) : ℝ := if h : HasIntegrableRep f μ then (∫⁻ x, posPart (integrableRep h) x ∂μ).toReal - (∫⁻ x, negPart (integrableRep h) x ∂μ).toReal else 0
補題.

ルベーグ積分は可積分な実数値関数の上で線形である: \int_{x \in X} (f(x) + g(x))\,d\mu = \int_{x \in X} f(x)\,d\mu + \int_{x \in X} g(x)\,d\mu. \int_{x \in X} c f(x)\,d\mu = c \int_{x \in X} f(x)\,d\mu.

Lean code
theorem integral_add_eq_integral_add {f g : X → ℝ} (hf : Integrable f μ) (hg : Integrable g μ) : ∫ x, (f x + g x) ∂μ = ∫ x, f x ∂μ + ∫ x, g x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μ⊢ ∫ (x : X), f x + g x ∂μ = ∫ (x : X), f x ∂μ + ∫ (x : X), g x ∂μ calc ∫ x, (f x + g x) ∂μ = ∫ x, (f x - (-g x)) ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μ⊢ ∫ (x : X), f x + g x ∂μ = ∫ (x : X), f x - -g x ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μ⊢ (fun x => f x + g x) =ᶠ[ae μ] fun x => f x - -g x exact Filter.Eventually.of_forall fun x ↦ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μx:X⊢ (fun x => f x + g x) x = (fun x => f x - -g x) x All goals completed! 🐙 _ = ∫ x, f x ∂μ - ∫ x, -g x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μ⊢ ∫ (x : X), f x - -g x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X), -g x ∂μ All goals completed! 🐙 _ = ∫ x, f x ∂μ + ∫ x, g x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μ⊢ ∫ (x : X), f x ∂μ - ∫ (x : X), -g x ∂μ = ∫ (x : X), f x ∂μ + ∫ (x : X), g x ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝg:X → ℝhf:Integrable f μhg:Integrable g μ⊢ ∫ (x : X), f x ∂μ - -∫ (x : X), g x ∂μ = ∫ (x : X), f x ∂μ + ∫ (x : X), g x ∂μ All goals completed! 🐙
theorem integral_const_mul (c : ℝ) {f : X → ℝ} (hf : Integrable f μ) : ∫ x, c * f x ∂μ = c * ∫ x, f x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:0 ≤ c⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ c⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:0 ≤ c⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ c⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ have hc' : 0 ≤ -c := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), c * f x ∂μ = c * ∫ (x : X), f x ∂μ All goals completed! 🐙 calc ∫ x, c * f x ∂μ = ∫ x, -((-c) * f x) ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ chc':0 ≤ -c := le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt (lt_of_not_ge hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))⊢ ∫ (x : X), c * f x ∂μ = ∫ (x : X), -(-c * f x) ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ chc':0 ≤ -c := le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt (lt_of_not_ge hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))⊢ (fun x => c * f x) =ᶠ[ae μ] fun x => -(-c * f x) exact Filter.Eventually.of_forall fun x ↦ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ chc':0 ≤ -c := le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt (lt_of_not_ge hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))x:X⊢ (fun x => c * f x) x = (fun x => -(-c * f x)) x All goals completed! 🐙 _ = -∫ x, (-c) * f x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ chc':0 ≤ -c := le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt (lt_of_not_ge hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))⊢ ∫ (x : X), -(-c * f x) ∂μ = -∫ (x : X), -c * f x ∂μ All goals completed! 🐙 _ = -((-c) * ∫ x, f x ∂μ) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ chc':0 ≤ -c := le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt (lt_of_not_ge hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))⊢ -∫ (x : X), -c * f x ∂μ = -(-c * ∫ (x : X), f x ∂μ) All goals completed! 🐙 _ = c * ∫ x, f x ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xc:ℝf:X → ℝhf:Integrable f μhc:¬0 ≤ chc':0 ≤ -c := le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.atom_pf c) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul c (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (c ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero c (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_neg (Mathlib.Tactic.Linarith.sub_neg_of_lt (lt_of_not_ge hc)) (Mathlib.Tactic.Linarith.sub_neg_of_lt a)))⊢ -(-c * ∫ (x : X), f x ∂μ) = c * ∫ (x : X), f x ∂μ All goals completed! 🐙
補題.

絶対値の積分は積分の絶対値を上から抑える: \left|\int_{x \in X} f(x)\,d\mu\right| \le \int_{x \in X} |f(x)|\,d\mu.

Lean code
theorem abs_integral_le_integral_abs {f : X → ℝ} (hf : Integrable f μ) : |∫ x, f x ∂μ| ≤ ∫ x, |f x| ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ |∫ (x : X), f x ∂μ| ≤ ∫ (x : X), |f x| ∂μ calc |∫ x, f x ∂μ| = |∫ x, (posPart f x).toReal ∂μ - ∫ x, (negPart f x).toReal ∂μ| := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ |∫ (x : X), f x ∂μ| = |∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μ| All goals completed! 🐙 _ ≤ ∫ x, (posPart f x).toReal ∂μ + ∫ x, (negPart f x).toReal ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ |∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μ| ≤ ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ -(∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ) ≤ ∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μ ∧ ∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μ ≤ ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ -(∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ) ≤ ∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μ ≤ ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ -(∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ) ≤ ∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μX:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), (posPart f x).toReal ∂μ - ∫ (x : X), (negPart f x).toReal ∂μ ≤ ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ linarith [integral_nonneg hf.posPart_toReal (fun _ ↦ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μx✝:X⊢ 0 ≤ (posPart f x✝).toReal All goals completed! 🐙), integral_nonneg hf.negPart_toReal (fun _ ↦ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μx✝:X⊢ 0 ≤ (negPart f x✝).toReal All goals completed! 🐙)] _ = ∫ x, |f x| ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ = ∫ (x : X), |f x| ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), |f x| ∂μ = ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ calc ∫ x, |f x| ∂μ = ∫ x, (posPart f x).toReal + (negPart f x).toReal ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), |f x| ∂μ = ∫ (x : X), (posPart f x).toReal + (negPart f x).toReal ∂μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ (fun x => |f x|) =ᶠ[ae μ] fun x => (posPart f x).toReal + (negPart f x).toReal All goals completed! 🐙 _ = ∫ x, (posPart f x).toReal ∂μ + ∫ x, (negPart f x).toReal ∂μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xf:X → ℝhf:Integrable f μ⊢ ∫ (x : X), (posPart f x).toReal + (negPart f x).toReal ∂μ = ∫ (x : X), (posPart f x).toReal ∂μ + ∫ (x : X), (negPart f x).toReal ∂μ All goals completed! 🐙
定理 (優収束定理).

F_0, F_1, \dots : X \to \mathbb{R} を可測関数の列とし、 g : X \to \mathbb{R} を可積分関数とする。 さらに任意の n \in \mathbb{N} と任意の x \in X に対して |F_n(x)| \le g(x) が成り立ち、任意の x \in X に対して F_n(x) \to f(x) が成り立つとする。 このとき \lim_{n \to \infty} \int_{x \in X} F_n(x)\,d\mu = \int_{x \in X} f(x)\,d\mu. が成り立つ。

Lean code
/-- Dominated convergence theorem for real-valued measurable functions. -/ theorem tendsto_integral_of_dominated_convergence {F : ℕ → X → ℝ} {f bound : X → ℝ} (hF_meas : ∀ n, Measurable (F n)) (h_bound_int : Integrable bound μ) (h_bound : ∀ n x, |F n x| ≤ bound x) (h_lim : ∀ x, Tendsto (fun n ↦ F n x) atTop (nhds (f x))) : Tendsto (fun n ↦ ∫ x, F n x ∂μ) atTop (nhds (∫ x, f x ∂μ)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) have h_bound_nonneg : ∀ x, 0 ≤ bound x := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))x:X⊢ 0 ≤ bound x All goals completed! 🐙 have hf_meas : Measurable f := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) All goals completed! 🐙 have h_abs_f_le : ∀ x, |f x| ≤ bound x := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)x:X⊢ |f x| ≤ bound x X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)x:Xh_closed:IsClosed (Icc (-bound x) (bound x)) := isClosed_Icc⊢ |f x| ≤ bound x have h_mem : ∀ᶠ n in atTop, F n x ∈ Set.Icc (-bound x) (bound x) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)x:Xh_closed:IsClosed (Icc (-bound x) (bound x)) := isClosed_Icc⊢ ∀ (x_1 : ℕ), F x_1 x ∈ Icc (-bound x) (bound x) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)x:Xh_closed:IsClosed (Icc (-bound x) (bound x)) := isClosed_Iccn:ℕ⊢ F n x ∈ Icc (-bound x) (bound x) All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)x:Xh_closed:IsClosed (Icc (-bound x) (bound x)) := isClosed_Icch_mem:∀ᶠ (n : ℕ) in atTop, F n x ∈ Icc (-bound x) (bound x) := Eventually.of_forall fun n => abs_le.mp (h_bound n x)hf_mem:f x ∈ Icc (-bound x) (bound x) := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem⊢ |f x| ≤ bound x All goals completed! 🐙 have hF_int : ∀ n, Integrable (F n) μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memn:ℕ⊢ Integrable (F n) μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memn:ℕ⊢ HasFiniteIntegral (F n) μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memn:ℕ⊢ ∫⁻ (x : X), ENNReal.ofReal |F n x| ∂μ ≠ ∞ X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memn:ℕ⊢ ∫⁻ (x : X), ENNReal.ofReal |F n x| ∂μ ≤ ∫⁻ (x : X), ENNReal.ofReal (bound x) ∂μ All goals completed! 🐙 have hf_int : Integrable f μ := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }⊢ HasFiniteIntegral f μ X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }⊢ ∫⁻ (x : X), ENNReal.ofReal |f x| ∂μ ≠ ∞ X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }⊢ ∫⁻ (x : X), ENNReal.ofReal |f x| ∂μ ≤ ∫⁻ (x : X), ENNReal.ofReal (bound x) ∂μ All goals completed! 🐙 have h_pos_lim : ∀ x, Tendsto (fun n ↦ posPart (F n) x) atTop (nhds (posPart f x)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }hf_int:Integrable f μ := { measurable := hf_meas, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }x:X⊢ Tendsto (fun n => posPart (F n) x) atTop (nhds (posPart f x)) All goals completed! 🐙 have h_neg_lim : ∀ x, Tendsto (fun n ↦ negPart (F n) x) atTop (nhds (negPart f x)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }hf_int:Integrable f μ := { measurable := hf_meas, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : X), Tendsto (fun n => posPart (F n) x) atTop (nhds (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))x:X⊢ Tendsto (fun n => negPart (F n) x) atTop (nhds (negPart f x)) All goals completed! 🐙 have h_pos_tendsto : Tendsto (fun n ↦ ∫⁻ x, posPart (F n) x ∂μ) atTop (nhds (∫⁻ x, posPart f x ∂μ)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) All goals completed! 🐙 have h_neg_tendsto : Tendsto (fun n ↦ ∫⁻ x, negPart (F n) x ∂μ) atTop (nhds (∫⁻ x, negPart f x ∂μ)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) All goals completed! 🐙 have h_pos_toReal : Tendsto (fun n ↦ (∫⁻ x, posPart (F n) x ∂μ).toReal) atTop (nhds ((∫⁻ x, posPart f x ∂μ).toReal)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) All goals completed! 🐙 have h_neg_toReal : Tendsto (fun n ↦ (∫⁻ x, negPart (F n) x ∂μ).toReal) atTop (nhds ((∫⁻ x, negPart f x ∂μ).toReal)) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) All goals completed! 🐙 have hF_integral : (fun n ↦ ∫ x, F n x ∂μ) = (fun n ↦ (∫⁻ x, posPart (F n) x ∂μ).toReal - (∫⁻ x, negPart (F n) x ∂μ).toReal) := X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))⊢ Tendsto (fun n => ∫ (x : X), F n x ∂μ) atTop (nhds (∫ (x : X), f x ∂μ)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }hf_int:Integrable f μ := { measurable := hf_meas, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : X), Tendsto (fun n => posPart (F n) x) atTop (nhds (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))h_neg_lim:∀ (x : X), Tendsto (fun n => negPart (F n) x) atTop (nhds (negPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto (Continuous.comp continuous_ofReal continuous_neg) (f x)) (h_lim x))h_pos_tendsto:Tendsto (fun n => ∫⁻ (x : X), posPart (F n) x ∂μ) atTop (nhds (∫⁻ (x : X), posPart f x ∂μ)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_posPart (hF_meas n)) (fun n => ae_of_all μ fun x => le_trans (posPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (ae_of_all μ h_pos_lim)h_neg_tendsto:Tendsto (fun n => ∫⁻ (x : X), negPart (F n) x ∂μ) atTop (nhds (∫⁻ (x : X), negPart f x ∂μ)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_negPart (hF_meas n)) (fun n => ae_of_all μ fun x => le_trans (negPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (ae_of_all μ h_neg_lim)h_pos_toReal:Tendsto (fun n => (∫⁻ (x : X), posPart (F n) x ∂μ).toReal) atTop (nhds (∫⁻ (x : X), posPart f x ∂μ).toReal) := Tendsto.comp (tendsto_toReal (Integrable.posPart_ne_top hf_int)) h_pos_tendstoh_neg_toReal:Tendsto (fun n => (∫⁻ (x : X), negPart (F n) x ∂μ).toReal) atTop (nhds (∫⁻ (x : X), negPart f x ∂μ).toReal) := Tendsto.comp (tendsto_toReal (Integrable.negPart_ne_top hf_int)) h_neg_tendston:ℕ⊢ ∫ (x : X), F n x ∂μ = (∫⁻ (x : X), posPart (F n) x ∂μ).toReal - (∫⁻ (x : X), negPart (F n) x ∂μ).toReal All goals completed! 🐙 X:Type u_1inst✝:MeasurableSpace Xμ:Measure XF:ℕ → X → ℝf:X → ℝbound:X → ℝhF_meas:∀ (n : ℕ), Measurable (F n)h_bound_int:Integrable bound μh_bound:∀ (n : ℕ) (x : X), |F n x| ≤ bound xh_lim:∀ (x : X), Tendsto (fun n => F n x) atTop (nhds (f x))h_bound_nonneg:∀ (x : X), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)hf_meas:Measurable f := measurable_of_tendsto_metrizable hF_meas (tendsto_pi_nhds.mpr h_lim)h_abs_f_le:∀ (x : X), |f x| ≤ bound x := fun x => have h_closed := isClosed_Icc; have h_mem := Eventually.of_forall fun n => abs_le.mp (h_bound n x); have hf_mem := IsClosed.mem_of_tendsto h_closed (h_lim x) h_mem; abs_le.mpr hf_memhF_int:∀ (n : ℕ), Integrable (F n) μ := fun n => { measurable := hF_meas n, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }hf_int:Integrable f μ := { measurable := hf_meas, hasFiniteIntegral := hasFiniteIntegral_of_ne_top (ne_top_of_le_ne_top (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : X), Tendsto (fun n => posPart (F n) x) atTop (nhds (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))h_neg_lim:∀ (x : X), Tendsto (fun n => negPart (F n) x) atTop (nhds (negPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto (Continuous.comp continuous_ofReal continuous_neg) (f x)) (h_lim x))h_pos_tendsto:Tendsto (fun n => ∫⁻ (x : X), posPart (F n) x ∂μ) atTop (nhds (∫⁻ (x : X), posPart f x ∂μ)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_posPart (hF_meas n)) (fun n => ae_of_all μ fun x => le_trans (posPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (ae_of_all μ h_pos_lim)h_neg_tendsto:Tendsto (fun n => ∫⁻ (x : X), negPart (F n) x ∂μ) atTop (nhds (∫⁻ (x : X), negPart f x ∂μ)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_negPart (hF_meas n)) (fun n => ae_of_all μ fun x => le_trans (negPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) (Integrable.lintegral_ne_top_of_nonneg h_bound_int h_bound_nonneg) (ae_of_all μ h_neg_lim)h_pos_toReal:Tendsto (fun n => (∫⁻ (x : X), posPart (F n) x ∂μ).toReal) atTop (nhds (∫⁻ (x : X), posPart f x ∂μ).toReal) := Tendsto.comp (tendsto_toReal (Integrable.posPart_ne_top hf_int)) h_pos_tendstoh_neg_toReal:Tendsto (fun n => (∫⁻ (x : X), negPart (F n) x ∂μ).toReal) atTop (nhds (∫⁻ (x : X), negPart f x ∂μ).toReal) := Tendsto.comp (tendsto_toReal (Integrable.negPart_ne_top hf_int)) h_neg_tendstohF_integral:(fun n => ∫ (x : X), F n x ∂μ) = fun n => (∫⁻ (x : X), posPart (F n) x ∂μ).toReal - (∫⁻ (x : X), negPart (F n) x ∂μ).toReal := funext fun n => integral_eq_lintegral_posPart_sub_lintegral_negPart (hF_int n)⊢ Tendsto (fun n => (∫⁻ (x : X), posPart (F n) x ∂μ).toReal - (∫⁻ (x : X), negPart (F n) x ∂μ).toReal) atTop (nhds ((∫⁻ (x : X), posPart f x ∂μ).toReal - (∫⁻ (x : X), negPart f x ∂μ).toReal)) All goals completed! 🐙