測度論と積分

3.2. 実数直線上の非負関数の積分🔗

定義.

f : \mathbb{R} \to [0,\infty] を関数とする。 f が 可測 であるとは、任意の a \in [0,\infty] に対して \{x \in \mathbb{R} \mid a \le f(x)\} が可測であることをいう。

Lean code
/-- Measurability for nonnegative functions on `ℝ`, expressed through superlevel sets. -/ def Measurable (f : ℝ → ℝ≥0∞) : Prop := ∀ a : ℝ≥0∞, MeasurableSet {x | a ≤ f x}
補題.

非負有理数の列挙 q : \mathbb{N} \to \mathbb{Q}_{\ge 0} を固定する。 関数 f : \mathbb{R} \to [0,\infty] と n \in \mathbb{N} に対して、 \approxFun_n f : \mathbb{R} \to [0,\infty] を (\approxFun_n f)(x) \coloneqq \max_{\substack{0 \le i < n \\ q_i \le f(x)}} q_i で定める。このとき次が成り立つ。

  1. 任意の n に対して、\approxFun_n f は単関数である。

  2. i \le j ならば \approxFun_i f \le \approxFun_j f である。

  3. f が可測ならば、任意の x \in \mathbb{R} に対して \sup_{n \in \mathbb{N}} (\approxFun_n f)(x) = f(x) である。

Lean code
/-- A sequence enumerating the nonnegative rational numbers in `ℝ≥0∞`. -/ def ennrealRatEmbed (n : ℕ) : ℝ≥0∞ := ENNReal.ofReal ((Encodable.decode (α := ℚ) n).getD (0 : ℚ))
/-- Rational-valued simple approximations of a measurable function. -/ def eapprox (f : ℝ → ℝ≥0∞) (n : ℕ) : SimpleFunc := (Finset.range n).sup fun k ↦ restrict (const (ennrealRatEmbed k)) {x : ℝ | ennrealRatEmbed k ≤ f x}
@[gcongr, mono] theorem monotone_eapprox (f : ℝ → ℝ≥0∞) : Monotone (eapprox f) := f:ℝ → ℝ≥0∞⊢ Monotone (eapprox f) intro i f:ℝ → ℝ≥0∞i:ℕj:ℕ⊢ i ≤ j → eapprox f i ≤ eapprox f j f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ j⊢ eapprox f i ≤ eapprox f j f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ j⊢ ∀ b ∈ Finset.range i, (const (ennrealRatEmbed b)).restrict {x | ennrealRatEmbed b ≤ f x} ≤ eapprox f j intro k f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ jk:ℕhk:k ∈ Finset.range i⊢ (const (ennrealRatEmbed k)).restrict {x | ennrealRatEmbed k ≤ f x} ≤ eapprox f j f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ jk:ℕhk:k < i⊢ (const (ennrealRatEmbed k)).restrict {x | ennrealRatEmbed k ≤ f x} ≤ eapprox f j f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ jk:ℕhk:k < i⊢ k ∈ Finset.range jf:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ jk:ℕhk:k < i⊢ (const (ennrealRatEmbed k)).restrict {x | ennrealRatEmbed k ≤ f x} ≤ (const (ennrealRatEmbed k)).restrict {x | ennrealRatEmbed k ≤ f x} f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ jk:ℕhk:k < i⊢ k ∈ Finset.range j All goals completed! 🐙 f:ℝ → ℝ≥0∞i:ℕj:ℕhij:i ≤ jk:ℕhk:k < i⊢ (const (ennrealRatEmbed k)).restrict {x | ennrealRatEmbed k ≤ f x} ≤ (const (ennrealRatEmbed k)).restrict {x | ennrealRatEmbed k ≤ f x} All goals completed! 🐙
theorem iSup_eapprox_apply {f : ℝ → ℝ≥0∞} (hf : Measurable f) (x : ℝ) : ⨆ n, eapprox f n x = f x := f:ℝ → ℝ≥0∞hf:Measurable fx:ℝ⊢ ⨆ n, (eapprox f n) x = f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕ⊢ (eapprox f n) x ≤ f xf:ℝ → ℝ≥0∞hf:Measurable fx:ℝ⊢ f x ≤ ⨆ n, (eapprox f n) x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕ⊢ (eapprox f n) x ≤ f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕ⊢ ((Finset.range n).sup fun k => if ennrealRatEmbed k ≤ f x then ennrealRatEmbed k else 0) ≤ f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕk:ℕx✝:k ∈ Finset.range n⊢ (if ennrealRatEmbed k ≤ f x then ennrealRatEmbed k else 0) ≤ f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕk:ℕx✝:k ∈ Finset.range nhki:ennrealRatEmbed k ≤ f x⊢ ennrealRatEmbed k ≤ f xf:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕk:ℕx✝:k ∈ Finset.range nhki:¬ennrealRatEmbed k ≤ f x⊢ 0 ≤ f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕk:ℕx✝:k ∈ Finset.range nhki:ennrealRatEmbed k ≤ f x⊢ ennrealRatEmbed k ≤ f x All goals completed! 🐙 f:ℝ → ℝ≥0∞hf:Measurable fx:ℝn:ℕk:ℕx✝:k ∈ Finset.range nhki:¬ennrealRatEmbed k ≤ f x⊢ 0 ≤ f x All goals completed! 🐙 f:ℝ → ℝ≥0∞hf:Measurable fx:ℝ⊢ f x ≤ ⨆ n, (eapprox f n) x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝ⊢ ¬⨆ n, (eapprox f n) x < f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f x⊢ False f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f x⊢ False have hq : (Real.toNNReal q : ℝ≥0∞) ≤ ⨆ n, eapprox f n x := f:ℝ → ℝ≥0∞hf:Measurable fx:ℝ⊢ ⨆ n, (eapprox f n) x = f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f x⊢ ↑(↑q).toNNReal ≤ (eapprox f (Encodable.encode q + 1)) x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f x⊢ ↑(↑q).toNNReal ≤ (Finset.range (Encodable.encode q + 1)).sup fun k => if ennrealRatEmbed k ≤ f x then ennrealRatEmbed k else 0 f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f xhk_mem:Encodable.encode q ∈ Finset.range (Encodable.encode q + 1) := Finset.mem_range.mpr (Nat.lt_succ_self (Encodable.encode q))⊢ ↑(↑q).toNNReal ≤ (Finset.range (Encodable.encode q + 1)).sup fun k => if ennrealRatEmbed k ≤ f x then ennrealRatEmbed k else 0 f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f xhk_mem:Encodable.encode q ∈ Finset.range (Encodable.encode q + 1) := Finset.mem_range.mpr (Nat.lt_succ_self (Encodable.encode q))⊢ ↑(↑q).toNNReal ≤ if ennrealRatEmbed (Encodable.encode q) ≤ f x then ennrealRatEmbed (Encodable.encode q) else 0 f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f xhk_mem:Encodable.encode q ∈ Finset.range (Encodable.encode q + 1) := Finset.mem_range.mpr (Nat.lt_succ_self (Encodable.encode q))⊢ ↑(↑q).toNNReal ≤ ennrealRatEmbed (Encodable.encode q)f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f xhk_mem:Encodable.encode q ∈ Finset.range (Encodable.encode q + 1) := Finset.mem_range.mpr (Nat.lt_succ_self (Encodable.encode q))⊢ ennrealRatEmbed (Encodable.encode q) ≤ f x f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f xhk_mem:Encodable.encode q ∈ Finset.range (Encodable.encode q + 1) := Finset.mem_range.mpr (Nat.lt_succ_self (Encodable.encode q))⊢ ↑(↑q).toNNReal ≤ ennrealRatEmbed (Encodable.encode q) All goals completed! 🐙 f:ℝ → ℝ≥0∞hf:Measurable fx:ℝh:⨆ n, (eapprox f n) x < f xq:ℚleft✝:0 ≤ qhlt_q:⨆ n, (eapprox f n) x < ↑(↑q).toNNRealhq_lt:↑(↑q).toNNReal < f xhk_mem:Encodable.encode q ∈ Finset.range (Encodable.encode q + 1) := Finset.mem_range.mpr (Nat.lt_succ_self (Encodable.encode q))⊢ ennrealRatEmbed (Encodable.encode q) ≤ f x All goals completed! 🐙 All goals completed! 🐙
定義.

f : \mathbb{R} \to [0,\infty] を関数とする。 f の 下ルベーグ積分 を \underline{\int}_{x \in \mathbb{R}} f(x)\,dx \coloneqq \sup_{\substack{g : \mathbb{R} \to [0,\infty],\\ \text{$g$ is simple},\, g \le f}} \Simp \int_{x \in \mathbb{R}} g(x)\,dx で定める。

Lean code
/-- Lower Lebesgue integral on `ℝ`. -/ noncomputable def lintegral (f : ℝ → ℝ≥0∞) : ℝ≥0∞ := ⨆ (g : SimpleFunc) (_ : ⇑g ≤ f), g.lintegral
補題.

f : \mathbb{R} \to [0,\infty] を単関数とする。 このとき \underline{\int}_{x \in \mathbb{R}} f(x)\,dx = \Simp \int_{x \in \mathbb{R}} f(x)\,dx が成り立つ。

Lean code
theorem lintegral_eq_lintegral (f : SimpleFunc) : ∫⁻ x, f x = f.lintegral := f:SimpleFunc⊢ ∫⁻ (x : ℝ), f x = f.lintegral All goals completed! 🐙
補題.

下ルベーグ積分の定義では、値が \mathbb{R}_{\ge 0} に入る単関数だけを考えれば十分である。 より正確には、 \underline{\int}_{x \in \mathbb{R}} f(x)\,dx = \sup_{\substack{g : \mathbb{R} \to \mathbb{R}_{\ge 0},\\ \text{$g$ is simple},\, g \le f}} \Simp \int_{x \in \mathbb{R}} g(x)\,dx が成り立つ。

Lean code
/-- It suffices to take the supremum over finite-valued simple functions. -/ theorem lintegral_eq_nnreal (f : ℝ → ℝ≥0∞) : ∫⁻ x, f x = ⨆ (g : SimpleFunc) (_ : ∀ x, g x ≤ f x) (_ : ∀ x, g x ≠ ∞), g.lintegral := f:ℝ → ℝ≥0∞⊢ ∫⁻ (x : ℝ), f x = ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral = ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f x⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegralf:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) g⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ g.lintegral ≤ ⨆ (_ : ∀ (x : ℝ), ψ x ≠ ∞), ψ.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)x:ℝ⊢ ψ x ≠ ∞f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ g.lintegral ≤ ψ.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)x:ℝ⊢ ψ x ≠ ∞ All goals completed! 🐙 f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ g.lintegral ≤ ψ.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ ψ.lintegral = g.lintegral calc ψ.lintegral = ψ.lintegralIn univ := f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ ψ.lintegral = ψ.lintegralIn univ All goals completed! 🐙 _ = ∑ y ∈ g.range, ENNReal.ofReal (ENNReal.toReal y) * measure (g ⁻¹' {y}) := f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ ψ.lintegralIn univ = ∑ y ∈ g.range, ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) All goals completed! 🐙 _ = ∑ y ∈ g.range, y * measure (g ⁻¹' {y}) := f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ ∑ y ∈ g.range, ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) = ∑ y ∈ g.range, y * measure (⇑g ⁻¹' {y}) f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)y:ℝ≥0∞x✝:y ∈ g.range⊢ ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) = y * measure (⇑g ⁻¹' {y}) f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)y:ℝ≥0∞x✝:y ∈ g.rangehy:y = ∞⊢ ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) = y * measure (⇑g ⁻¹' {y})f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)y:ℝ≥0∞x✝:y ∈ g.rangehy:¬y = ∞⊢ ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) = y * measure (⇑g ⁻¹' {y}) f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)y:ℝ≥0∞x✝:y ∈ g.rangehy:y = ∞⊢ ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) = y * measure (⇑g ⁻¹' {y}) f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)x✝:∞ ∈ g.range⊢ ENNReal.ofReal ∞.toReal * measure (⇑g ⁻¹' {∞}) = ∞ * measure (⇑g ⁻¹' {∞}) All goals completed! 🐙 f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)y:ℝ≥0∞x✝:y ∈ g.rangehy:¬y = ∞⊢ ENNReal.ofReal y.toReal * measure (⇑g ⁻¹' {y}) = y * measure (⇑g ⁻¹' {y}) All goals completed! 🐙 _ = g.lintegral := f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:measure (⇑g ⁻¹' {∞}) = 0ψ:SimpleFunc := SimpleFunc.map (ENNReal.ofReal ∘ ENNReal.toReal) ghψ:∀ (x : ℝ), ψ x ≤ f x := fun x => le_trans ofReal_toReal_le (hg x)⊢ ∑ y ∈ g.range, y * measure (⇑g ⁻¹' {y}) = g.lintegral All goals completed! 🐙 f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0⊢ g.lintegral ≤ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞⊢ ∃ i, b < ⨆ (_ : ∀ (x : ℝ), i x ≤ f x), ⨆ (_ : ∀ (x : ℝ), i x ≠ ∞), i.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})⊢ ∃ i, b < ⨆ (_ : ∀ (x : ℝ), i x ≤ f x), ⨆ (_ : ∀ (x : ℝ), i x ≠ ∞), i.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})⊢ ∃ i, b < ⨆ (_ : ∀ (x : ℝ), i x ≤ f x), ⨆ (_ : ∀ (x : ℝ), i x ≠ ∞), i.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞⊢ ∃ i, b < ⨆ (_ : ∀ (x : ℝ), i x ≤ f x), ⨆ (_ : ∀ (x : ℝ), i x ≠ ∞), i.lintegral have hψ : ∀ x, ψ x ≤ f x := f:ℝ → ℝ≥0∞⊢ ∫⁻ (x : ℝ), f x = ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞x:ℝ⊢ ψ x ≤ f x f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞x:ℝhx:x ∈ ⇑g ⁻¹' {∞}⊢ ψ x ≤ f xf:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞x:ℝhx:x ∉ ⇑g ⁻¹' {∞}⊢ ψ x ≤ f x f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞x:ℝhx:x ∈ ⇑g ⁻¹' {∞}⊢ ψ x ≤ f x have hfx : f x = ∞ := f:ℝ → ℝ≥0∞⊢ ∫⁻ (x : ℝ), f x = ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞x:ℝhx:g x = ∞⊢ f x = ∞ All goals completed! 🐙 All goals completed! 🐙 f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞x:ℝhx:x ∉ ⇑g ⁻¹' {∞}⊢ ψ x ≤ f x All goals completed! 🐙 have hψ_int : ψ.lintegral = n * measure (g ⁻¹' {∞}) := f:ℝ → ℝ≥0∞⊢ ∫⁻ (x : ℝ), f x = ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ f x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral All goals completed! 🐙 f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)⊢ ∃ i, (∀ (x : ℝ), i x ≤ f x) ∧ (∀ (x : ℝ), i x ≠ ∞) ∧ b < i.lintegral refine ⟨ψ, hψ, ?_, f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)⊢ b < ψ.lintegral All goals completed! 🐙⟩ f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)x:ℝ⊢ ψ x ≠ ∞ f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)x:ℝhx:x ∈ ⇑g ⁻¹' {∞}⊢ ψ x ≠ ∞f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)x:ℝhx:x ∉ ⇑g ⁻¹' {∞}⊢ ψ x ≠ ∞ f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)x:ℝhx:x ∈ ⇑g ⁻¹' {∞}⊢ ψ x ≠ ∞ All goals completed! 🐙 f:ℝ → ℝ≥0∞g:SimpleFunchg:⇑g ≤ fun x => f xh:¬measure (⇑g ⁻¹' {∞}) = 0b:ℝ≥0∞hb:b < ∞n:ℕhn:b < ↑n * measure (⇑g ⁻¹' {∞})ψ:SimpleFunc := (SimpleFunc.const ↑n).restrict (⇑g ⁻¹' {∞})hs:MeasurableSet (⇑g ⁻¹' {∞}) := measurableSet_fiber g ∞hψ:∀ (x : ℝ), ψ x ≤ f x := fun x => if hx : x ∈ ⇑g ⁻¹' {∞} then have hfx := top_le_iff.mp (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx ▸ hg x); of_eq_true (Eq.trans (congr (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_mem hx (Function.const ℝ ↑n))))) hfx) le_top._simp_2) else of_eq_true (Eq.trans (congrFun' (congrArg LE.le (Eq.trans (congrFun (coe_restrict (SimpleFunc.const ↑n) hs) x) (Eq.trans (congrFun' (congrArg (⇑g ⁻¹' {∞}).indicator (coe_const ↑n)) x) (indicator_of_notMem (of_eq_true (Eq.trans (congrArg Not (eq_false hx)) not_false_eq_true)) (Function.const ℝ ↑n))))) (f x)) (one_le._simp_3 (f x)))hψ_int:ψ.lintegral = ↑n * measure (⇑g ⁻¹' {∞}) := id (restrict_const_lintegral (↑n) hs)x:ℝhx:x ∉ ⇑g ⁻¹' {∞}⊢ ψ x ≠ ∞ All goals completed! 🐙
定理 (単調収束定理).

f_0, f_1, \dots : \mathbb{R} \to [0,\infty] を可測関数の列とする。 n \le m ならば f_n \le f_m であると仮定する。 このとき \underline{\int}_{x \in \mathbb{R}} \sup_{n \in \mathbb{N}} f_n(x)\,dx = \sup_{n \in \mathbb{N}} \underline{\int}_{x \in \mathbb{R}} f_n(x)\,dx. が成り立つ。

Lean code
theorem iSup_lintegral_le {ι : Sort*} (f : ι → ℝ → ℝ≥0∞) : ⨆ i, ∫⁻ x, f i x ≤ ∫⁻ x, ⨆ i, f i x := ι:Sort u_1f:ι → ℝ → ℝ≥0∞⊢ ⨆ i, ∫⁻ (x : ℝ), f i x ≤ ∫⁻ (x : ℝ), ⨆ i, f i x ι:Sort u_1f:ι → ℝ → ℝ≥0∞i:ι⊢ ∫⁻ (x : ℝ), f i x ≤ ∫⁻ (x : ℝ), ⨆ i, f i x All goals completed! 🐙
theorem lintegral_iSup {f : ℕ → ℝ → ℝ≥0∞} (hf : ∀ n, Measurable (f n)) (h_mono : Monotone f) : ∫⁻ x, ⨆ n, f n x = ⨆ n, ∫⁻ x, f n x := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone f⊢ ∫⁻ (x : ℝ), ⨆ n, f n x = ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n x⊢ lintegral F = ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n x⊢ lintegral F ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n x⊢ ⨆ g, ⨆ (_ : ∀ (x : ℝ), g x ≤ ⨆ n, f n x), ⨆ (_ : ∀ (x : ℝ), g x ≠ ∞), g.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞⊢ s.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞a:ℝ≥0∞ha:a < 1⊢ a * s.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1⊢ ↑r * s.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) s⊢ ↑r * s.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfl⊢ ↑r * s.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x have eq : ∀ p, rs ⁻¹' {p} = ⋃ n, rs ⁻¹' {p} ∩ {x | p ≤ f n x} := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone f⊢ ∫⁻ (x : ℝ), ⨆ n, f n x = ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞⊢ ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞⊢ ⇑rs ⁻¹' {p} = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x} nth_rw 1 [← inter_univ (rs ⁻¹' {p})f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞⊢ ⇑rs ⁻¹' {p} ∩ univ = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞x:ℝhx:x ∈ ⇑rs ⁻¹' {p}⊢ x ∈ ⋃ i, {x | p ≤ f i x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞x:ℝhx:x ∈ ⇑rs ⁻¹' {p}hp:p = 0⊢ x ∈ ⋃ i, {x | p ≤ f i x}f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞x:ℝhx:x ∈ ⇑rs ⁻¹' {p}hp:¬p = 0⊢ x ∈ ⋃ i, {x | p ≤ f i x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞x:ℝhx:x ∈ ⇑rs ⁻¹' {p}hp:p = 0⊢ x ∈ ⋃ i, {x | p ≤ f i x} All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflp:ℝ≥0∞x:ℝhp:¬p = 0hx:rs x = p⊢ x ∈ ⋃ i, {x | p ≤ f i x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0⊢ x ∈ ⋃ i, {x_1 | rs x ≤ f i x_1} have hne : r * s x ≠ 0 := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone f⊢ ∫⁻ (x : ℝ), ⨆ n, f n x = ⨆ n, ∫⁻ (x : ℝ), f n x rwa [Nef:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0⊢ ¬↑r * s x = 0 f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0hne:↑r * s x ≠ 0 := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hphsx_ne:s x ≠ 0 := right_ne_zero_of_mul hne⊢ x ∈ ⋃ i, {x_1 | rs x ≤ f i x_1} have hsx_lt : rs x < ⨆ n : ℕ, f n x := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone f⊢ ∫⁻ (x : ℝ), ⨆ n, f n x = ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0hne:↑r * s x ≠ 0 := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hphsx_ne:s x ≠ 0 := right_ne_zero_of_mul hne⊢ rs x < s x suffices r * s x < 1 * s x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0hne:↑r * s x ≠ 0 := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hphsx_ne:s x ≠ 0 := right_ne_zero_of_mul hnethis:↑r * s x < 1 * s x := ?m.250⊢ rs x < s x All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0hne:↑r * s x ≠ 0 := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hphsx_ne:s x ≠ 0 := right_ne_zero_of_mul hne⊢ s x ≠ ∞ All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rflx:ℝhp:¬rs x = 0hne:↑r * s x ≠ 0 := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hphsx_ne:s x ≠ 0 := right_ne_zero_of_mul hnehsx_lt:rs x < ⨆ n, f n x := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x)n:ℕhn:rs x < f n x⊢ x ∈ ⋃ i, {x_1 | rs x ≤ f i x_1} All goals completed! 🐙 have mono : ∀ p : ℝ≥0∞, Monotone fun n ↦ rs ⁻¹' {p} ∩ {x | p ≤ f n x} := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone f⊢ ∫⁻ (x : ℝ), ⨆ n, f n x = ⨆ n, ∫⁻ (x : ℝ), f n x intro p f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))p:ℝ≥0∞i:ℕ⊢ ∀ ⦃b : ℕ⦄, i ≤ b → (fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) i ≤ (fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) b f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))p:ℝ≥0∞i:ℕj:ℕ⊢ i ≤ j → (fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) i ≤ (fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) j f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))p:ℝ≥0∞i:ℕj:ℕhij:i ≤ j⊢ (fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) i ≤ (fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) j f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))p:ℝ≥0∞i:ℕj:ℕhij:i ≤ j⊢ {x | p ≤ f i x} ⊆ {x | p ≤ f j x} intro x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))p:ℝ≥0∞i:ℕj:ℕhij:i ≤ jx:ℝhx:x ∈ {x | p ≤ f i x}⊢ x ∈ {x | p ≤ f j x} All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ↑r * s.lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x calc (r : ℝ≥0∞) * s.lintegral = ((const r) * s).lintegral := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ↑r * s.lintegral = (SimpleFunc.const ↑r * s).lintegral All goals completed! 🐙 _ = ∑ p ∈ rs.range, p * measure (rs ⁻¹' {p}) := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ (SimpleFunc.const ↑r * s).lintegral = ∑ p ∈ rs.range, p * measure (⇑rs ⁻¹' {p}) f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ (SimpleFunc.const ↑r * s).lintegral = ∑ p ∈ (SimpleFunc.const ↑r * s).range, p * measure (⇑(SimpleFunc.const ↑r * s) ⁻¹' {p}) All goals completed! 🐙 _ = ∑ p ∈ rs.range, p * measure (⋃ n, rs ⁻¹' {p} ∩ {x | p ≤ f n x}) := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ∑ p ∈ rs.range, p * measure (⇑rs ⁻¹' {p}) = ∑ p ∈ rs.range, p * measure (⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) refine Finset.sum_congr rfl fun p _ ↦ f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)p:ℝ≥0∞x✝:p ∈ rs.range⊢ p * measure (⇑rs ⁻¹' {p}) = p * measure (⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) All goals completed! 🐙 _ = ∑ p ∈ rs.range, ⨆ n, p * measure (rs ⁻¹' {p} ∩ {x | p ≤ f n x}) := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ∑ p ∈ rs.range, p * measure (⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) = ∑ p ∈ rs.range, ⨆ n, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) refine Finset.sum_congr rfl fun p _ ↦ f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)p:ℝ≥0∞x✝:p ∈ rs.range⊢ p * measure (⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) = ⨆ n, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) All goals completed! 🐙 _ = ⨆ n, ∑ p ∈ rs.range, p * measure (rs ⁻¹' {p} ∩ {x | p ≤ f n x}) := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ∑ p ∈ rs.range, ⨆ n, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) = ⨆ n, ∑ p ∈ rs.range, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)p:ℝ≥0∞i:ℕj:ℕhij:i ≤ j⊢ p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f i x}) ≤ p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f j x}) All goals completed! 🐙 _ ≤ ⨆ n, (rs.restrict {x | rs x ≤ f n x}).lintegral := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ⨆ n, ∑ p ∈ rs.range, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) ≤ ⨆ n, (rs.restrict {x | rs x ≤ f n x}).lintegral f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕ⊢ ∑ p ∈ rs.range, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) ≤ (rs.restrict {x | rs x ≤ f n x}).lintegral f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕ⊢ ∑ p ∈ rs.range, p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) ≤ rs.lintegralIn {x | rs x ≤ f n x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕp:ℝ≥0∞x✝:p ∈ rs.range⊢ p * measure (⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x}) = p * measure (⇑rs ⁻¹' {p} ∩ {x | rs x ≤ f n x}) f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕp:ℝ≥0∞x✝:p ∈ rs.rangex:ℝ⊢ x ∈ ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} ↔ x ∈ ⇑rs ⁻¹' {p} ∩ {x | rs x ≤ f n x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕp:ℝ≥0∞x✝:p ∈ rs.rangex:ℝhx:x ∈ ⇑rs ⁻¹' {p}⊢ x ∈ {x | p ≤ f n x} ↔ x ∈ {x | rs x ≤ f n x} f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕp:ℝ≥0∞x✝:p ∈ rs.rangex:ℝhx:rs x = p⊢ x ∈ {x | p ≤ f n x} ↔ x ∈ {x | rs x ≤ f n x} All goals completed! 🐙 _ ≤ ⨆ n, ∫⁻ x, f n x := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ⨆ n, (rs.restrict {x | rs x ≤ f n x}).lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕ⊢ (rs.restrict {x | rs x ≤ f n x}).lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕ⊢ (rs.restrict {x | rs x ≤ f n x}).lintegral ≤ ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}⊢ (rs.restrict {x | rs x ≤ f n x}).lintegral ≤ ∫⁻ (x : ℝ), f n x have ht : ∀ x, t x ≤ f n x := f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)⊢ ⨆ n, (rs.restrict {x | rs x ≤ f n x}).lintegral ≤ ⨆ n, ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝ⊢ t x ≤ f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝ⊢ (rs.restrict {x | rs x ≤ f n x}) x ≤ f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝ⊢ {x | rs x ≤ f n x}.indicator (⇑rs) x ≤ f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝhx:rs x ≤ f n x⊢ {x | rs x ≤ f n x}.indicator (⇑rs) x ≤ f n xf:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝhx:¬rs x ≤ f n x⊢ {x | rs x ≤ f n x}.indicator (⇑rs) x ≤ f n x f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝhx:rs x ≤ f n x⊢ {x | rs x ≤ f n x}.indicator (⇑rs) x ≤ f n x All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞hf:∀ (n : ℕ), Measurable (f n)h_mono:Monotone fF:ℝ → ℝ≥0∞ := fun x => ⨆ n, f n xs:SimpleFunchsf:∀ (x : ℝ), s x ≤ ⨆ n, f n xhsfin:∀ (x : ℝ), s x ≠ ∞r:ℝ≥0right✝:↑r < 1ha:↑r < 1rs:SimpleFunc := SimpleFunc.map (fun y => ↑r * y) seq_rs:rs = SimpleFunc.const ↑r * s := rfleq:∀ (p : ℝ≥0∞), ⇑rs ⁻¹' {p} = ⋃ n, ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p => Eq.mpr (id (congrArg (fun _a => ⇑rs ⁻¹' {p} = _a) (Eq.symm (inter_iUnion (⇑rs ⁻¹' {p}) fun n => {x | p ≤ f n x})))) (Eq.mpr (id (congrArg (fun _a => _a = ⇑rs ⁻¹' {p} ∩ ⋃ i, {x | p ≤ f i x}) (Eq.symm (inter_univ (⇑rs ⁻¹' {p}))))) (Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff (x ∈ ⋃ i, {x | p ≤ f i x}))).mpr (if hp : p = 0 then of_eq_true (Eq.trans (Eq.trans (congrFun' (congrArg Membership.mem (congrArg iUnion (funext fun i => congrArg setOf (funext fun x => Eq.trans (congrFun' (congrArg LE.le hp) (f i x)) (one_le._simp_3 (f i x)))))) x) mem_iUnion._simp_1) (Eq.trans (congrArg Exists (funext fun i => mem_univ._simp_1 x)) (exists_const._simp_1 ℕ))) else Eq.ndrec (motive := fun p => ¬p = 0 → x ∈ ⋃ i, {x | p ≤ f i x}) (fun hp => have hne := Eq.mpr (id (congrArg (fun _a => _a) (Ne.eq_1 (↑r * s x) 0))) hp; have hsx_ne := right_ne_zero_of_mul hne; have hsx_lt := lt_of_lt_of_le (have this := ENNReal.mul_lt_mul_left (ne_of_gt (lt_of_le_of_ne' (zero_le (s x)) hsx_ne)) (hsfin x) right✝; Eq.mpr (id (Eq.trans (congrFun' (congrArg LT.lt (Eq.trans (congrFun' (congrArg DFunLike.coe eq_rs) x) (congrFun' (congrFun' (congrArg HMul.hMul (coe_const ↑r)) ⇑s) x))) (s x)) gt_iff_lt._simp_1)) (Eq.mp (congrArg (LT.lt (↑r * s x)) (one_mul (s x))) this)) (hsf x); Exists.casesOn (lt_iSup_iff.mp hsx_lt) fun n hn => mem_iUnion.mpr (Exists.intro n (le_of_lt hn))) (Eq.mp (Eq.trans lintegral_eq_nnreal._simp_2 lintegral_eq_nnreal._simp_3) hx) hp)))mono:∀ (p : ℝ≥0∞), Monotone fun n => ⇑rs ⁻¹' {p} ∩ {x | p ≤ f n x} := fun p ⦃i j⦄ hij => inter_subset_inter_right (⇑rs ⁻¹' {p}) fun ⦃x⦄ hx => le_trans hx (h_mono hij x)h_meas:∀ (n : ℕ), MeasurableSet {x | rs x ≤ f n x} := fun n => measurableSet_le rs (hf n)n:ℕt:SimpleFunc := rs.restrict {x | rs x ≤ f n x}x:ℝhx:¬rs x ≤ f n x⊢ {x | rs x ≤ f n x}.indicator (⇑rs) x ≤ f n x All goals completed! 🐙 All goals completed! 🐙
定理.

f, g : \mathbb{R} \to [0,\infty] を可測関数とする。 このとき \underline{\int}_{x \in \mathbb{R}} (f(x) + g(x))\,dx = \underline{\int}_{x \in \mathbb{R}} f(x)\,dx + \underline{\int}_{x \in \mathbb{R}} g(x)\,dx. が成り立つ。

Lean code
theorem lintegral_add {f g : ℝ → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) : ∫⁻ x, f x + g x = (∫⁻ x, f x) + (∫⁻ x, g x) := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : ℝ), f x + g x = (∫⁻ (x : ℝ), f x) + ∫⁻ (x : ℝ), g x calc ∫⁻ x, f x + g x = (∫⁻ x, (⨆ n, (eapprox f n : ℝ → ℝ≥0∞) x) + ⨆ n, (eapprox g n : ℝ → ℝ≥0∞) x) := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : ℝ), f x + g x = ∫⁻ (x : ℝ), (⨆ n, (eapprox f n) x) + ⨆ n, (eapprox g n) x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (x : ℝ), f x + g x = (⨆ n, (eapprox f n) x) + ⨆ n, (eapprox g n) x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ f x + g x = (⨆ n, (eapprox f n) x) + ⨆ n, (eapprox g n) x All goals completed! 🐙 _ = (∫⁻ x, ⨆ n, (eapprox f n + eapprox g n : SimpleFunc) x) := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : ℝ), (⨆ n, (eapprox f n) x) + ⨆ n, (eapprox g n) x = ∫⁻ (x : ℝ), ⨆ n, (eapprox f n + eapprox g n) x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (x : ℝ), (⨆ n, (eapprox f n) x) + ⨆ n, (eapprox g n) x = ⨆ n, (eapprox f n + eapprox g n) x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ (⨆ n, (eapprox f n) x) + ⨆ n, (eapprox g n) x = ⨆ n, (eapprox f n + eapprox g n) x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ ⨆ a, (eapprox f a) x + (eapprox g a) x = ⨆ n, (eapprox f n + eapprox g n) xf:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ Monotone fun n => (eapprox f n) xf:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ Monotone fun n => (eapprox g n) x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ ⨆ a, (eapprox f a) x + (eapprox g a) x = ⨆ n, (eapprox f n + eapprox g n) x All goals completed! 🐙 f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ Monotone fun n => (eapprox f n) x intro i f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝi:ℕj:ℕ⊢ i ≤ j → (fun n => (eapprox f n) x) i ≤ (fun n => (eapprox f n) x) j f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝi:ℕj:ℕhij:i ≤ j⊢ (fun n => (eapprox f n) x) i ≤ (fun n => (eapprox f n) x) j All goals completed! 🐙 f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝ⊢ Monotone fun n => (eapprox g n) x intro i f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝi:ℕj:ℕ⊢ i ≤ j → (fun n => (eapprox g n) x) i ≤ (fun n => (eapprox g n) x) j f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gx:ℝi:ℕj:ℕhij:i ≤ j⊢ (fun n => (eapprox g n) x) i ≤ (fun n => (eapprox g n) x) j All goals completed! 🐙 _ = ⨆ n, (eapprox f n).lintegral + (eapprox g n).lintegral := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∫⁻ (x : ℝ), ⨆ n, (eapprox f n + eapprox g n) x = ⨆ n, (eapprox f n).lintegral + (eapprox g n).lintegral f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ⨆ n, ∫⁻ (x : ℝ), (eapprox f n + eapprox g n) x = ⨆ n, (eapprox f n).lintegral + (eapprox g n).lintegralf:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n + eapprox g n)f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => ⇑(eapprox f n + eapprox g n) f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ⨆ n, ∫⁻ (x : ℝ), (eapprox f n + eapprox g n) x = ⨆ n, (eapprox f n).lintegral + (eapprox g n).lintegral f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gn:ℕ⊢ ∫⁻ (x : ℝ), (eapprox f n + eapprox g n) x = (eapprox f n).lintegral + (eapprox g n).lintegral calc (∫⁻ x, (eapprox f n + eapprox g n : SimpleFunc) x) = (eapprox f n + eapprox g n).lintegral := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gn:ℕ⊢ ∫⁻ (x : ℝ), (eapprox f n + eapprox g n) x = (eapprox f n + eapprox g n).lintegral All goals completed! 🐙 _ = (eapprox f n).lintegral + (eapprox g n).lintegral := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gn:ℕ⊢ (eapprox f n + eapprox g n).lintegral = (eapprox f n).lintegral + (eapprox g n).lintegral All goals completed! 🐙 f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ∀ (n : ℕ), Measurable ⇑(eapprox f n + eapprox g n) f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gn:ℕ⊢ Measurable ⇑(eapprox f n + eapprox g n) All goals completed! 🐙 f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => ⇑(eapprox f n + eapprox g n) intro i f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕ⊢ i ≤ j → (fun n => ⇑(eapprox f n + eapprox g n)) i ≤ (fun n => ⇑(eapprox f n + eapprox g n)) j f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕhij:i ≤ j⊢ (fun n => ⇑(eapprox f n + eapprox g n)) i ≤ (fun n => ⇑(eapprox f n + eapprox g n)) j f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕhij:i ≤ jx:ℝ⊢ (fun n => ⇑(eapprox f n + eapprox g n)) i x ≤ (fun n => ⇑(eapprox f n + eapprox g n)) j x All goals completed! 🐙 _ = (⨆ n, (eapprox f n).lintegral) + ⨆ n, (eapprox g n).lintegral := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ ⨆ n, (eapprox f n).lintegral + (eapprox g n).lintegral = (⨆ n, (eapprox f n).lintegral) + ⨆ n, (eapprox g n).lintegral f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => (eapprox f n).lintegralf:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => (eapprox g n).lintegral f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => (eapprox f n).lintegral intro i f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕ⊢ i ≤ j → (fun n => (eapprox f n).lintegral) i ≤ (fun n => (eapprox f n).lintegral) j f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕhij:i ≤ j⊢ (fun n => (eapprox f n).lintegral) i ≤ (fun n => (eapprox f n).lintegral) j All goals completed! 🐙 f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ Monotone fun n => (eapprox g n).lintegral intro i f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕ⊢ i ≤ j → (fun n => (eapprox g n).lintegral) i ≤ (fun n => (eapprox g n).lintegral) j f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable gi:ℕj:ℕhij:i ≤ j⊢ (fun n => (eapprox g n).lintegral) i ≤ (fun n => (eapprox g n).lintegral) j All goals completed! 🐙 _ = (∫⁻ x, f x) + (∫⁻ x, g x) := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable g⊢ (⨆ n, (eapprox f n).lintegral) + ⨆ n, (eapprox g n).lintegral = (∫⁻ (x : ℝ), f x) + ∫⁻ (x : ℝ), g x All goals completed! 🐙
定理.

f, g : \mathbb{R} \to [0,\infty] を可測関数とする。 g \le f かつ \underline{\int}_{x \in \mathbb{R}} g(x)\,dx < \infty と仮定する。 このとき \underline{\int}_{x \in \mathbb{R}} (f(x)-g(x))\,dx = \underline{\int}_{x \in \mathbb{R}} f(x)\,dx - \underline{\int}_{x \in \mathbb{R}} g(x)\,dx. が成り立つ。

Lean code
theorem lintegral_sub {f g : ℝ → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) (hg_fin : ∫⁻ x, g x ≠ ∞) (h_le : g ≤ f) : ∫⁻ x, f x - g x = (∫⁻ x, f x) - (∫⁻ x, g x) := f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable ghg_fin:∫⁻ (x : ℝ), g x ≠ ∞h_le:g ≤ f⊢ ∫⁻ (x : ℝ), f x - g x = (∫⁻ (x : ℝ), f x) - ∫⁻ (x : ℝ), g x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable ghg_fin:∫⁻ (x : ℝ), g x ≠ ∞h_le:g ≤ f⊢ (∫⁻ (x : ℝ), f x - g x) + ∫⁻ (x : ℝ), g x = ∫⁻ (x : ℝ), f x f:ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf:Measurable fhg:Measurable ghg_fin:∫⁻ (x : ℝ), g x ≠ ∞h_le:g ≤ f⊢ ∫⁻ (x : ℝ), f x - g x + g x = ∫⁻ (x : ℝ), f x All goals completed! 🐙
定理 (単調収束定理（減少列版）).

f_0, f_1, \dots : \mathbb{R} \to [0,\infty] を可測関数の減少列とする。 このとき \underline{\int}_{x \in \mathbb{R}} \inf_{n \in \mathbb{N}} f_n(x)\,dx \le \inf_{n \in \mathbb{N}} \underline{\int}_{x \in \mathbb{R}} f_n(x)\,dx. が成り立つ。 さらに \underline{\int}_{x \in \mathbb{R}} f_0(x)\,dx < \infty ならば \underline{\int}_{x \in \mathbb{R}} \inf_{n \in \mathbb{N}} f_n(x)\,dx = \inf_{n \in \mathbb{N}} \underline{\int}_{x \in \mathbb{R}} f_n(x)\,dx. が成り立つ。

Lean code
theorem le_iInf_lintegral {ι : Sort*} (f : ι → ℝ → ℝ≥0∞) : ∫⁻ x, ⨅ i, f i x ≤ ⨅ i, ∫⁻ x, f i x := ι:Sort u_1f:ι → ℝ → ℝ≥0∞⊢ ∫⁻ (x : ℝ), ⨅ i, f i x ≤ ⨅ i, ∫⁻ (x : ℝ), f i x ι:Sort u_1f:ι → ℝ → ℝ≥0∞i:ι⊢ ∫⁻ (x : ℝ), ⨅ i, f i x ≤ ∫⁻ (x : ℝ), f i x All goals completed! 🐙
theorem lintegral_iInf {f : ℕ → ℝ → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) (h_anti : Antitone f) (h_fin : ∫⁻ x, f 0 x ≠ ∞) : ∫⁻ x, ⨅ n, f n x = ⨅ n, ∫⁻ x, f n x := have fn_le_f0 : ∫⁻ x, ⨅ n, f n x ≤ ∫⁻ x, f 0 x := lintegral_mono fun _ ↦ iInf_le_of_le 0 le_rfl have fn_le_f0' : (⨅ n, ∫⁻ x, f n x) ≤ ∫⁻ x, f 0 x := iInf_le_of_le 0 le_rfl (ENNReal.sub_right_inj h_fin fn_le_f0 fn_le_f0').1 <| show (∫⁻ x, f 0 x) - (∫⁻ x, ⨅ n, f n x) = (∫⁻ x, f 0 x) - (⨅ n, ∫⁻ x, f n x) from calc (∫⁻ x, f 0 x) - (∫⁻ x, ⨅ n, f n x) = (∫⁻ x, f 0 x - ⨅ n, f n x) := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ (∫⁻ (x : ℝ), f 0 x) - ∫⁻ (x : ℝ), ⨅ n, f n x = ∫⁻ (x : ℝ), f 0 x - ⨅ n, f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ ∫⁻ (x : ℝ), f 0 x - ⨅ n, f n x = (∫⁻ (x : ℝ), f 0 x) - ∫⁻ (x : ℝ), ⨅ n, f n x All goals completed! 🐙 _ = ∫⁻ x, ⨆ n, f 0 x - f n x := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ ∫⁻ (x : ℝ), f 0 x - ⨅ n, f n x = ∫⁻ (x : ℝ), ⨆ n, f 0 x - f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ (fun x => f 0 x - ⨅ n, f n x) = fun x => ⨆ n, f 0 x - f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rflx:ℝ⊢ f 0 x - ⨅ n, f n x = ⨆ n, f 0 x - f n x All goals completed! 🐙 _ = ⨆ n, (∫⁻ x, f 0 x - f n x) := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ ∫⁻ (x : ℝ), ⨆ n, f 0 x - f n x = ⨆ n, ∫⁻ (x : ℝ), f 0 x - f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ ∀ (n : ℕ), Measurable fun x => f 0 x - f n xf:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ Monotone fun n x => f 0 x - f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ ∀ (n : ℕ), Measurable fun x => f 0 x - f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfln:ℕ⊢ Measurable fun x => f 0 x - f n x All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ Monotone fun n x => f 0 x - f n x intro i f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfli:ℕj:ℕ⊢ i ≤ j → (fun n x => f 0 x - f n x) i ≤ (fun n x => f 0 x - f n x) j f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfli:ℕj:ℕh:i ≤ j⊢ (fun n x => f 0 x - f n x) i ≤ (fun n x => f 0 x - f n x) j f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfli:ℕj:ℕh:i ≤ jx:ℝ⊢ (fun n x => f 0 x - f n x) i x ≤ (fun n x => f 0 x - f n x) j x All goals completed! 🐙 _ = ⨆ n, (∫⁻ x, f 0 x) - (∫⁻ x, f n x) := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rfl⊢ ⨆ n, ∫⁻ (x : ℝ), f 0 x - f n x = ⨆ n, (∫⁻ (x : ℝ), f 0 x) - ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rflh_mono:∀ (n : ℕ) (x : ℝ), f n x ≤ f 0 x := fun n x => h_anti (Nat.zero_le n) x⊢ ⨆ n, ∫⁻ (x : ℝ), f 0 x - f n x = ⨆ n, (∫⁻ (x : ℝ), f 0 x) - ∫⁻ (x : ℝ), f n x f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)h_anti:Antitone fh_fin:∫⁻ (x : ℝ), f 0 x ≠ ∞fn_le_f0:∫⁻ (x : ℝ), ⨅ n, f n x ≤ ∫⁻ (x : ℝ), f 0 x := lintegral_mono fun x => iInf_le_of_le 0 le_rflfn_le_f0':⨅ n, ∫⁻ (x : ℝ), f n x ≤ ∫⁻ (x : ℝ), f 0 x := iInf_le_of_le 0 le_rflh_mono:∀ (n : ℕ) (x : ℝ), f n x ≤ f 0 x := fun n x => h_anti (Nat.zero_le n) xn:ℕ⊢ ∫⁻ (x : ℝ), f 0 x - f n x = (∫⁻ (x : ℝ), f 0 x) - ∫⁻ (x : ℝ), f n x All goals completed! 🐙 _ = (∫⁻ x, f 0 x) - (⨅ n, ∫⁻ x, f n x) := ENNReal.sub_iInf.symm
定理 (ファトゥの補題).

f_0, f_1, \dots : \mathbb{R} \to [0,\infty] を可測関数の列とする。 このとき \underline{\int}_{x \in \mathbb{R}} \liminf_{n \to \infty} f_n(x)\,dx \le \liminf_{n \to \infty} \underline{\int}_{x \in \mathbb{R}} f_n(x)\,dx. が成り立つ。

Lean code
theorem lintegral_liminf_le {f : ℕ → ℝ → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n)) : ∫⁻ x, liminf (fun n ↦ f n x) atTop ≤ liminf (fun n ↦ ∫⁻ x, f n x) atTop := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)⊢ ∫⁻ (x : ℝ), liminf (fun n => f n x) atTop ≤ liminf (fun n => ∫⁻ (x : ℝ), f n x) atTop calc ∫⁻ x, liminf (fun n ↦ f n x) atTop = ∫⁻ x, ⨆ n : ℕ, ⨅ i ≥ n, f i x := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)⊢ ∫⁻ (x : ℝ), liminf (fun n => f n x) atTop = ∫⁻ (x : ℝ), ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i x All goals completed! 🐙 _ = ⨆ n : ℕ, ∫⁻ x, ⨅ i ≥ n, f i x := f:ℕ → ℝ → ℝ≥0∞h_meas:∀ (n : ℕ), Measurable (f n)⊢ ∫⁻ (x : ℝ), ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), f i x = ⨆ n, ∫⁻ (x : ℝ), ⨅ i, ⨅ (_ : i ≥ n), f i x All goals completed! 🐙 _ ≤ ⨆ n : ℕ, (⨅ i ≥ n, ∫⁻ x, f i x) := iSup_mono fun _ ↦ le_iInf₂_lintegral _ _ = liminf (fun n ↦ ∫⁻ x, f n x) atTop := Filter.liminf_eq_iSup_iInf_of_nat.symm
定理 (ファトゥの補題（limsup 版）).

f_0, f_1, \dots : \mathbb{R} \to [0,\infty] を可測関数とし、 g : \mathbb{R} \to [0,\infty] が全ての n に対して f_n \le g を満たすとする。 さらに \underline{\int}_{x \in \mathbb{R}} g(x)\,dx < \infty と仮定する。 このとき \limsup_{n \to \infty} \underline{\int}_{x \in \mathbb{R}} f_n(x)\,dx \le \underline{\int}_{x \in \mathbb{R}} \limsup_{n \to \infty} f_n(x)\,dx. が成り立つ。

Lean code
theorem limsup_lintegral_le {f : ℕ → ℝ → ℝ≥0∞} (g : ℝ → ℝ≥0∞) (hf_meas : ∀ n, Measurable (f n)) (h_bound : ∀ n, f n ≤ g) (h_fin : ∫⁻ x, g x ≠ ∞) : limsup (fun n ↦ ∫⁻ x, f n x) atTop ≤ ∫⁻ x, limsup (fun n ↦ f n x) atTop := f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ limsup (fun n => ∫⁻ (x : ℝ), f n x) atTop ≤ ∫⁻ (x : ℝ), limsup (fun n => f n x) atTop calc limsup (fun n ↦ ∫⁻ x, f n x) atTop = ⨅ n : ℕ, ⨆ i ≥ n, ∫⁻ x, f i x := limsup_eq_iInf_iSup_of_nat _ ≤ ⨅ n : ℕ, ∫⁻ x, ⨆ i ≥ n, f i x := f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), ∫⁻ (x : ℝ), f i x ≤ ⨅ n, ∫⁻ (x : ℝ), ⨆ i, ⨆ (_ : i ≥ n), f i x f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞n:ℕ⊢ ⨆ i, ⨆ (_ : i ≥ n), ∫⁻ (x : ℝ), f i x ≤ ∫⁻ (x : ℝ), ⨆ i, ⨆ (_ : i ≥ n), f i x All goals completed! 🐙 _ = ∫⁻ x, ⨅ n : ℕ, ⨆ i ≥ n, f i x := f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ⨅ n, ∫⁻ (x : ℝ), ⨆ i, ⨆ (_ : i ≥ n), f i x = ∫⁻ (x : ℝ), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i x f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ∫⁻ (x : ℝ), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i x = ⨅ n, ∫⁻ (x : ℝ), ⨆ i, ⨆ (_ : i ≥ n), f i x f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ∀ (n : ℕ), Measurable fun x => ⨆ i, ⨆ (_ : i ≥ n), f i xf:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ Antitone fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i xf:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ∫⁻ (x : ℝ), ⨆ i, ⨆ (_ : i ≥ 0), f i x ≠ ∞ f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ∀ (n : ℕ), Measurable fun x => ⨆ i, ⨆ (_ : i ≥ n), f i x f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞n:ℕ⊢ Measurable fun x => ⨆ i, ⨆ (_ : i ≥ n), f i x All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ Antitone fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x intro n f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞n:ℕm:ℕ⊢ n ≤ m → (fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x) m ≤ (fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x) n f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞n:ℕm:ℕhnm:n ≤ m⊢ (fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x) m ≤ (fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x) n f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞n:ℕm:ℕhnm:n ≤ mx:ℝ⊢ (fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x) m x ≤ (fun n x => ⨆ i, ⨆ (_ : i ≥ n), f i x) n x All goals completed! 🐙 f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ∫⁻ (x : ℝ), ⨆ i, ⨆ (_ : i ≥ 0), f i x ≠ ∞ f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ (fun x => ⨆ i, ⨆ (_ : i ≥ 0), f i x) ≤ g f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞x:ℝ⊢ (fun x => ⨆ i, ⨆ (_ : i ≥ 0), f i x) x ≤ g x All goals completed! 🐙 _ = ∫⁻ x, limsup (fun n ↦ f n x) atTop := f:ℕ → ℝ → ℝ≥0∞g:ℝ → ℝ≥0∞hf_meas:∀ (n : ℕ), Measurable (f n)h_bound:∀ (n : ℕ), f n ≤ gh_fin:∫⁻ (x : ℝ), g x ≠ ∞⊢ ∫⁻ (x : ℝ), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i x = ∫⁻ (x : ℝ), limsup (fun n => f n x) atTop All goals completed! 🐙
定理 (優収束定理).

f_0, f_1, \dots : \mathbb{R} \to [0,\infty] を可測関数の列とし、 F : \mathbb{R} \to [0,\infty] を関数、g : \mathbb{R} \to [0,\infty] を関数とする。 次を仮定する。

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

  2. \underline{\int}_{x \in \mathbb{R}} g(x)\,dx < \infty である。

  3. 任意の x \in \mathbb{R} に対して、列 f_0(x), f_1(x), \dots は F(x) に収束する。

このとき \lim_{n \to \infty} \underline{\int}_{x \in \mathbb{R}} f_n(x)\,dx = \underline{\int}_{x \in \mathbb{R}} F(x)\,dx. が成り立つ。

Lean code
theorem tendsto_lintegral_of_dominated_convergence {F : ℕ → ℝ → ℝ≥0∞} {f : ℝ → ℝ≥0∞} (bound : ℝ → ℝ≥0∞) (hF_meas : ∀ n, Measurable (F n)) (h_bound : ∀ n, F n ≤ bound) (h_fin : ∫⁻ x, bound x ≠ ∞) (h_lim : ∀ x, Tendsto (fun n ↦ F n x) atTop (𝓝 (f x))) : Tendsto (fun n ↦ ∫⁻ x, F n x) atTop (𝓝 (∫⁻ x, f x)) := tendsto_of_le_liminf_of_limsup_le (calc ∫⁻ x, f x = ∫⁻ x, liminf (fun n : ℕ ↦ F n x) atTop := F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ ∫⁻ (x : ℝ), f x = ∫⁻ (x : ℝ), liminf (fun n => F n x) atTop F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ ∀ (x : ℝ), f x = liminf (fun n => F n x) atTop F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))x:ℝ⊢ f x = liminf (fun n => F n x) atTop All goals completed! 🐙 _ ≤ liminf (fun n ↦ ∫⁻ x, F n x) atTop := lintegral_liminf_le hF_meas) (calc limsup (fun n : ℕ ↦ ∫⁻ x, F n x) atTop ≤ ∫⁻ x, limsup (fun n ↦ F n x) atTop := F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ limsup (fun n => ∫⁻ (x : ℝ), F n x) atTop ≤ ∫⁻ (x : ℝ), limsup (fun n => F n x) atTop All goals completed! 🐙 _ = ∫⁻ x, f x := F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ ∫⁻ (x : ℝ), limsup (fun n => F n x) atTop = ∫⁻ (x : ℝ), f x F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))⊢ ∀ (x : ℝ), limsup (fun n => F n x) atTop = f x F:ℕ → ℝ → ℝ≥0∞f:ℝ → ℝ≥0∞bound:ℝ → ℝ≥0∞hF_meas:∀ (n : ℕ), Measurable (F n)h_bound:∀ (n : ℕ), F n ≤ boundh_fin:∫⁻ (x : ℝ), bound x ≠ ∞h_lim:∀ (x : ℝ), Tendsto (fun n => F n x) atTop (𝓝 (f x))x:ℝ⊢ limsup (fun n => F n x) atTop = f x All goals completed! 🐙)