測度論と積分

3.3. 実数直線上の実数値関数の積分🔗

f : \mathbb{R} \to \mathbb{R} を実数値関数とします。

定義.

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

Lean code
/-- A real-valued function has finite integral if the lower integral of its absolute value is finite. -/ def HasFiniteIntegral (f : ℝ → ℝ) : Prop := ∫⁻ x, ENNReal.ofReal |f x| < ∞
/-- A real-valued function on `ℝ` is integrable if it is measurable and the lower integral of its absolute value is finite. -/ structure Integrable (f : ℝ → ℝ) : Prop where measurable : MeasurableFun 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 : ℝ → ℝ) : ℝ → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (f x)
/-- The negative part of a real-valued function, regarded as an `ℝ≥0∞`-valued function. -/ def negPart (f : ℝ → ℝ) : ℝ → ℝ≥0∞ := fun x ↦ ENNReal.ofReal (-f x)
補題.

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

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

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

Lean code
/-- The Lebesgue integral of a real-valued function on `ℝ`. -/ noncomputable def integral (f : ℝ → ℝ) : ℝ := f:ℝ → ℝ⊢ ℝ classical All goals completed! 🐙
補題.

任意の x に対して f(x) \ge 0 ならば、積分は下積分と一致する: \int_{x \in \mathbb{R}} f(x)\,dx = \underline{\int}_{x \in \mathbb{R}} f(x)\,dx.

Lean code
theorem integral_eq_lintegral_of_nonneg {f : ℝ → ℝ} (hf_meas : MeasurableFun f) (hf_nonneg : ∀ x, 0 ≤ f x) : ∫ x, f x = (∫⁻ x, ENNReal.ofReal (f x)).toReal := f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f x⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toRealf:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal have hf_not : ¬ Integrable f := f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f x⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf:Integrable f⊢ False exact hf.posPart_ne_top (f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf:Integrable f⊢ ∫⁻ (x : ℝ), posPart f x = ∞ All goals completed! 🐙) All goals completed! 🐙 f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal have hf_int : Integrable f := f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f x⊢ ∫ (x : ℝ), f x = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal All goals completed! 🐙 f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf_int:Integrable f := integrable_of_nonneg hf_meas hf_nonneg (lt_of_le_of_ne le_top hfin)⊢ (∫⁻ (x : ℝ), posPart f x).toReal - (∫⁻ (x : ℝ), negPart f x).toReal = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf_int:Integrable f := integrable_of_nonneg hf_meas hf_nonneg (lt_of_le_of_ne le_top hfin)⊢ (∫⁻ (x : ℝ), posPart f x).toReal = (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf_int:Integrable f := integrable_of_nonneg hf_meas hf_nonneg (lt_of_le_of_ne le_top hfin)⊢ ∫⁻ (x : ℝ), posPart f x = ∫⁻ (x : ℝ), ENNReal.ofReal (f x) f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf_int:Integrable f := integrable_of_nonneg hf_meas hf_nonneg (lt_of_le_of_ne le_top hfin)⊢ ∀ (x : ℝ), posPart f x = ENNReal.ofReal (f x) f:ℝ → ℝhf_meas:MeasurableFun fhf_nonneg:∀ (x : ℝ), 0 ≤ f xhfin:¬∫⁻ (x : ℝ), ENNReal.ofReal (f x) = ∞hf_int:Integrable f := integrable_of_nonneg hf_meas hf_nonneg (lt_of_le_of_ne le_top hfin)x:ℝ⊢ posPart f x = ENNReal.ofReal (f x) All goals completed! 🐙
theorem integral_nonneg {f : ℝ → ℝ} (hf_nonneg : ∀ x, 0 ≤ f x) : 0 ≤ ∫ x, f x := f:ℝ → ℝhf_nonneg:∀ (x : ℝ), 0 ≤ f x⊢ 0 ≤ ∫ (x : ℝ), f x f:ℝ → ℝhf_nonneg:∀ (x : ℝ), 0 ≤ f xhf:Integrable f⊢ 0 ≤ ∫ (x : ℝ), f xf:ℝ → ℝhf_nonneg:∀ (x : ℝ), 0 ≤ f xhf:¬Integrable f⊢ 0 ≤ ∫ (x : ℝ), f x f:ℝ → ℝhf_nonneg:∀ (x : ℝ), 0 ≤ f xhf:Integrable f⊢ 0 ≤ ∫ (x : ℝ), f x f:ℝ → ℝhf_nonneg:∀ (x : ℝ), 0 ≤ f xhf:Integrable f⊢ 0 ≤ (∫⁻ (x : ℝ), ENNReal.ofReal (f x)).toReal All goals completed! 🐙 f:ℝ → ℝhf_nonneg:∀ (x : ℝ), 0 ≤ f xhf:¬Integrable f⊢ 0 ≤ ∫ (x : ℝ), f x All goals completed! 🐙
theorem integral_zero : (∫ _x, (0 : ℝ)) = 0 := ⊢ ∫ (_x : ℝ), 0 = 0 ⊢ (∫⁻ (x : ℝ), posPart (fun x => 0) x).toReal - (∫⁻ (x : ℝ), negPart (fun x => 0) x).toReal = 0 have hpos : posPart (fun _ : ℝ ↦ (0 : ℝ)) = fun _ ↦ (0 : ℝ≥0∞) := ⊢ ∫ (_x : ℝ), 0 = 0 x:ℝ⊢ posPart (fun x => 0) x = 0 All goals completed! 🐙 have hneg : negPart (fun _ : ℝ ↦ (0 : ℝ)) = fun _ ↦ (0 : ℝ≥0∞) := ⊢ ∫ (_x : ℝ), 0 = 0 hpos:(posPart fun x => 0) = fun x => 0 := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq ofReal_zero) 0) (eq_self 0))x:ℝ⊢ negPart (fun x => 0) x = 0 All goals completed! 🐙 All goals completed! 🐙
補題.

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

Lean code
theorem integral_add_eq_integral_add {f g : ℝ → ℝ} (hf : Integrable f) (hg : Integrable g) (hfg : Integrable (fun x ↦ f x + g x)) : ∫ x, f x + g x = (∫ x, f x) + ∫ x, g x := f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x have hlin : (∫⁻ x, posPart (fun x ↦ f x + g x) x) + (∫⁻ x, negPart f x) + (∫⁻ x, negPart g x) = (∫⁻ x, negPart (fun x ↦ f x + g x) x) + (∫⁻ x, posPart f x) + ∫⁻ x, posPart g x := f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x + negPart g x = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x + posPart g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = ∫⁻ (x : ℝ), negPart (fun x => f x + g x) x + (posPart f x + posPart g x) f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g x⊢ ∀ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = negPart (fun x => f x + g x) x + (posPart f x + posPart g x) f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xx:ℝ⊢ posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = negPart (fun x => f x + g x) x + (posPart f x + posPart g x) All goals completed! 🐙 f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfg⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hf⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hg⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfg⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hf⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hg⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:(((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x).toReal = (((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x).toReal := congrArg ENNReal.toReal hlin⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x)).toReal = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)).toReal⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:(∫⁻ (x : ℝ), posPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x).toReal = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)).toReal⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:(∫⁻ (x : ℝ), posPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), negPart f x).toReal + (∫⁻ (x : ℝ), negPart g x).toReal) = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)).toReal⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:(∫⁻ (x : ℝ), posPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), negPart f x).toReal + (∫⁻ (x : ℝ), negPart g x).toReal) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x).toReal⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:(∫⁻ (x : ℝ), posPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), negPart f x).toReal + (∫⁻ (x : ℝ), negPart g x).toReal) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), posPart f x).toReal + (∫⁻ (x : ℝ), posPart g x).toReal)⊢ ∫ (x : ℝ), f x + g x = (∫ (x : ℝ), f x) + ∫ (x : ℝ), g x f:ℝ → ℝg:ℝ → ℝhf:Integrable fhg:Integrable ghfg:Integrable fun x => f x + g xhlin:((∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x := Eq.mpr (id (congrArg (fun _a => _a = ((∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x) (add_assoc (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), negPart f x) (∫⁻ (x : ℝ), negPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), negPart f x) + ∫⁻ (x : ℝ), negPart g x) = _a) (add_assoc (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) (∫⁻ (x : ℝ), posPart f x) (∫⁻ (x : ℝ), posPart g x)))) (Eq.mpr (id (congrArg (fun _a => (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x) + _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + ((∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), posPart g x)) (Eq.symm (lintegral_add (measurable_posPart hfg.measurable) (Measurable.add (measurable_negPart hf.measurable) (measurable_negPart hg.measurable)))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x) + _a) (Eq.symm (lintegral_add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable))))) (Eq.mpr (id (congrArg (fun _a => ∫⁻ (x : ℝ), posPart (fun x => f x + g x) x + (negPart f x + negPart g x) = _a) (Eq.symm (lintegral_add (measurable_negPart hfg.measurable) (Measurable.add (measurable_posPart hf.measurable) (measurable_posPart hg.measurable)))))) (lintegral_congr fun x => Eq.mp (congr (congrArg Eq (add_assoc (posPart (fun x => f x + g x) x) (negPart f x) (negPart g x))) (add_assoc (negPart (fun x => f x + g x) x) (posPart f x) (posPart g x))) (posPart_add_add_negPart_eq_negPart_add_posPart x)))))))hL₁:∫⁻ (x : ℝ), posPart (fun x => f x + g x) x ≠ ∞ := Integrable.posPart_ne_top hfghL₂:∫⁻ (x : ℝ), negPart f x ≠ ∞ := Integrable.negPart_ne_top hfhL₃:∫⁻ (x : ℝ), negPart g x ≠ ∞ := Integrable.negPart_ne_top hghR₁:∫⁻ (x : ℝ), negPart (fun x => f x + g x) x ≠ ∞ := Integrable.negPart_ne_top hfghR₂:∫⁻ (x : ℝ), posPart f x ≠ ∞ := Integrable.posPart_ne_top hfhR₃:∫⁻ (x : ℝ), posPart g x ≠ ∞ := Integrable.posPart_ne_top hghreal:(∫⁻ (x : ℝ), posPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), negPart f x).toReal + (∫⁻ (x : ℝ), negPart g x).toReal) = (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x).toReal + ((∫⁻ (x : ℝ), posPart f x).toReal + (∫⁻ (x : ℝ), posPart g x).toReal)⊢ (∫⁻ (x : ℝ), posPart (fun x => f x + g x) x).toReal - (∫⁻ (x : ℝ), negPart (fun x => f x + g x) x).toReal = (∫⁻ (x : ℝ), posPart f x).toReal - (∫⁻ (x : ℝ), negPart f x).toReal + ((∫⁻ (x : ℝ), posPart g x).toReal - (∫⁻ (x : ℝ), negPart g x).toReal) All goals completed! 🐙
theorem integral_const_mul (c : ℝ) {f : ℝ → ℝ} (hf : Integrable f) : ∫ x, c * f x = c * ∫ x, f x := c:ℝf:ℝ → ℝhf:Integrable f⊢ ∫ (x : ℝ), c * f x = c * ∫ (x : ℝ), f x c:ℝf:ℝ → ℝhf:Integrable fhc:0 ≤ c⊢ ∫ (x : ℝ), c * f x = c * ∫ (x : ℝ), f xc:ℝf:ℝ → ℝhf:Integrable fhc:¬0 ≤ c⊢ ∫ (x : ℝ), c * f x = c * ∫ (x : ℝ), f x c:ℝf:ℝ → ℝhf:Integrable fhc:0 ≤ c⊢ ∫ (x : ℝ), c * f x = c * ∫ (x : ℝ), f x All goals completed! 🐙 c:ℝf:ℝ → ℝhf:Integrable fhc:¬0 ≤ c⊢ ∫ (x : ℝ), c * f x = c * ∫ (x : ℝ), f x have hc' : 0 ≤ -c := c:ℝf:ℝ → ℝhf:Integrable f⊢ ∫ (x : ℝ), c * f x = c * ∫ (x : ℝ), f x All goals completed! 🐙 calc integral (fun x ↦ c * f x) = integral (fun x ↦ -((-c) * f x)) := c:ℝf:ℝ → ℝhf:Integrable fhc:¬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 : ℝ), c * f x = ∫ (x : ℝ), -(-c * f x) c:ℝf:ℝ → ℝhf:Integrable fhc:¬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 : ℝ), c * f x = -(-c * f x) c:ℝf:ℝ → ℝhf:Integrable fhc:¬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:ℝ⊢ c * f x = -(-c * f x) All goals completed! 🐙 _ = -integral (fun x ↦ (-c) * f x) := c:ℝf:ℝ → ℝhf:Integrable fhc:¬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 : ℝ), -(-c * f x) = -∫ (x : ℝ), -c * f x All goals completed! 🐙 _ = -((-c) * integral f) := c:ℝf:ℝ → ℝhf:Integrable fhc:¬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 : ℝ), -c * f x = -(-c * integral f) All goals completed! 🐙 _ = c * integral f := c:ℝf:ℝ → ℝhf:Integrable fhc:¬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 * integral f) = c * integral f All goals completed! 🐙
補題.

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

Lean code
theorem abs_integral_le_lintegral_abs {f : ℝ → ℝ} (hf : Integrable f) : |∫ x, f x| ≤ (∫⁻ x, ENNReal.ofReal |f x|).toReal := f:ℝ → ℝhf:Integrable f⊢ |∫ (x : ℝ), f x| ≤ (∫⁻ (x : ℝ), ENNReal.ofReal |f x|).toReal have habs : ∫⁻ x, ENNReal.ofReal |f x| = (∫⁻ x, posPart f x) + ∫⁻ x, negPart f x := f:ℝ → ℝhf:Integrable f⊢ |∫ (x : ℝ), f x| ≤ (∫⁻ (x : ℝ), ENNReal.ofReal |f x|).toReal calc ∫⁻ x, ENNReal.ofReal |f x| = ∫⁻ x, posPart f x + negPart f x := f:ℝ → ℝhf:Integrable f⊢ ∫⁻ (x : ℝ), ENNReal.ofReal |f x| = ∫⁻ (x : ℝ), posPart f x + negPart f x f:ℝ → ℝhf:Integrable f⊢ ∀ (x : ℝ), ENNReal.ofReal |f x| = posPart f x + negPart f x f:ℝ → ℝhf:Integrable fx:ℝ⊢ ENNReal.ofReal |f x| = posPart f x + negPart f x f:ℝ → ℝhf:Integrable fx:ℝ⊢ posPart f x + negPart f x = ENNReal.ofReal |f x| All goals completed! 🐙 _ = (∫⁻ x, posPart f x) + ∫⁻ x, negPart f x := f:ℝ → ℝhf:Integrable f⊢ ∫⁻ (x : ℝ), posPart f x + negPart f x = (∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), negPart f x All goals completed! 🐙 calc |∫ x, f x| = |(∫⁻ x, posPart f x).toReal - (∫⁻ x, negPart f x).toReal| := f:ℝ → ℝhf:Integrable fhabs:∫⁻ (x : ℝ), ENNReal.ofReal |f x| = (∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), negPart f x := Trans.trans (lintegral_congr fun x => Eq.symm (posPart_add_negPart_eq_abs x)) (lintegral_add (measurable_posPart hf.measurable) (measurable_negPart hf.measurable))⊢ |∫ (x : ℝ), f x| = |(∫⁻ (x : ℝ), posPart f x).toReal - (∫⁻ (x : ℝ), negPart f x).toReal| All goals completed! 🐙 _ ≤ |(∫⁻ x, posPart f x).toReal| + |(∫⁻ x, negPart f x).toReal| := f:ℝ → ℝhf:Integrable fhabs:∫⁻ (x : ℝ), ENNReal.ofReal |f x| = (∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), negPart f x := Trans.trans (lintegral_congr fun x => Eq.symm (posPart_add_negPart_eq_abs x)) (lintegral_add (measurable_posPart hf.measurable) (measurable_negPart hf.measurable))⊢ |(∫⁻ (x : ℝ), posPart f x).toReal - (∫⁻ (x : ℝ), negPart f x).toReal| ≤ |(∫⁻ (x : ℝ), posPart f x).toReal| + |(∫⁻ (x : ℝ), negPart f x).toReal| All goals completed! 🐙 _ = (∫⁻ x, posPart f x).toReal + (∫⁻ x, negPart f x).toReal := f:ℝ → ℝhf:Integrable fhabs:∫⁻ (x : ℝ), ENNReal.ofReal |f x| = (∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), negPart f x := Trans.trans (lintegral_congr fun x => Eq.symm (posPart_add_negPart_eq_abs x)) (lintegral_add (measurable_posPart hf.measurable) (measurable_negPart hf.measurable))⊢ |(∫⁻ (x : ℝ), posPart f x).toReal| + |(∫⁻ (x : ℝ), negPart f x).toReal| = (∫⁻ (x : ℝ), posPart f x).toReal + (∫⁻ (x : ℝ), negPart f x).toReal All goals completed! 🐙 _ = (∫⁻ x, ENNReal.ofReal |f x|).toReal := f:ℝ → ℝhf:Integrable fhabs:∫⁻ (x : ℝ), ENNReal.ofReal |f x| = (∫⁻ (x : ℝ), posPart f x) + ∫⁻ (x : ℝ), negPart f x := Trans.trans (lintegral_congr fun x => Eq.symm (posPart_add_negPart_eq_abs x)) (lintegral_add (measurable_posPart hf.measurable) (measurable_negPart hf.measurable))⊢ (∫⁻ (x : ℝ), posPart f x).toReal + (∫⁻ (x : ℝ), negPart f x).toReal = (∫⁻ (x : ℝ), ENNReal.ofReal |f x|).toReal All goals completed! 🐙
定理 (優収束定理).

F_0, F_1, \dots : \mathbb{R} \to \mathbb{R} を可測関数の列とし、 g : \mathbb{R} \to \mathbb{R} を可積分関数とする。 次を仮定する。

  1. 任意の n \in \mathbb{N} と任意の x \in \mathbb{R} に対して |F_n(x)| \le g(x) である。

  2. 任意の x \in \mathbb{R} に対して、列 F_0(x), F_1(x), \dots は f(x) に収束する。

このとき \lim_{n \to \infty} \int_{x \in \mathbb{R}} F_n(x)\,dx = \int_{x \in \mathbb{R}} f(x)\,dx. が成り立つ。

Lean code
/-- Dominated convergence theorem for real-valued measurable functions on `ℝ`. -/ theorem tendsto_integral_of_dominated_convergence {F : ℕ → ℝ → ℝ} {f bound : ℝ → ℝ} (hF_meas : ∀ n, MeasurableFun (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)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) have h_bound_nonneg : ∀ x, 0 ≤ bound x := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))x:ℝ⊢ 0 ≤ bound x All goals completed! 🐙 have h_bound_ne_top : ∫⁻ x, ENNReal.ofReal (bound x) ≠ ∞ := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) have habs : (fun x ↦ ENNReal.ofReal |bound x|) = fun x ↦ ENNReal.ofReal (bound x) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)x:ℝ⊢ ENNReal.ofReal |bound x| = ENNReal.ofReal (bound x) All goals completed! 🐙 All goals completed! 🐙 F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_lim⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) have h_abs_f_le : ∀ x, |f x| ≤ bound x := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limx:ℝ⊢ |f x| ≤ bound x F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limx:ℝh_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) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limx:ℝh_closed:IsClosed (Icc (-bound x) (bound x)) := isClosed_Iccn:ℕ⊢ F n x ∈ Icc (-bound x) (bound x) All goals completed! 🐙 F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limx:ℝh_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) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 : ℝ), ENNReal.ofReal |F n x| ≠ ∞ F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 : ℝ), ENNReal.ofReal |F n x| ≤ ∫⁻ (x : ℝ), ENNReal.ofReal (bound x) All goals completed! 🐙 have hf_int : Integrable f := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }⊢ HasFiniteIntegral f F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }⊢ ∫⁻ (x : ℝ), ENNReal.ofReal |f x| ≠ ∞ F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_bound n x))) }⊢ ∫⁻ (x : ℝ), ENNReal.ofReal |f 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)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }x:ℝ⊢ Tendsto (fun n => posPart (F n) x) atTop (𝓝 (posPart f x)) All goals completed! 🐙 have h_neg_lim : ∀ x, Tendsto (fun n ↦ negPart (F n) x) atTop (nhds (negPart f x)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : ℝ), Tendsto (fun n => posPart (F n) x) atTop (𝓝 (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))x:ℝ⊢ Tendsto (fun n => negPart (F n) x) atTop (𝓝 (negPart f x)) All goals completed! 🐙 have h_pos_tendsto : Tendsto (fun n ↦ ∫⁻ x, posPart (F n) x) atTop (nhds (∫⁻ x, posPart f x)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) All goals completed! 🐙 have h_neg_tendsto : Tendsto (fun n ↦ ∫⁻ x, negPart (F n) x) atTop (nhds (∫⁻ x, negPart f x)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (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)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (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)) := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) All goals completed! 🐙 F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : ℝ), Tendsto (fun n => posPart (F n) x) atTop (𝓝 (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))h_neg_lim:∀ (x : ℝ), Tendsto (fun n => negPart (F n) x) atTop (𝓝 (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 : ℝ), posPart (F n) x) atTop (𝓝 (∫⁻ (x : ℝ), posPart f x)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_posPart (hF_meas n)) (fun n x => le_trans (posPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) h_bound_ne_top h_pos_limh_neg_tendsto:Tendsto (fun n => ∫⁻ (x : ℝ), negPart (F n) x) atTop (𝓝 (∫⁻ (x : ℝ), negPart f x)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_negPart (hF_meas n)) (fun n x => le_trans (negPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) h_bound_ne_top h_neg_limh_pos_toReal:Tendsto (fun n => (∫⁻ (x : ℝ), posPart (F n) x).toReal) atTop (𝓝 (∫⁻ (x : ℝ), posPart f x).toReal) := Tendsto.comp (tendsto_toReal (Integrable.posPart_ne_top hf_int)) h_pos_tendstoh_neg_toReal:Tendsto (fun n => (∫⁻ (x : ℝ), negPart (F n) x).toReal) atTop (𝓝 (∫⁻ (x : ℝ), negPart f x).toReal) := Tendsto.comp (tendsto_toReal (Integrable.negPart_ne_top hf_int)) h_neg_tendsto⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 ((∫⁻ (x : ℝ), posPart f x).toReal - (∫⁻ (x : ℝ), negPart f x).toReal)) have hF_eq : (fun n ↦ ∫ x, F n x) = fun n ↦ (∫⁻ x, posPart (F n) x).toReal - (∫⁻ x, negPart (F n) x).toReal := F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ Tendsto (fun n => ∫ (x : ℝ), F n x) atTop (𝓝 (∫ (x : ℝ), f x)) F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : ℝ), Tendsto (fun n => posPart (F n) x) atTop (𝓝 (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))h_neg_lim:∀ (x : ℝ), Tendsto (fun n => negPart (F n) x) atTop (𝓝 (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 : ℝ), posPart (F n) x) atTop (𝓝 (∫⁻ (x : ℝ), posPart f x)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_posPart (hF_meas n)) (fun n x => le_trans (posPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) h_bound_ne_top h_pos_limh_neg_tendsto:Tendsto (fun n => ∫⁻ (x : ℝ), negPart (F n) x) atTop (𝓝 (∫⁻ (x : ℝ), negPart f x)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_negPart (hF_meas n)) (fun n x => le_trans (negPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) h_bound_ne_top h_neg_limh_pos_toReal:Tendsto (fun n => (∫⁻ (x : ℝ), posPart (F n) x).toReal) atTop (𝓝 (∫⁻ (x : ℝ), posPart f x).toReal) := Tendsto.comp (tendsto_toReal (Integrable.posPart_ne_top hf_int)) h_pos_tendstoh_neg_toReal:Tendsto (fun n => (∫⁻ (x : ℝ), negPart (F n) x).toReal) atTop (𝓝 (∫⁻ (x : ℝ), negPart f x).toReal) := Tendsto.comp (tendsto_toReal (Integrable.negPart_ne_top hf_int)) h_neg_tendston:ℕ⊢ ∫ (x : ℝ), F n x = (∫⁻ (x : ℝ), posPart (F n) x).toReal - (∫⁻ (x : ℝ), negPart (F n) x).toReal All goals completed! 🐙 F:ℕ → ℝ → ℝf:ℝ → ℝbound:ℝ → ℝhF_meas:∀ (n : ℕ), MeasurableFun (F n)h_bound_int:Integrable boundh_bound:∀ (n : ℕ) (x : ℝ), |F n x| ≤ bound xh_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))h_bound_nonneg:∀ (x : ℝ), 0 ≤ bound x := fun x => le_trans (abs_nonneg (F 0 x)) (h_bound 0 x)h_bound_ne_top:∫⁻ (x : ℝ), ENNReal.ofReal (bound x) ≠ ∞ := have habs := funext fun x => of_eq_true (Eq.trans (congrFun' (congrArg Eq (congrArg ENNReal.ofReal (abs_of_nonneg (h_bound_nonneg x)))) (ENNReal.ofReal (bound x))) (eq_self (ENNReal.ofReal (bound x)))); id (Eq.mp (congrFun' (congrArg Ne (congrArg lintegral habs)) ∞) (HasFiniteIntegral.ne_top h_bound_int.hasFiniteIntegral))hf_meas:MeasurableFun f := measurableFun_of_tendsto hF_meas h_limh_abs_f_le:∀ (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 h_bound_ne_top (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 h_bound_ne_top (lintegral_mono fun x => ofReal_le_ofReal (h_abs_f_le x))) }h_pos_lim:∀ (x : ℝ), Tendsto (fun n => posPart (F n) x) atTop (𝓝 (posPart f x)) := fun x => id (Tendsto.comp (Continuous.tendsto continuous_ofReal (f x)) (h_lim x))h_neg_lim:∀ (x : ℝ), Tendsto (fun n => negPart (F n) x) atTop (𝓝 (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 : ℝ), posPart (F n) x) atTop (𝓝 (∫⁻ (x : ℝ), posPart f x)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_posPart (hF_meas n)) (fun n x => le_trans (posPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) h_bound_ne_top h_pos_limh_neg_tendsto:Tendsto (fun n => ∫⁻ (x : ℝ), negPart (F n) x) atTop (𝓝 (∫⁻ (x : ℝ), negPart f x)) := tendsto_lintegral_of_dominated_convergence (fun x => ENNReal.ofReal (bound x)) (fun n => measurable_negPart (hF_meas n)) (fun n x => le_trans (negPart_le_abs x) (ofReal_le_ofReal (h_bound n x))) h_bound_ne_top h_neg_limh_pos_toReal:Tendsto (fun n => (∫⁻ (x : ℝ), posPart (F n) x).toReal) atTop (𝓝 (∫⁻ (x : ℝ), posPart f x).toReal) := Tendsto.comp (tendsto_toReal (Integrable.posPart_ne_top hf_int)) h_pos_tendstoh_neg_toReal:Tendsto (fun n => (∫⁻ (x : ℝ), negPart (F n) x).toReal) atTop (𝓝 (∫⁻ (x : ℝ), negPart f x).toReal) := Tendsto.comp (tendsto_toReal (Integrable.negPart_ne_top hf_int)) h_neg_tendstohF_eq:(fun n => ∫ (x : ℝ), F n x) = fun n => (∫⁻ (x : ℝ), posPart (F n) x).toReal - (∫⁻ (x : ℝ), negPart (F n) x).toReal := funext fun n => Eq.mpr (id (congrArg (fun _a => _a = (∫⁻ (x : ℝ), posPart (F n) x).toReal - (∫⁻ (x : ℝ), negPart (F n) x).toReal) (integral_eq_lintegral_posPart_sub_lintegral_negPart (hF_int n)))) (Eq.refl ((∫⁻ (x : ℝ), posPart (F n) x).toReal - (∫⁻ (x : ℝ), negPart (F n) x).toReal))⊢ Tendsto (fun n => (∫⁻ (x : ℝ), posPart (F n) x).toReal - (∫⁻ (x : ℝ), negPart (F n) x).toReal) atTop (𝓝 ((∫⁻ (x : ℝ), posPart f x).toReal - (∫⁻ (x : ℝ), negPart f x).toReal)) All goals completed! 🐙