7.2. 押し出し測度🔗

押し出しは、可測写像に沿って測度を運ぶ操作です。

定義.

X と Y を可測空間とし、\mu を X 上の測度、f : X \to Y を可測写像とする。 f に沿った \mu の 押し出し とは、Y の任意の可測集合 A \subseteq Y に対して (f_*\mu)(A) \coloneqq \mu(f^{-1}(A)) で定まる Y 上の測度 f_*\mu のことである。

Lean code

/-- The pushforward of a measure along a measurable map. -/
def map (f : X → Y) (hf : Measurable f) (μ : Measure X) : Measure Y :=
  Measure.ofMeasurable (fun A _ ↦ μ (f ⁻¹' A)) (byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure X⊢ (fun A x => μ (f ⁻¹' A)) ∅ ⋯ = 0 simpAll goals completed! 🐙) <| byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure X⊢ ∀ ⦃f_1 : ℕ → Set Y⦄ (h : ∀ (i : ℕ), MeasurableSet (f_1 i)),
  Pairwise (Function.onFun Disjoint f_1) →
    (fun A x => μ (f ⁻¹' A)) (⋃ i, f_1 i) ⋯ = ∑' (i : ℕ), (fun A x => μ (f ⁻¹' A)) (f_1 i) ⋯
    intro A hAX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Pairwise (Function.onFun Disjoint A) →
  (fun A x => μ (f ⁻¹' A)) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => μ (f ⁻¹' A)) (A i) ⋯ hAdX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (fun A x => μ (f ⁻¹' A)) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => μ (f ⁻¹' A)) (A i) ⋯
    simp only [preimage_iUnion]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ μ (⋃ i, f ⁻¹' A i) = ∑' (i : ℕ), μ (f ⁻¹' A i)
    apply measure_iUnion _ (fun i ↦ hf (hA i))X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ Pairwise (Function.onFun Disjoint fun i => f ⁻¹' A i)
    intro i jX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)i:ℕj:ℕ⊢ i ≠ j → Function.onFun Disjoint (fun i => f ⁻¹' A i) i j hijX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)i:ℕj:ℕhij:i ≠ j⊢ Function.onFun Disjoint (fun i => f ⁻¹' A i) i j
    have := hAd hijX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:ℕ → Set YhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)i:ℕj:ℕhij:i ≠ jthis:Function.onFun Disjoint A i j := hAd hij⊢ Function.onFun Disjoint (fun i => f ⁻¹' A i) i j
    grindAll goals completed! 🐙

@[simp]
theorem map_apply (f : X → Y) (hf : Measurable f) (μ : Measure X) {A : Set Y}
    (hA : MeasurableSet A) :
    Measure.map f hf μ A = μ (f ⁻¹' A) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:Set YhA:MeasurableSet A⊢ (map f hf μ) A = μ (f ⁻¹' A)
  rw [Measure.map]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure XA:Set YhA:MeasurableSet A⊢ (Measure.ofMeasurable (fun A x => μ (f ⁻¹' A)) ⋯ ⋯) A = μ (f ⁻¹' A)
  exact Measure.ofMeasurable_apply _ hAAll goals completed! 🐙

補題.

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

Lean code

theorem lintegral_map (f : X → Y) (hf : Measurable f)
    (μ : Measure X) {g : Y → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ y, g y ∂(Measure.map f hf μ) = ∫⁻ x, g (f x) ∂μ := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable g⊢ ∫⁻ (y : Y), g y ∂Measure.map f hf μ = ∫⁻ (x : X), g (f x) ∂μ
  let h n : SimpleFunc X ℝ≥0∞ := {
    toFun := (SimpleFunc.eapprox g n) ∘ f
    measurableSet_fiber' := fun a ↦ byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gn:ℕa:ℝ≥0∞⊢ MeasurableSet (⇑(SimpleFunc.eapprox g n) ∘ f ⁻¹' {a})
      apply (SimpleFunc.measurable (SimpleFunc.eapprox g n)).comp hfaX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gn:ℕa:ℝ≥0∞⊢ MeasurableSet {a}
      exact measurableSet_singleton aAll goals completed! 🐙
    finite_range' := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gn:ℕ⊢ (range (⇑(SimpleFunc.eapprox g n) ∘ f)).Finite
      rw [@range_comp]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gn:ℕ⊢ (⇑(SimpleFunc.eapprox g n) '' range f).Finite
      have hsubset : (⇑(SimpleFunc.eapprox g n) '' range f) ⊆ range (SimpleFunc.eapprox g n) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gn:ℕ⊢ (range (⇑(SimpleFunc.eapprox g n) ∘ f)).Finite
        exact image_subset_range (⇑(SimpleFunc.eapprox g n)) (range f)All goals completed! 🐙
      clear hf hgX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yμ:Measure Xg:Y → ℝ≥0∞n:ℕhsubset:⇑(SimpleFunc.eapprox g n) '' range f ⊆ range ⇑(SimpleFunc.eapprox g n) := image_subset_range (⇑(SimpleFunc.eapprox g n)) (range f)⊢ (⇑(SimpleFunc.eapprox g n) '' range f).Finite
      exact Set.Finite.subset (SimpleFunc.finite_range (SimpleFunc.eapprox g n)) hsubsetAll goals completed! 🐙 }
  calc
    ∫⁻ y, g y ∂(Measure.map f hf μ) =
        ⨆ n, ∫⁻ y, (SimpleFunc.eapprox g n) y ∂(Measure.map f hf μ) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∫⁻ (y : Y), g y ∂Measure.map f hf μ = ⨆ n, ∫⁻ (y : Y), (SimpleFunc.eapprox g n) y ∂Measure.map f hf μ
      rw [lintegral_eq_iSup_eapprox_lintegral hg]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, (SimpleFunc.eapprox g n).lintegral (Measure.map f hf μ) =
  ⨆ n, ∫⁻ (y : Y), (SimpleFunc.eapprox g n) y ∂Measure.map f hf μ
      apply iSup_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (i : ℕ),
  (SimpleFunc.eapprox g i).lintegral (Measure.map f hf μ) = ∫⁻ (y : Y), (SimpleFunc.eapprox g i) y ∂Measure.map f hf μ
      intro nhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ (SimpleFunc.eapprox g n).lintegral (Measure.map f hf μ) = ∫⁻ (y : Y), (SimpleFunc.eapprox g n) y ∂Measure.map f hf μ
      rw [SimpleFunc.lintegral_eq_lintegral]All goals completed! 🐙
    _ = ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range,
        a * Measure.map f hf μ ((SimpleFunc.eapprox g n) ⁻¹' {a}) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∫⁻ (y : Y), (SimpleFunc.eapprox g n) y ∂Measure.map f hf μ =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g n) ⁻¹' {a})
      apply iSup_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (i : ℕ),
  ∫⁻ (y : Y), (SimpleFunc.eapprox g i) y ∂Measure.map f hf μ =
    ∑ a ∈ (SimpleFunc.eapprox g i).range, a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g i) ⁻¹' {a})
      intro nhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∫⁻ (y : Y), (SimpleFunc.eapprox g n) y ∂Measure.map f hf μ =
  ∑ a ∈ (SimpleFunc.eapprox g n).range, a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g n) ⁻¹' {a})
      rw [← SimpleFunc.map_lintegral, SimpleFunc.lintegral_eq_lintegral]hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ (SimpleFunc.eapprox g n).lintegral (Measure.map f hf μ) =
  (SimpleFunc.map (fun a => a) (SimpleFunc.eapprox g n)).lintegral (Measure.map f hf μ)
      rflAll goals completed! 🐙
    _ = ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range,
        a * μ (f ⁻¹' ((SimpleFunc.eapprox g n) ⁻¹' {a})) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}) =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (f ⁻¹' (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}))
      apply iSup_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (i : ℕ),
  ∑ a ∈ (SimpleFunc.eapprox g i).range, a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g i) ⁻¹' {a}) =
    ∑ a ∈ (SimpleFunc.eapprox g i).range, a * μ (f ⁻¹' (⇑(SimpleFunc.eapprox g i) ⁻¹' {a}))
      intro nhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox g n).range, a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}) =
  ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (f ⁻¹' (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}))
      congr 1 with ah.e_f.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ a * (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}) = a * μ (f ⁻¹' (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}))
      congr 1h.e_f.h.e_aX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ (Measure.map f hf μ) (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}) = μ (f ⁻¹' (⇑(SimpleFunc.eapprox g n) ⁻¹' {a}))
      rw [Measure.map_apply]h.e_f.h.e_a.hAX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ MeasurableSet (⇑(SimpleFunc.eapprox g n) ⁻¹' {a})
      exact SimpleFunc.measurableSet_fiber (SimpleFunc.eapprox g n) aAll goals completed! 🐙
    _ = ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range,
        a * μ ((SimpleFunc.eapprox g n ∘ f) ⁻¹' {a}) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (f ⁻¹' (⇑(SimpleFunc.eapprox g n) ⁻¹' {a})) =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(SimpleFunc.eapprox g n) ∘ f ⁻¹' {a})
      rflAll goals completed! 🐙
    _ = ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range,
        a * μ (h n ⁻¹' {a}) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(SimpleFunc.eapprox g n) ∘ f ⁻¹' {a}) =
  ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(h n) ⁻¹' {a})
      rflAll goals completed! 🐙
    _ = ⨆ n, ∑ a ∈ (h n).range, a * μ (h n ⁻¹' {a}) := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(h n) ⁻¹' {a}) = ⨆ n, ∑ a ∈ (h n).range, a * μ (⇑(h n) ⁻¹' {a})
      apply iSup_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (i : ℕ), ∑ a ∈ (SimpleFunc.eapprox g i).range, a * μ (⇑(h i) ⁻¹' {a}) = ∑ a ∈ (h i).range, a * μ (⇑(h i) ⁻¹' {a})
      intro nhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(h n) ⁻¹' {a}) = ∑ a ∈ (h n).range, a * μ (⇑(h n) ⁻¹' {a})
      apply Eq.symmh.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∑ a ∈ (h n).range, a * μ (⇑(h n) ⁻¹' {a}) = ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(h n) ⁻¹' {a})
      apply Finset.sum_subseth.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ (h n).range ⊆ (SimpleFunc.eapprox g n).rangeh.h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∀ x ∈ (SimpleFunc.eapprox g n).range, x ∉ (h n).range → x * μ (⇑(h n) ⁻¹' {x}) = 0
      ·h.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ (h n).range ⊆ (SimpleFunc.eapprox g n).range intro ah.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ a ∈ (h n).range → a ∈ (SimpleFunc.eapprox g n).range
        simp only [SimpleFunc.mem_range, mem_range, forall_exists_index]h.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ ∀ (x : X), (h n) x = a → ∃ y, (SimpleFunc.eapprox g n) y = a
        intro x hxh.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞x:Xhx:(h n) x = a⊢ ∃ y, (SimpleFunc.eapprox g n) y = a
        refine ⟨f x, ?_⟩h.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞x:Xhx:(h n) x = a⊢ (SimpleFunc.eapprox g n) (f x) = a
        rw [← hx]h.h.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞x:Xhx:(h n) x = a⊢ (SimpleFunc.eapprox g n) (f x) = (h n) x
        rflAll goals completed! 🐙
      ·h.h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∀ x ∈ (SimpleFunc.eapprox g n).range, x ∉ (h n).range → x * μ (⇑(h n) ⁻¹' {x}) = 0 intro ah.h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ a ∈ (SimpleFunc.eapprox g n).range → a ∉ (h n).range → a * μ (⇑(h n) ⁻¹' {a}) = 0
        simp only [SimpleFunc.mem_range, mem_range, not_exists, mul_eq_zero, forall_exists_index]h.h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞⊢ ∀ (x : Y), (SimpleFunc.eapprox g n) x = a → (∀ (x : X), ¬(h n) x = a) → a = 0 ∨ μ (⇑(h n) ⁻¹' {a}) = 0
        intro y hyh.h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞y:Yhy:(SimpleFunc.eapprox g n) y = a⊢ (∀ (x : X), ¬(h n) x = a) → a = 0 ∨ μ (⇑(h n) ⁻¹' {a}) = 0 hah.h.hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞y:Yhy:(SimpleFunc.eapprox g n) y = aha:∀ (x : X), ¬(h n) x = a⊢ a = 0 ∨ μ (⇑(h n) ⁻¹' {a}) = 0
        righth.h.hf.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞y:Yhy:(SimpleFunc.eapprox g n) y = aha:∀ (x : X), ¬(h n) x = a⊢ μ (⇑(h n) ⁻¹' {a}) = 0
        have hempty : (h n) ⁻¹' {a} = ∅ := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∑ a ∈ (SimpleFunc.eapprox g n).range, a * μ (⇑(h n) ⁻¹' {a}) = ⨆ n, ∑ a ∈ (h n).range, a * μ (⇑(h n) ⁻¹' {a})
          ext xhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞y:Yhy:(SimpleFunc.eapprox g n) y = aha:∀ (x : X), ¬(h n) x = ax:X⊢ x ∈ ⇑(h n) ⁻¹' {a} ↔ x ∈ ∅
          simp only [mem_preimage, mem_singleton_iff, mem_empty_iff_false, iff_false]hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞y:Yhy:(SimpleFunc.eapprox g n) y = aha:∀ (x : X), ¬(h n) x = ax:X⊢ ¬(h n) x = a
          exact ha xAll goals completed! 🐙
        rw [hempty]h.h.hf.hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕa:ℝ≥0∞y:Yhy:(SimpleFunc.eapprox g n) y = aha:∀ (x : X), ¬(h n) x = ahempty:⇑(h n) ⁻¹' {a} = ∅ := 
  ext fun x =>
    Eq.mpr
      (id
        (Eq.trans (congr (congrArg Iff (Eq.trans lintegral_map._simp_6 lintegral_map._simp_7)) (lintegral_map._simp_8 x))
          (iff_false ((h n) x = a))))
      (ha x)⊢ μ ∅ = 0
        simpAll goals completed! 🐙
    _ = ⨆ n, ∫⁻ x, (h n) x ∂μ := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∑ a ∈ (h n).range, a * μ (⇑(h n) ⁻¹' {a}) = ⨆ n, ∫⁻ (x : X), (h n) x ∂μ
      apply iSup_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (i : ℕ), ∑ a ∈ (h i).range, a * μ (⇑(h i) ⁻¹' {a}) = ∫⁻ (x : X), (h i) x ∂μ
      intro nhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ ∑ a ∈ (h n).range, a * μ (⇑(h n) ⁻¹' {a}) = ∫⁻ (x : X), (h n) x ∂μ
      rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.lintegral]All goals completed! 🐙
    _ = ∫⁻ x, (g ∘ f) x ∂μ := byX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ⨆ n, ∫⁻ (x : X), (h n) x ∂μ = ∫⁻ (x : X), (g ∘ f) x ∂μ
      rw [← lintegral_iSup]X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∫⁻ (a : X), ⨆ n, (h n) a ∂μ = ∫⁻ (x : X), (g ∘ f) x ∂μhfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (n : ℕ), Measurable ⇑(h n)h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ Monotone fun n => ⇑(h n)
      ·X:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∫⁻ (a : X), ⨆ n, (h n) a ∂μ = ∫⁻ (x : X), (g ∘ f) x ∂μ apply lintegral_congrhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (a : X), ⨆ n, (h n) a = (g ∘ f) a
        intro xhX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }x:X⊢ ⨆ n, (h n) x = (g ∘ f) x
        simp only [SimpleFunc.coe_mk, Function.comp_apply, h]hX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }x:X⊢ ⨆ n, (SimpleFunc.eapprox g n) (f x) = g (f x)
        rw [SimpleFunc.iSup_eapprox_apply hg (f x)]All goals completed! 🐙
      ·hfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ ∀ (n : ℕ), Measurable ⇑(h n) intro nhfX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }n:ℕ⊢ Measurable ⇑(h n)
        exact SimpleFunc.measurable (h n)All goals completed! 🐙
      ·h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }⊢ Monotone fun n => ⇑(h n) intro i jh_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }i:ℕj:ℕ⊢ i ≤ j → (fun n => ⇑(h n)) i ≤ (fun n => ⇑(h n)) j hijh_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }i:ℕj:ℕhij:i ≤ j⊢ (fun n => ⇑(h n)) i ≤ (fun n => ⇑(h n)) j xh_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }i:ℕj:ℕhij:i ≤ jx:X⊢ (fun n => ⇑(h n)) i x ≤ (fun n => ⇑(h n)) j x
        simp only [SimpleFunc.coe_mk, Function.comp_apply, h]h_monoX:Type u_1Y:Type u_2inst✝¹:MeasurableSpace Xinst✝:MeasurableSpace Yf:X → Yhf:Measurable fμ:Measure Xg:Y → ℝ≥0∞hg:Measurable gh:ℕ → SimpleFunc X ℝ≥0∞ := fun n => { toFun := ⇑(SimpleFunc.eapprox g n) ∘ f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }i:ℕj:ℕhij:i ≤ jx:X⊢ (SimpleFunc.eapprox g i) (f x) ≤ (SimpleFunc.eapprox g j) (f x)
        exact SimpleFunc.monotone_eapprox g hij (f x)All goals completed! 🐙