7.1. 制限測度🔗

定義.

X を可測空間とし、\mu を X 上の測度、A \subseteq X を可測集合とする。 \mu の A への制限を \mu|_A と書き、任意の可測集合 B \subseteq X に対して (\mu|_A)(B) \coloneqq \mu(A \cap B) で定義される測度として定める。

Lean code

/-- Restriction of a measure to a measurable set. -/
def restrict (μ : Measure X) (A : Set X) (hA : MeasurableSet A) : Measure X :=
  Measure.ofMeasurable (fun B _ ↦ μ (A ∩ B)) (byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ (fun B x => μ (A ∩ B)) ∅ ⋯ = 0 simpAll goals completed! 🐙) <| byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet A⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
  Pairwise (Function.onFun Disjoint f) →
    (fun B x => μ (A ∩ B)) (⋃ i, f i) ⋯ = ∑' (i : ℕ), (fun B x => μ (A ∩ B)) (f i) ⋯
    intro B hBX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)⊢ Pairwise (Function.onFun Disjoint B) → (fun B x => μ (A ∩ B)) (⋃ i, B i) ⋯ = ∑' (i : ℕ), (fun B x => μ (A ∩ B)) (B i) ⋯ hBdX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ (fun B x => μ (A ∩ B)) (⋃ i, B i) ⋯ = ∑' (i : ℕ), (fun B x => μ (A ∩ B)) (B i) ⋯
    dsimp onlyX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ μ (A ∩ ⋃ i, B i) = ∑' (i : ℕ), μ (A ∩ B i)
    rw [Set.inter_iUnion]X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ μ (⋃ i, A ∩ B i) = ∑' (i : ℕ), μ (A ∩ B i)
    refine measure_iUnion ?_ ?_refine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ Pairwise (Function.onFun Disjoint fun i => A ∩ B i)refine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ ∀ (i : ℕ), MeasurableSet (A ∩ B i)
    ·refine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ Pairwise (Function.onFun Disjoint fun i => A ∩ B i) intro i jrefine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)i:ℕj:ℕ⊢ i ≠ j → Function.onFun Disjoint (fun i => A ∩ B i) i j hijrefine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)i:ℕj:ℕhij:i ≠ j⊢ Function.onFun Disjoint (fun i => A ∩ B i) i j
      exact (hBd hij).mono Set.inter_subset_right Set.inter_subset_rightAll goals completed! 🐙
    ·refine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)⊢ ∀ (i : ℕ), MeasurableSet (A ∩ B i) intro irefine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:ℕ → Set XhB:∀ (i : ℕ), MeasurableSet (B i)hBd:Pairwise (Function.onFun Disjoint B)i:ℕ⊢ MeasurableSet (A ∩ B i)
      exact hA.inter (hB i)All goals completed! 🐙

@[simp]
theorem restrict_apply (μ : Measure X) {A B : Set X} (hA : MeasurableSet A)
    (hB : MeasurableSet B) :
    restrict μ A hA B = μ (A ∩ B) := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ (restrict μ A hA) B = μ (A ∩ B)
  rw [restrict]X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ (Measure.ofMeasurable (fun B x => μ (A ∩ B)) ⋯ ⋯) B = μ (A ∩ B)
  exact Measure.ofMeasurable_apply _ hBAll goals completed! 🐙

概念的には、\mu|_A は A の外側の情報を捨て、集合のうち A の内側に残る部分だけを測ります。

補題.

この定義は、付随する外測度と両立している: (\mu|_A)^{*} (B) = \mu^{*} (A \cap B) が任意の部分集合 B \subseteq X（可測でなくてもよい）に対して成り立つ。

ここで \mu^{*} は \mu に付随する外測度を表す。

Lean code

theorem restrict_toOuterMeasure_eq_toOuterMeasure_restrict (μ : Measure X) {A : Set X}
    (hA : MeasurableSet A) (B : Set X) :
    Measure.restrict μ A hA B = μ (A ∩ B) := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ (restrict μ A hA) B = μ (A ∩ B)
  apply le_antisymmaX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ (restrict μ A hA) B ≤ μ (A ∩ B)aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ (A ∩ B) ≤ (restrict μ A hA) B
  ·aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ (restrict μ A hA) B ≤ μ (A ∩ B) rcases μ.exists_measurable_superset_eq_trim (A ∩ B) with ⟨C, hCAB, hC, hμC⟩aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:A ∩ B ⊆ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ.trim (A ∩ B)⊢ (restrict μ A hA) B ≤ μ (A ∩ B)
    rw [← measure_eq_trim] at hμCaX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:A ∩ B ⊆ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ (restrict μ A hA) B ≤ μ (A ∩ B)
    rw [← hμC]aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:A ∩ B ⊆ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ (restrict μ A hA) B ≤ μ.toOuterMeasure C
    rw [inter_comm] at hCABaX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:B ∩ A ⊆ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ (restrict μ A hA) B ≤ μ.toOuterMeasure C
    rw [inter_subset] at hCABaX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:B ⊆ Aᶜ ∪ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ (restrict μ A hA) B ≤ μ.toOuterMeasure C
    apply (measure_mono hCAB).transaX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:B ⊆ Aᶜ ∪ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ (restrict μ A hA) (Aᶜ ∪ C) ≤ μ.toOuterMeasure C
    simp only [Measure.coe_toOuterMeasure]aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:B ⊆ Aᶜ ∪ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ (restrict μ A hA) (Aᶜ ∪ C) ≤ μ C
    rw [Measure.restrict_apply _ hA (hA.compl.union hC)]aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:B ⊆ Aᶜ ∪ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ μ (A ∩ (Aᶜ ∪ C)) ≤ μ C
    apply le_trans (le_of_eq _) (measure_mono (show A ∩ C ⊆ C from Set.inter_subset_right))X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhCAB:B ⊆ Aᶜ ∪ ChC:MeasurableSet ChμC:μ.toOuterMeasure C = μ (A ∩ B)⊢ μ (A ∩ (Aᶜ ∪ C)) = μ (A ∩ C)
    have : A ∩ (Aᶜ ∪ C) = A ∩ C := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ (restrict μ A hA) B = μ (A ∩ B) grindAll goals completed! 🐙
    grindAll goals completed! 🐙
  ·aX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ μ (A ∩ B) ≤ (restrict μ A hA) B conv_rhs => rw [measure_eq_iInf]X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X| ⨅ t, ⨅ (_ : B ⊆ t), ⨅ (_ : MeasurableSet t), (restrict μ A hA) t
    apply le_iInfa.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set X⊢ ∀ (i : Set X), μ (A ∩ B) ≤ ⨅ (_ : B ⊆ i), ⨅ (_ : MeasurableSet i), (restrict μ A hA) i
    intro Ca.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set X⊢ μ (A ∩ B) ≤ ⨅ (_ : B ⊆ C), ⨅ (_ : MeasurableSet C), (restrict μ A hA) C
    apply le_iInfa.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set X⊢ B ⊆ C → μ (A ∩ B) ≤ ⨅ (_ : MeasurableSet C), (restrict μ A hA) C
    intro hBCa.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ C⊢ μ (A ∩ B) ≤ ⨅ (_ : MeasurableSet C), (restrict μ A hA) C
    apply le_iInfa.h.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ C⊢ MeasurableSet C → μ (A ∩ B) ≤ (restrict μ A hA) C
    intro hCa.h.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ (A ∩ B) ≤ (restrict μ A hA) C
    rw [Measure.restrict_apply _ hA hC]a.h.h.hX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet AB:Set XC:Set XhBC:B ⊆ ChC:MeasurableSet C⊢ μ (A ∩ B) ≤ μ (A ∩ C)
    exact measure_mono (inter_subset_inter_right A hBC)All goals completed! 🐙

補題.

A が可測ならば、制限測度に関する積分は被積分関数に A の指示関数を掛けることと同じである: \underline{\int}_{x \in X} f(x)\,d(\mu|_A) = \underline{\int}_{x \in X} 1_A(x) \cdot f(x)\,d\mu.

Lean code

theorem lintegral_indicator_le (f : X → ℝ≥0∞) (A : Set X) (μ : Measure X)
    (hA : MeasurableSet A) :
    ∫⁻ x, A.indicator f x ∂μ ≤ ∫⁻ x, f x ∂(Measure.restrict μ A hA) := byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet A⊢ ∫⁻ (x : X), A.indicator f x ∂μ ≤ ∫⁻ (x : X), f x ∂Measure.restrict μ A hA
  simp only [lintegral]X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet A⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => A.indicator f x), g.lintegral μ ≤
  ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (Measure.restrict μ A hA)
  apply iSup_le fun g ↦ iSup_le fun hg ↦ ?_X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f x⊢ g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (Measure.restrict μ A hA)
  have hgf : g ≤ f := hg.trans (indicator_le_self A f)X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)⊢ g.lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (Measure.restrict μ A hA)
  refine le_iSup_of_le g <| le_iSup_of_le hgf <| le_of_eq ?_X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)⊢ g.lintegral μ = g.lintegral (Measure.restrict μ A hA)
  rw [SimpleFunc.lintegral_restrict_measure g μ hA, SimpleFunc.lintegral]X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)⊢ ∑ x ∈ g.range, x * μ (⇑g ⁻¹' {x}) = ∑ y ∈ g.range, y * μ (⇑g ⁻¹' {y} ∩ A)
  congr with te_f.hX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ A)
  by_cases ht : t = 0posX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞ht:t = 0⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ A)negX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞ht:¬t = 0⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ A)
  ·posX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞ht:t = 0⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ A) simp [ht]All goals completed! 🐙
  ·negX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞ht:¬t = 0⊢ t * μ (⇑g ⁻¹' {t}) = t * μ (⇑g ⁻¹' {t} ∩ A) congr with xneg.e_a.h.e_6.h.hX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞ht:¬t = 0x:X⊢ x ∈ ⇑g ⁻¹' {t} ↔ x ∈ ⇑g ⁻¹' {t} ∩ A
    simp only [mem_preimage, mem_singleton_iff, mem_inter_iff, iff_self_and]neg.e_a.h.e_6.h.hX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)t:ℝ≥0∞ht:¬t = 0x:X⊢ g x = t → x ∈ A
    rintro rflneg.e_a.h.e_6.h.hX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)x:Xht:¬g x = 0⊢ x ∈ A
    contrapose! htneg.e_a.h.e_6.h.hX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞A:Set Xμ:Measure XhA:MeasurableSet Ag:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => A.indicator f xhgf:⇑g ≤ f := LE.le.trans hg (indicator_le_self A f)x:Xht:x ∉ A⊢ g x = 0
    simpa [ht] using hg xAll goals completed! 🐙

theorem lintegral_restrict {μ : Measure X} {A : Set X} (hA : MeasurableSet A)
    (f : X → ℝ≥0∞) :
    ∫⁻ x, f x ∂(Measure.restrict μ A hA) = ∫⁻ x, A.indicator f x ∂μ := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞⊢ ∫⁻ (x : X), f x ∂Measure.restrict μ A hA = ∫⁻ (x : X), A.indicator f x ∂μ
  apply le_antisymm ?_ (lintegral_indicator_le f A μ hA)X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞⊢ ∫⁻ (x : X), f x ∂Measure.restrict μ A hA ≤ ∫⁻ (x : X), A.indicator f x ∂μ
  simp only [lintegral, iSup_subtype']X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞⊢ ⨆ x, (↑x).lintegral (Measure.restrict μ A hA) ≤ ⨆ x, (↑x).lintegral μ
  refine iSup_mono' (Subtype.forall.2 fun g hg ↦ ?_)X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞g:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f x⊢ ∃ i', (↑⟨g, hg⟩).lintegral (Measure.restrict μ A hA) ≤ (↑i').lintegral μ
  refine ⟨⟨g.restrict A, fun x ↦ ?_⟩, ?_⟩refine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞g:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f xx:X⊢ (g.restrict A) x ≤ (fun x => A.indicator f x) xrefine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞g:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f x⊢ (↑⟨g, hg⟩).lintegral (Measure.restrict μ A hA) ≤ (↑⟨g.restrict A, ⋯⟩).lintegral μ
  ·refine_1X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞g:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f xx:X⊢ (g.restrict A) x ≤ (fun x => A.indicator f x) x simp [hg x, hA, indicator_le_indicator]All goals completed! 🐙
  ·refine_2X:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:Set XhA:MeasurableSet Af:X → ℝ≥0∞g:X →ₛ ℝ≥0∞hg:⇑g ≤ fun x => f x⊢ (↑⟨g, hg⟩).lintegral (Measure.restrict μ A hA) ≤ (↑⟨g.restrict A, ⋯⟩).lintegral μ exact le_of_eq (MTI.SimpleFunc.restrict_lintegral_eq_lintegral_restrict_measure g hA μ).symmAll goals completed! 🐙