7.7. カーネル積分🔗

定義.

可測空間 X に対して、\Measure(X) に \left\{ \mu \in \Measure(X) \mid \mu(A) \in B \right\} で生成される σ-代数を入れることで、\Measure(X) を可測空間とみなす。ただし A \subseteq X は可測、B \subseteq [0,\infty] は可測とする。特に、任意の可測集合 A \subseteq X に対して評価写像 \mu \mapsto \mu(A) は可測である。

Lean code

inductive Measure.MeasurableGen (X : Type*) [MeasurableSpace X] : Set (Set (Measure X))
  | proj (A : Set X) (hs : MeasurableSet A) (B : Set ℝ≥0∞) (hB : MeasurableSet B) :
      Measure.MeasurableGen X ({μ | μ A ∈ B})

instance Measure.instMeasurableSpace : MeasurableSpace (Measure X) :=
  MeasurableSpace.generateFrom (Measure.MeasurableGen X)

theorem Measure.measurable_coe {A : Set X} (hA : MeasurableSet A) :
    Measurable fun μ : Measure X ↦ μ A :=
  fun {B} hB ↦ MeasurableSpace.measurableSet_generateFrom (MeasurableGen.proj A hA B hB)

補題.

写像 \mu : X \to \Measure(Y) が可測であることを示すには、任意の可測集合 A \subseteq Y に対してスカラー値写像 x \mapsto \mu(x)(A) が可測であることを示せば十分である。

Lean code

theorem measurable_of_measurable_coe (μ : X → Measure Y)
    (h : ∀ (s : Set Y), MeasurableSet s → Measurable fun x ↦ μ x s) : Measurable μ := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) s⊢ Measurable μ
  intro s hsX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss:Set (Measure Y)hs:MeasurableSet s⊢ MeasurableSet (μ ⁻¹' s)
  induction hs with
  | basic s hs =>basicX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss✝:Set (Measure Y)s:Set (Measure Y)hs:s ∈ Measure.MeasurableGen Y⊢ MeasurableSet (μ ⁻¹' s)
    obtain ⟨s, hs, t, ht⟩ := hsbasicX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss✝:Set (Measure Y)s:Set Yhs:MeasurableSet st:Set ℝ≥0∞ht:MeasurableSet t⊢ MeasurableSet (μ ⁻¹' {μ | μ s ∈ t})
    simp only [preimage_setOf_eq, measurableSet_setOf]basicX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss✝:Set (Measure Y)s:Set Yhs:MeasurableSet st:Set ℝ≥0∞ht:MeasurableSet t⊢ Measurable fun a => (μ a) s ∈ t
    exact measurableSet_setOf.mp (h s hs ht)All goals completed! 🐙
  | empty =>emptyX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss:Set (Measure Y)⊢ MeasurableSet (μ ⁻¹' ∅) simpAll goals completed! 🐙
  | compl s hs ih =>complX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss✝:Set (Measure Y)s:Set (Measure Y)hs:MeasurableSpace.GenerateMeasurable (Measure.MeasurableGen Y) sih:MeasurableSet (μ ⁻¹' s)⊢ MeasurableSet (μ ⁻¹' sᶜ)
    rw [@preimage_compl]complX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss✝:Set (Measure Y)s:Set (Measure Y)hs:MeasurableSpace.GenerateMeasurable (Measure.MeasurableGen Y) sih:MeasurableSet (μ ⁻¹' s)⊢ MeasurableSet (μ ⁻¹' s)ᶜ
    apply ih.complAll goals completed! 🐙
  | iUnion A hAd ihA =>iUnionX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss:Set (Measure Y)A:ℕ → Set (Measure Y)hAd:∀ (n : ℕ), MeasurableSpace.GenerateMeasurable (Measure.MeasurableGen Y) (A n)ihA:∀ (n : ℕ), MeasurableSet (μ ⁻¹' A n)⊢ MeasurableSet (μ ⁻¹' ⋃ i, A i)
    rw [@preimage_iUnion]iUnionX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yμ:X → Measure Yh:∀ (s : Set Y), MeasurableSet s → Measurable fun x => (μ x) ss:Set (Measure Y)A:ℕ → Set (Measure Y)hAd:∀ (n : ℕ), MeasurableSpace.GenerateMeasurable (Measure.MeasurableGen Y) (A n)ihA:∀ (n : ℕ), MeasurableSet (μ ⁻¹' A n)⊢ MeasurableSet (⋃ i, μ ⁻¹' A i)
    apply MeasurableSet.iUnion ihAAll goals completed! 🐙

補題.

f : X \to [0,\infty] が可測ならば、写像 \mu \mapsto \underline{\int}_{x \in X} f(x)\,d\mu は \Measure(X) から [0,\infty] への可測写像である。

Lean code

@[fun_prop]
theorem Measure.measurable_lintegral {f : X → ℝ≥0∞} (hf : Measurable f) :
    Measurable fun μ : Measure X ↦ ∫⁻ x, f x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable f⊢ Measurable fun μ => ∫⁻ (x : X), f x ∂μ
  simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable f⊢ Measurable fun μ => ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x})
  refine .iSup fun n ↦ Finset.measurable_fun_sum _ fun i _ ↦ ?_X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fn:ℕi:ℝ≥0∞x✝:i ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun μ => i * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})
  refine Measurable.const_mul ?_ _X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fn:ℕi:ℝ≥0∞x✝:i ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun μ => μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})
  exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)All goals completed! 🐙

定義.

X と Y を可測空間とし、 \nu : X \to \Measure(Y) を可測写像とする。 X 上の測度 \mu に対して、Y 上の測度 \mathcal{K}_{\nu}(\mu) を、可測集合 A \subseteq Y に対して \mathcal{K}_{\nu}(\mu)(A) \coloneqq \underline{\int}_{x \in X} \nu_x(A)\,d\mu で定める。

Lean code

open Classical in
def Measure.bind (f : X → Measure Y) (μ : Measure X) : Measure Y :=
  if hf : Measurable f then
    Measure.ofMeasurable (fun A _ ↦ ∫⁻ x, f x A ∂μ) (byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zf:X → Measure Yμ:Measure Xhf:Measurable f⊢ (fun A x => ∫⁻ (x : X), (f x) A ∂μ) ∅ ⋯ = 0 simpAll goals completed! 🐙) <| fun A hA hAd ↦
      calc
      ∫⁻ (x : X), (f x) (⋃ i, A i) ∂μ
      _ = ∫⁻ (x : X), ∑' (i : ℕ), (f x) (A i) ∂μ :=
        lintegral_congr (fun x ↦ measure_iUnion hAd hA)
      _ = ∑' (i : ℕ), ∫⁻ (x : X), (f x) (A i) ∂μ :=
        lintegral_tsum (fun n ↦ ((measurable_coe (hA n)).comp hf).aemeasurable)
  else 0

@[simp]
theorem Measure.bind_apply (f : X → Measure Y) (hf : Measurable f) (μ : Measure X) (A : Set Y)
    (hA : MeasurableSet A) :
    bind f μ A = ∫⁻ x, f x A ∂μ := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fμ:Measure XA:Set YhA:MeasurableSet A⊢ (bind f μ) A = ∫⁻ (x : X), (f x) A ∂μ
  rw [bind, dif_pos hf]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Measure Yhf:Measurable fμ:Measure XA:Set YhA:MeasurableSet A⊢ (Measure.ofMeasurable (fun A x => ∫⁻ (x : X), (f x) A ∂μ) ⋯ ⋯) A = ∫⁻ (x : X), (f x) A ∂μ
  apply Measure.ofMeasurable_apply _ hAAll goals completed! 🐙

補題.

f : Y \to [0,\infty] を可測とする。このとき \underline{\int}_{y \in Y} f(y)\,d(\mathcal{K}_{\nu}(\mu)) = \underline{\int}_{x \in X} \underline{\int}_{y \in Y} f(y)\,d\nu_x\,d\mu. が成り立つ。

Lean code

theorem lintegral_bind {m : Measure X} {μ : X → Measure Y} {f : Y → ℝ≥0∞} (hμ : Measurable μ)
    (hf : Measurable f) : ∫⁻ y, f y ∂Measure.bind μ m = ∫⁻ x, ∫⁻ y, f y ∂μ x ∂m := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∫⁻ (y : Y), f y ∂Measure.bind μ m = ∫⁻ (x : X), ∫⁻ (y : Y), f y ∂μ x ∂m
  rw [lintegral_eq_iSup_eapprox_lintegral hf]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, (SimpleFunc.eapprox f n).lintegral (Measure.bind μ m) = ∫⁻ (x : X), ∫⁻ (y : Y), f y ∂μ x ∂m
  dsimp only [SimpleFunc.lintegral]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) =
  ∫⁻ (x : X), ∫⁻ (y : Y), f y ∂μ x ∂m
  calc
    ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range,
        a * (Measure.bind μ m) ((SimpleFunc.eapprox f n) ⁻¹' {a})
    _ = ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range,
        a * (∫⁻ x, μ x ((SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      congr 1e_sX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ (fun n => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = fun n =>
  ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      ext ne_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      congr 1e_s.h.e_fX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ (fun a => a * (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = fun a =>
  a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      ext ae_s.h.e_f.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞⊢ a * (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      congr 1e_s.h.e_f.h.e_aX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞⊢ (Measure.bind μ m) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) = ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      rw [Measure.bind_apply μ hμ m]e_s.h.e_f.h.e_a.hAX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞⊢ MeasurableSet (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      exact SimpleFunc.measurableSet_fiber (SimpleFunc.eapprox f n) aAll goals completed! 🐙
    _ = ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range,
        (∫⁻ x, a * μ x ((SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      congr 1e_sX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ (fun n => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) = fun n =>
  ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      ext ne_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      congr 1e_s.h.e_fX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ (fun a => a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) = fun a =>
  ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      ext ae_s.h.e_f.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞⊢ a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      apply (lintegral_const_mul _ _).symmX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞⊢ Measurable fun a_1 => (μ a_1) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      have : (fun x ↦ (μ x) ((SimpleFunc.eapprox f n) ⁻¹' {a})) =
          ((fun ν : Measure Y ↦ ν ((SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * ∫⁻ (x : X), (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
        rflAll goals completed! 🐙
      rw [this]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞this:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ Measurable ((fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ)
      apply Measurable.comp _ hμX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞this:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ Measurable fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      refine Measure.measurable_coe ?_X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞this:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ MeasurableSet (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      exact SimpleFunc.measurableSet_fiber (SimpleFunc.eapprox f n) aAll goals completed! 🐙
    _ = ⨆ n, (∫⁻ x, ∑ a ∈ (SimpleFunc.eapprox f n).range,
        a * μ x ((SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ⨆ n, ∫⁻ (x : X), ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      congr 1e_sX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ (fun n => ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) = fun n =>
  ∫⁻ (x : X), ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      ext ne_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ∫⁻ (x : X), ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      refine Eq.symm (lintegral_finset_sum' (SimpleFunc.eapprox f n).range ?_)e_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ ∀ b ∈ (SimpleFunc.eapprox f n).range, AEMeasurable (fun x => b * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {b})) m
      intro a hae_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ AEMeasurable (fun x => a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) m
      apply Measurable.aemeasurablee_s.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      refine Measurable.mul ?_ ?_e_s.h.h.refine_1X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => ae_s.h.h.refine_2X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      ·e_s.h.h.refine_1X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => a exact measurable_constAll goals completed! 🐙
      ·e_s.h.h.refine_2X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) have : (fun x ↦ (μ x) ((SimpleFunc.eapprox f n) ⁻¹' {a})) =
            ((fun ν : Measure Y ↦ ν ((SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, ∫⁻ (x : X), a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ⨆ n, ∫⁻ (x : X), ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
          rflAll goals completed! 🐙
        rw [this]e_s.h.h.refine_2X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).rangethis:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ Measurable ((fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ)
        apply Measurable.comp _ hμX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).rangethis:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ Measurable fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        refine Measure.measurable_coe ?_X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).rangethis:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ MeasurableSet (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        exact SimpleFunc.measurableSet_fiber (SimpleFunc.eapprox f n) aAll goals completed! 🐙
    _ = (∫⁻ x, ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range,
        a * μ x ((SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∫⁻ (x : X), ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ∫⁻ (x : X), ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
      refine Eq.symm (lintegral_iSup' ?_ ?_)refine_1X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∀ (n : ℕ), AEMeasurable (fun x => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) mrefine_2X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∀ᵐ (x : X) ∂m, Monotone fun n => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
      ·refine_1X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∀ (n : ℕ), AEMeasurable (fun x => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) m intro nrefine_1X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ AEMeasurable (fun x => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) m
        apply Measurable.aemeasurablerefine_1.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ Measurable fun x => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        refine Finset.measurable_fun_sum (SimpleFunc.eapprox f n).range ?_refine_1.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕ⊢ ∀ i ∈ (SimpleFunc.eapprox f n).range, Measurable fun x => i * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {i})
        intro a harefine_1.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        refine Measurable.const_mul ?_ arefine_1.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).range⊢ Measurable fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        have : (fun x ↦ (μ x) ((SimpleFunc.eapprox f n) ⁻¹' {a})) =
            ((fun ν : Measure Y ↦ ν ((SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ⨆ n, ∫⁻ (x : X), ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ∫⁻ (x : X), ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m
          rflAll goals completed! 🐙
        rw [this]refine_1.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).rangethis:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ Measurable ((fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ)
        apply Measurable.comp _ hμX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).rangethis:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ Measurable fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        refine Measure.measurable_coe ?_X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fn:ℕa:ℝ≥0∞ha:a ∈ (SimpleFunc.eapprox f n).rangethis:(fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = (fun ν => ν (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) ∘ μ := Eq.refl fun x => (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})⊢ MeasurableSet (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})
        exact SimpleFunc.measurableSet_fiber (SimpleFunc.eapprox f n) aAll goals completed! 🐙
      ·refine_2X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∀ᵐ (x : X) ∂m, Monotone fun n => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) filter_upwards with a irefine_2.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕ⊢ ∀ ⦃b : ℕ⦄,
  i ≤ b →
    (fun n => ∑ a_2 ∈ (SimpleFunc.eapprox f n).range, a_2 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_2})) i ≤
      (fun n => ∑ a_2 ∈ (SimpleFunc.eapprox f n).range, a_2 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_2})) b jrefine_2.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕj:ℕ⊢ i ≤ j →
  (fun n => ∑ a_2 ∈ (SimpleFunc.eapprox f n).range, a_2 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_2})) i ≤
    (fun n => ∑ a_2 ∈ (SimpleFunc.eapprox f n).range, a_2 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_2})) j hijrefine_2.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕj:ℕhij:i ≤ j⊢ (fun n => ∑ a_1 ∈ (SimpleFunc.eapprox f n).range, a_1 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_1})) i ≤
  (fun n => ∑ a_1 ∈ (SimpleFunc.eapprox f n).range, a_1 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_1})) j
        simp onlyrefine_2.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕj:ℕhij:i ≤ j⊢ ∑ a_1 ∈ (SimpleFunc.eapprox f i).range, a_1 * (μ a) (⇑(SimpleFunc.eapprox f i) ⁻¹' {a_1}) ≤
  ∑ a_1 ∈ (SimpleFunc.eapprox f j).range, a_1 * (μ a) (⇑(SimpleFunc.eapprox f j) ⁻¹' {a_1})
        rw [← SimpleFunc.lintegral]refine_2.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕj:ℕhij:i ≤ j⊢ (SimpleFunc.eapprox f i).lintegral (μ a) ≤
  ∑ a_1 ∈ (SimpleFunc.eapprox f j).range, a_1 * (μ a) (⇑(SimpleFunc.eapprox f j) ⁻¹' {a_1})
        rw [← SimpleFunc.lintegral]refine_2.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕj:ℕhij:i ≤ j⊢ (SimpleFunc.eapprox f i).lintegral (μ a) ≤ (SimpleFunc.eapprox f j).lintegral (μ a)
        apply SimpleFunc.lintegral_mono _ (le_of_eq rfl)X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fa:Xi:ℕj:ℕhij:i ≤ j⊢ SimpleFunc.eapprox f i ≤ SimpleFunc.eapprox f j
        apply SimpleFunc.monotone_eapprox f hijAll goals completed! 🐙
    _ = ∫⁻ (a : X), ∫⁻ (x : Y), f x ∂μ a ∂m := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∫⁻ (x : X), ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) ∂m =
  ∫⁻ (a : X), ∫⁻ (x : Y), f x ∂μ a ∂m
      apply lintegral_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable f⊢ ∀ (a : X),
  ⨆ n, ∑ a_1 ∈ (SimpleFunc.eapprox f n).range, a_1 * (μ a) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a_1}) = ∫⁻ (x : Y), f x ∂μ a
      intro xhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) = ∫⁻ (x : Y), f x ∂μ x
      simp only [← SimpleFunc.iSup_eapprox_apply hf]hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  ∫⁻ (x : Y), ⨆ n, (SimpleFunc.eapprox f n) x ∂μ x
      rw [lintegral_iSup]hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  ⨆ n, ∫⁻ (a : Y), (SimpleFunc.eapprox f n) a ∂μ xh.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ ∀ (n : ℕ), Measurable ⇑(SimpleFunc.eapprox f n)h.h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ Monotone fun n => ⇑(SimpleFunc.eapprox f n)
      ·hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  ⨆ n, ∫⁻ (a : Y), (SimpleFunc.eapprox f n) a ∂μ x congr 1h.e_sX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ (fun n => ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a})) = fun n =>
  ∫⁻ (a : Y), (SimpleFunc.eapprox f n) a ∂μ x
        ext nh.e_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:Xn:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  ∫⁻ (a : Y), (SimpleFunc.eapprox f n) a ∂μ x
        rw [SimpleFunc.lintegral_eq_lintegral]h.e_s.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:Xn:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox f n).range, a * (μ x) (⇑(SimpleFunc.eapprox f n) ⁻¹' {a}) =
  (SimpleFunc.eapprox f n).lintegral (μ x)
        rw [SimpleFunc.lintegral]All goals completed! 🐙
      ·h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ ∀ (n : ℕ), Measurable ⇑(SimpleFunc.eapprox f n) intro nh.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:Xn:ℕ⊢ Measurable ⇑(SimpleFunc.eapprox f n)
        exact SimpleFunc.measurable (SimpleFunc.eapprox f n)All goals completed! 🐙
      ·h.h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:X⊢ Monotone fun n => ⇑(SimpleFunc.eapprox f n) intro i jh.h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:Xi:ℕj:ℕ⊢ i ≤ j → (fun n => ⇑(SimpleFunc.eapprox f n)) i ≤ (fun n => ⇑(SimpleFunc.eapprox f n)) j hijh.h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:Xi:ℕj:ℕhij:i ≤ j⊢ (fun n => ⇑(SimpleFunc.eapprox f n)) i ≤ (fun n => ⇑(SimpleFunc.eapprox f n)) j
        dsimp onlyh.h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Ym:Measure Xμ:X → Measure Yf:Y → ℝ≥0∞hμ:Measurable μhf:Measurable fx:Xi:ℕj:ℕhij:i ≤ j⊢ ⇑(SimpleFunc.eapprox f i) ≤ ⇑(SimpleFunc.eapprox f j)
        gcongrAll goals completed! 🐙