7.4. 測度の和
定義.
X を可測空間とし、\mu と \nu を X 上の測度とする。
それらの 和 とは、任意の可測集合 A \subseteq X に対して
(\mu + \nu)(A) \coloneqq \mu(A) + \nu(A)
で定まる X 上の測度である。
Lean code
/-- The sum of two measures, defined on measurable sets by pointwise addition. -/
def add (μ ν : Measure X) : Measure X :=
Measure.ofMeasurable (fun A _ ↦ μ A + ν A) (X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure X⊢ (fun A x => μ A + ν A) ∅ ⋯ = 0 All goals completed! 🐙) <| X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure X⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
Pairwise (Function.onFun Disjoint f) →
(fun A x => μ A + ν A) (⋃ i, f i) ⋯ = ∑' (i : ℕ), (fun A x => μ A + ν A) (f i) ⋯
intro A X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Pairwise (Function.onFun Disjoint A) → (fun A x => μ A + ν A) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => μ A + ν A) (A i) ⋯ X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (fun A x => μ A + ν A) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x => μ A + ν A) (A i) ⋯
simpa using (show μ (⋃ i, A i) + ν (⋃ i, A i) = ∑' i, (μ (A i) + ν (A i)) X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure X⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
Pairwise (Function.onFun Disjoint f) →
(fun A x => μ A + ν A) (⋃ i, f i) ⋯ = ∑' (i : ℕ), (fun A x => μ A + ν A) (f i) ⋯
All goals completed! 🐙)@[simp]
theorem add_apply (μ ν : Measure X) {A : Set X} (hA : MeasurableSet A) :
Measure.add μ ν A = μ A + ν A := X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure XA:Set XhA:MeasurableSet A⊢ (add μ ν) A = μ A + ν A
X:Type u_1inst✝:MeasurableSpace Xμ:Measure Xν:Measure XA:Set XhA:MeasurableSet A⊢ (Measure.ofMeasurable (fun A x => μ A + ν A) ⋯ ⋯) A = μ A + ν A
All goals completed! 🐙
補題.
下積分は測度の和に関して加法的である:
\underline{\int}_{x \in X} f(x)\,d(\mu + \nu)
=
\underline{\int}_{x \in X} f(x)\,d\mu
+
\underline{\int}_{x \in X} f(x)\,d\nu.
Lean code
theorem lintegral_add_measure (f : X → ℝ≥0∞) (μ ν : Measure X) :
∫⁻ x, f x ∂(Measure.add μ ν) = ∫⁻ x, f x ∂μ + ∫⁻ x, f x ∂ν := X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure X⊢ ∫⁻ (x : X), f x ∂Measure.add μ ν = ∫⁻ (x : X), f x ∂μ + ∫⁻ (x : X), f x ∂ν
simp_rw X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure X⊢ ∫⁻ (x : X), f x ∂Measure.add μ ν = ∫⁻ (x : X), f x ∂μ + ∫⁻ (x : X), f x ∂νlintegral_def]
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (Measure.add μ ν) =
(⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral μ) + ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral ν
simp_rw X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral (Measure.add μ ν) =
(⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral μ) + ⨆ g, ⨆ (_ : ⇑g ≤ fun x => f x), g.lintegral νiSup_subtype']
have hsum : ∀ g : X →ₛ ℝ≥0∞,
g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure X⊢ ∫⁻ (x : X), f x ∂Measure.add μ ν = ∫⁻ (x : X), f x ∂μ + ∫⁻ (x : X), f x ∂ν
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}g:X →ₛ ℝ≥0∞⊢ g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν)
All goals completed! 🐙
have hiSup :
⨆ g : S, SimpleFunc.lintegral g (Measure.add μ ν) =
⨆ g : S, SimpleFunc.lintegral g μ + SimpleFunc.lintegral g ν := X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure X⊢ ∫⁻ (x : X), f x ∂Measure.add μ ν = ∫⁻ (x : X), f x ∂μ + ∫⁻ (x : X), f x ∂ν
All goals completed! 🐙
calc
⨆ g : S, SimpleFunc.lintegral g (Measure.add μ ν)
= ⨆ g : S, SimpleFunc.lintegral g μ + SimpleFunc.lintegral g ν := hiSup
_ = (⨆ g : S, SimpleFunc.lintegral g μ) + ⨆ g : S, SimpleFunc.lintegral g ν := X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)⊢ ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν = (⨆ g, (↑g).lintegral μ) + ⨆ g, (↑g).lintegral ν
have hdir : IsDirectedOrder S := X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)⊢ ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν = (⨆ g, (↑g).lintegral μ) + ⨆ g, (↑g).lintegral ν
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)⊢ ∀ (a b : ↑S), ∃ c, a ≤ c ∧ b ≤ c
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ∃ c, ⟨g₁, hg₁⟩ ≤ c ∧ ⟨g₂, hg₂⟩ ≤ c
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ g₁ ⊔ g₂ ∈ SX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ⟨g₁, hg₁⟩ ≤ ⟨g₁ ⊔ g₂, ?directed.refine_1⟩ ∧ ⟨g₂, hg₂⟩ ≤ ⟨g₁ ⊔ g₂, ?directed.refine_1⟩
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ g₁ ⊔ g₂ ∈ S X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ Sx:X⊢ (g₁ ⊔ g₂) x ≤ (fun x => f x) x
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ Sx:X⊢ g₁ x ≤ f x ∧ g₂ x ≤ f x
All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ⟨g₁, hg₁⟩ ≤ ⟨g₁ ⊔ g₂, ?directed.refine_1⟩ ∧ ⟨g₂, hg₂⟩ ≤ ⟨g₁ ⊔ g₂, ?directed.refine_1⟩ X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ⟨g₁, hg₁⟩ ≤ ⟨g₁ ⊔ g₂, ⋯⟩X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ⟨g₂, hg₂⟩ ≤ ⟨g₁ ⊔ g₂, ⋯⟩ X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ⟨g₁, hg₁⟩ ≤ ⟨g₁ ⊔ g₂, ⋯⟩X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ S⊢ ⟨g₂, hg₂⟩ ≤ ⟨g₁ ⊔ g₂, ⋯⟩ X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ Sx:X⊢ ↑⟨g₂, hg₂⟩ x ≤ ↑⟨g₁ ⊔ g₂, ⋯⟩ x X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ Sx:X⊢ ↑⟨g₁, hg₁⟩ x ≤ ↑⟨g₁ ⊔ g₂, ⋯⟩ xX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)g₁:X →ₛ ℝ≥0∞hg₁:g₁ ∈ Sg₂:X →ₛ ℝ≥0∞hg₂:g₂ ∈ Sx:X⊢ ↑⟨g₂, hg₂⟩ x ≤ ↑⟨g₁ ⊔ g₂, ⋯⟩ x All goals completed! 🐙
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)hdir:IsDirectedOrder ↑S :=
{
directed := fun a =>
Subtype.casesOn (motive := fun x => ∀ (b : ↑S), ∃ c, x ≤ c ∧ b ≤ c) a fun g₁ hg₁ b =>
Subtype.casesOn b fun g₂ hg₂ =>
Exists.intro ⟨g₁ ⊔ g₂, fun x => Eq.mpr (id lintegral_add_measure._simp_1) ⟨hg₁ x, hg₂ x⟩⟩
⟨fun x => of_eq_true le_sup_left._simp_2, fun x => of_eq_true le_sup_right._simp_2⟩ }⊢ Monotone fun g => (↑g).lintegral μX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)hdir:IsDirectedOrder ↑S :=
{
directed := fun a =>
Subtype.casesOn (motive := fun x => ∀ (b : ↑S), ∃ c, x ≤ c ∧ b ≤ c) a fun g₁ hg₁ b =>
Subtype.casesOn b fun g₂ hg₂ =>
Exists.intro ⟨g₁ ⊔ g₂, fun x => Eq.mpr (id lintegral_add_measure._simp_1) ⟨hg₁ x, hg₂ x⟩⟩
⟨fun x => of_eq_true le_sup_left._simp_2, fun x => of_eq_true le_sup_right._simp_2⟩ }⊢ Monotone fun g => (↑g).lintegral ν
all_goals
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)hdir:IsDirectedOrder ↑S :=
{
directed := fun a =>
Subtype.casesOn (motive := fun x => ∀ (b : ↑S), ∃ c, x ≤ c ∧ b ≤ c) a fun g₁ hg₁ b =>
Subtype.casesOn b fun g₂ hg₂ =>
Exists.intro ⟨g₁ ⊔ g₂, fun x => Eq.mpr (id lintegral_add_measure._simp_1) ⟨hg₁ x, hg₂ x⟩⟩
⟨fun x => of_eq_true le_sup_left._simp_2, fun x => of_eq_true le_sup_right._simp_2⟩ }g:X →ₛ ℝ≥0∞hg:g ∈ Sg':X →ₛ ℝ≥0∞hg':g' ∈ Shgg':⟨g, hg⟩ ≤ ⟨g', hg'⟩⊢ (fun g => (↑g).lintegral ν) ⟨g, hg⟩ ≤ (fun g => (↑g).lintegral ν) ⟨g', hg'⟩
X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞μ:Measure Xν:Measure XS:Set (X →ₛ ℝ≥0∞) := {g | ⇑g ≤ fun x => f x}hsum:∀ (g : X →ₛ ℝ≥0∞), g.lintegral μ + g.lintegral ν = g.lintegral (Measure.add μ ν) := fun g => Eq.symm (SimpleFunc.lintegral_add_measure g μ ν)hiSup:⨆ g, (↑g).lintegral (Measure.add μ ν) = ⨆ g, (↑g).lintegral μ + (↑g).lintegral ν := Eq.symm (iSup_congr fun g => hsum ↑g)hdir:IsDirectedOrder ↑S :=
{
directed := fun a =>
Subtype.casesOn (motive := fun x => ∀ (b : ↑S), ∃ c, x ≤ c ∧ b ≤ c) a fun g₁ hg₁ b =>
Subtype.casesOn b fun g₂ hg₂ =>
Exists.intro ⟨g₁ ⊔ g₂, fun x => Eq.mpr (id lintegral_add_measure._simp_1) ⟨hg₁ x, hg₂ x⟩⟩
⟨fun x => of_eq_true le_sup_left._simp_2, fun x => of_eq_true le_sup_right._simp_2⟩ }g:X →ₛ ℝ≥0∞hg:g ∈ Sg':X →ₛ ℝ≥0∞hg':g' ∈ Shgg':g ≤ g'⊢ (fun g => (↑g).lintegral ν) ⟨g, hg⟩ ≤ (fun g => (↑g).lintegral ν) ⟨g', hg'⟩
All goals completed! 🐙