4.2. 測度🔗

4.2.1. 測度🔗

定義 (測度).

X を可測空間とする。 X 上の測度とは、各可測集合 A \subseteq X に [0,\infty] の値を対応させる関数であって、次を満たすものをいう。

\mu(\emptyset) = 0 である。
A と B が可測で交わりを持たなければ、\mu(A \cup B) = \mu(A) + \mu(B) である。
A_0 \subseteq A_1 \subseteq \cdots が可測集合の増大列ならば、 \mu\left(\bigcup_{n \in \mathbb{N}} A_n\right) = \sup_{n \in \mathbb{N}} \mu(A_n) である。

Lean code

structure Measure (X : Type*) [MeasurableSpace X] where
  toFun : (A : Set X) → MeasurableSet A → ℝ≥0∞
  empty' : toFun ∅ .empty = 0
  union' : ∀ {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) (_hAB : Disjoint A B),
    toFun (A ∪ B) (hA.union hB) = toFun A hA + toFun B hB
  iUnion_of_monotone' : ∀ {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i)) (_hmono : Monotone A),
    toFun (⋃ i, A i) (.iUnion hA) = ⨆ i, toFun (A i) (hA i)

定理 (可算加法性).

A_0, A_1, \dots \subseteq X を互いに交わらない可測集合の列とする。このとき \mu\left(\bigcup_{n \in \mathbb{N}} A_n\right) = \sum_{n \in \mathbb{N}} \mu(A_n).

Lean code

theorem Measure.iUnion_of_disjoint' (μ : Measure X) {A : ℕ → Set X}
    (hd : Pairwise (Disjoint on A)) (hA : ∀ n, MeasurableSet (A n)) :
    μ.toFun (⋃ n, A n) (.iUnion hA) = ∑' n, μ.toFun (A n) (hA n) :=
  calc
    μ.toFun (⋃ n, A n) (.iUnion hA)
    _ = μ.toFun (⋃ n, accumulate A n) (.iUnion (.accumulate hA)) := byX:Type u_1inst✝:MeasurableSpace Xμ:Measure XA:ℕ → Set Xhd:Pairwise (Disjoint on A)hA:∀ (n : ℕ), MeasurableSet (A n)⊢ μ.toFun (⋃ n, A n) ⋯ = μ.toFun (⋃ n, accumulate A n) ⋯
      simp [iUnion_accumulate]All goals completed! 🐙
    _ = ⨆ n, μ.toFun (accumulate A n) (.accumulate hA n) :=
      μ.iUnion_of_monotone' (.accumulate hA) monotone_accumulate
    _ = ⨆ n, ∑ j ∈ Finset.range (n + 1), μ.toFun (A j) (hA j) :=
      iSup_congr <| Measure.accumulate_eq_sum' μ hA hd
    _ = ∑' n, μ.toFun (A n) (hA n) :=
      (ENNReal.tsum_eq_iSup_nat' (Filter.tendsto_add_atTop_nat 1)).symm

定理 (可算加法性から作る測度).

逆に、可測集合上の関数 \mu(A) が与えられていて、次を満たすとする。

\mu(\emptyset) = 0 である。
互いに交わらない可測集合の列 A_0, A_1, \dots に対して常に \mu\left(\bigcup_{n \in \mathbb{N}} A_n\right) = \sum_{n \in \mathbb{N}} \mu(A_n). が成り立つ。

このとき \mu は測度である。

Lean code

theorem Measure.iUnion_of_disjoint_countable
    (m : (A : Set X) → MeasurableSet A → ℝ≥0∞)
    (m_empty : m ∅ .empty = 0)
    (m_iUnion : ∀ {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i))
      (_hAd : Pairwise (Disjoint on A)), m (⋃ i, A i) (.iUnion hA) = ∑' i, m (A i) (hA i))
    {ι : Type*} [Countable ι] {A : ι → Set X}
    (hA : ∀ i, MeasurableSet (A i)) (hAd : Pairwise (Disjoint on A)) :
    m (⋃ i, A i) (.iUnion hA) = ∑' i, m (A i) (hA i) := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)⊢ m (⋃ i, A i) ⋯ = ∑' (i : ι), m (A i) ⋯
  classical
  cases nonempty_encodable ιintroX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ι⊢ m (⋃ i, A i) ⋯ = ∑' (i : ι), m (A i) ⋯
  let m' : Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0introX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0⊢ m (⋃ i, A i) ⋯ = ∑' (i : ι), m (A i) ⋯
  have hm' : ∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)⊢ m (⋃ i, A i) ⋯ = ∑' (i : ι), m (A i) ⋯
    intro s hsX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0s:Set Xhs:MeasurableSet s⊢ m' s = m s hs
    simp [m', hs]All goals completed! 🐙
  have hm'_empty : m' ∅ = 0 := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)⊢ m (⋃ i, A i) ⋯ = ∑' (i : ι), m (A i) ⋯ simp [m', m_empty]All goals completed! 🐙
  have hdecode : ∀ n, MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)⊢ m (⋃ i, A i) ⋯ = ∑' (i : ι), m (A i) ⋯
    intro nX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))n:ℕ⊢ MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i)
    apply Encodable.iUnion_decode₂_casesH0X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))n:ℕ⊢ MeasurableSet ∅H1X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))n:ℕ⊢ ∀ (b : ι), MeasurableSet (A b)
    ·H0X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))n:ℕ⊢ MeasurableSet ∅ exact .emptyAll goals completed! 🐙
    ·H1X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))n:ℕ⊢ ∀ (b : ι), MeasurableSet (A b) intro iH1X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))n:ℕi:ι⊢ MeasurableSet (A i)
      exact hA iAll goals completed! 🐙
  calc
    m (⋃ i, A i) (.iUnion hA)
      = m (⋃ n, ⋃ i ∈ Encodable.decode₂ ι n, A i) (.iUnion hdecode) := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ m (⋃ i, A i) ⋯ = m (⋃ n, ⋃ i ∈ Encodable.decode₂ ι n, A i) ⋯
          congre_AX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ ⋃ i, A i = ⋃ n, ⋃ i ∈ Encodable.decode₂ ι n, A i
          exact (Encodable.iUnion_decode₂ A).symmAll goals completed! 🐙
    _ = ∑' n, m (⋃ i ∈ Encodable.decode₂ ι n, A i) (hdecode n) :=
      m_iUnion hdecode (Encodable.iUnion_decode₂_disjoint_on hAd)
    _ = ∑' n, m' (⋃ i ∈ Encodable.decode₂ ι n, A i) := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ ∑' (n : ℕ), m (⋃ i ∈ Encodable.decode₂ ι n, A i) ⋯ = ∑' (n : ℕ), m' (⋃ i ∈ Encodable.decode₂ ι n, A i)
      refine tsum_congr ?_X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ ∀ (b : ℕ), m (⋃ i ∈ Encodable.decode₂ ι b, A i) ⋯ = m' (⋃ i ∈ Encodable.decode₂ ι b, A i)
      intro nX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA in:ℕ⊢ m (⋃ i ∈ Encodable.decode₂ ι n, A i) ⋯ = m' (⋃ i ∈ Encodable.decode₂ ι n, A i)
      symmX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA in:ℕ⊢ m' (⋃ i ∈ Encodable.decode₂ ι n, A i) = m (⋃ i ∈ Encodable.decode₂ ι n, A i) ⋯
      exact hm' (hdecode n)All goals completed! 🐙
    _ = ∑' i, m' (A i) := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ ∑' (n : ℕ), m' (⋃ i ∈ Encodable.decode₂ ι n, A i) = ∑' (i : ι), m' (A i)
      exact tsum_iUnion_decode₂ (β := ι) m' hm'_empty AAll goals completed! 🐙
    _ = ∑' i, m (A i) (hA i) := byX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ ∑' (i : ι), m' (A i) = ∑' (i : ι), m (A i) ⋯
      refine tsum_congr ?_X:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA i⊢ ∀ (b : ι), m' (A b) = m (A b) ⋯
      intro iX:Type u_1inst✝¹:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯ι:Type u_2inst✝:Countable ιA:ι → Set XhA:∀ (i : ι), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)val✝:Encodable ιm':Set X → ℝ≥0∞ := fun s => if hs : MeasurableSet s then m s hs else 0hm':∀ {s : Set X} (hs : MeasurableSet s), m' s = m s hs := 
  fun {s} hs =>
    of_eq_true
      (Eq.trans (congrFun' (congrArg Eq (dite_cond_eq_true (eq_true hs))) (m s hs))
        (eq_self (m s (of_eq_true (eq_true hs)))))hm'_empty:m' ∅ = 0 := 
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (Eq.trans (dite_cond_eq_true MeasurableSet.empty._simp_1) m_empty)) 0) (eq_self 0))hdecode:∀ (n : ℕ), MeasurableSet (⋃ i ∈ Encodable.decode₂ ι n, A i) := fun n => Encodable.iUnion_decode₂_cases MeasurableSet.empty fun i => hA ii:ι⊢ m' (A i) = m (A i) ⋯
      exact hm' (hA i)All goals completed! 🐙

theorem Measure.union_of_countablyAdditive
    (m : (A : Set X) → MeasurableSet A → ℝ≥0∞)
    (m_empty : m ∅ .empty = 0)
    (m_iUnion : ∀ {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i))
      (_hAd : Pairwise (Disjoint on A)), m (⋃ i, A i) (.iUnion hA) = ∑' i, m (A i) (hA i))
    {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : Disjoint A B) :
    m (A ∪ B) (hA.union hB) = m A hA + m B hB := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet BhAB:Disjoint A B⊢ m (A ∪ B) ⋯ = m A hA + m B hB
  let C : Bool → Set X := fun b ↦ cond b A BX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet BhAB:Disjoint A BC:Bool → Set X := fun b => bif b then A else B⊢ m (A ∪ B) ⋯ = m A hA + m B hB
  have hC : ∀ b, MeasurableSet (C b) := fun b ↦ MeasurableSet.cond hA hBX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet BhAB:Disjoint A BC:Bool → Set X := fun b => bif b then A else BhC:∀ (b : Bool), MeasurableSet (C b) := fun b => MeasurableSet.cond hA hB⊢ m (A ∪ B) ⋯ = m A hA + m B hB
  have hCd : Pairwise (Disjoint on C) := (pairwise_on_bool fun ⦃x y⦄ h ↦ h.symm).mpr hABX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet BhAB:Disjoint A BC:Bool → Set X := fun b => bif b then A else BhC:∀ (b : Bool), MeasurableSet (C b) := fun b => MeasurableSet.cond hA hBhCd:Pairwise (Disjoint on C) := (pairwise_on_bool fun ⦃x y⦄ h => Disjoint.symm h).mpr hAB⊢ m (A ∪ B) ⋯ = m A hA + m B hB
  simpa [union_eq_iUnion, C, tsum_fintype] using
    (iUnion_of_disjoint_countable m m_empty m_iUnion hC hCd)All goals completed! 🐙

lemma Measure.accumulate_eq_sum_of_countablyAdditive
    (m : (A : Set X) → MeasurableSet A → ℝ≥0∞)
    (m_empty : m ∅ .empty = 0)
    (m_iUnion : ∀ {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i))
      (_hAd : Pairwise (Disjoint on A)), m (⋃ i, A i) (.iUnion hA) = ∑' i, m (A i) (hA i))
    {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i))
    (hAd : Pairwise (Disjoint on A)) (n : ℕ) :
    m (accumulate A n) (MeasurableSet.accumulate hA n) =
      ∑ i ∈ Finset.range (n + 1), m (A i) (hA i) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)n:ℕ⊢ m (accumulate A n) ⋯ = ∑ i ∈ Finset.range (n + 1), m (A i) ⋯
  induction n with
  | zero =>zeroX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)⊢ m (accumulate A 0) ⋯ = ∑ i ∈ Finset.range (0 + 1), m (A i) ⋯ simpAll goals completed! 🐙
  | succ n ih =>succX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)n:ℕih:m (accumulate A n) ⋯ = ∑ i ∈ Finset.range (n + 1), m (A i) ⋯⊢ m (accumulate A (n + 1)) ⋯ = ∑ i ∈ Finset.range (n + 1 + 1), m (A i) ⋯
      calc
        m (accumulate A (n + 1)) (MeasurableSet.accumulate hA (n + 1))
            = m (accumulate A n) (MeasurableSet.accumulate hA n) + m (A (n + 1)) (hA (n + 1)) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)n:ℕih:m (accumulate A n) ⋯ = ∑ i ∈ Finset.range (n + 1), m (A i) ⋯⊢ m (accumulate A (n + 1)) ⋯ = m (accumulate A n) ⋯ + m (A (n + 1)) ⋯
                simpa [Set.accumulate_succ] using
                  (union_of_countablyAdditive m m_empty m_iUnion
                    (MeasurableSet.accumulate hA n) (hA (n + 1))
                    (Set.disjoint_accumulate hAd (Nat.lt_succ_self n)))All goals completed! 🐙
        _ = ∑ i ∈ Finset.range (n + 1), m (A i) (hA i) + m (A (n + 1)) (hA (n + 1)) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)n:ℕih:m (accumulate A n) ⋯ = ∑ i ∈ Finset.range (n + 1), m (A i) ⋯⊢ m (accumulate A n) ⋯ + m (A (n + 1)) ⋯ = ∑ i ∈ Finset.range (n + 1), m (A i) ⋯ + m (A (n + 1)) ⋯
              rw [ih]All goals completed! 🐙
        _ = ∑ i ∈ Finset.range (n + 2), m (A i) (hA i) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Disjoint on A)n:ℕih:m (accumulate A n) ⋯ = ∑ i ∈ Finset.range (n + 1), m (A i) ⋯⊢ ∑ i ∈ Finset.range (n + 1), m (A i) ⋯ + m (A (n + 1)) ⋯ = ∑ i ∈ Finset.range (n + 2), m (A i) ⋯
              exact (Finset.sum_range_succ (f := fun i => m (A i) (hA i)) (n := n + 1)).symmAll goals completed! 🐙

theorem Measure.iUnion_of_monotone_of_countablyAdditive
    (m : (A : Set X) → MeasurableSet A → ℝ≥0∞)
    (m_empty : m ∅ .empty = 0)
    (m_iUnion : ∀ {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i))
      (_hAd : Pairwise (Disjoint on A)), m (⋃ i, A i) (.iUnion hA) = ∑' i, m (A i) (hA i))
    {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i)) (hmono : Monotone A) :
    m (⋃ i, A i) (.iUnion hA) = ⨆ i, m (A i) (hA i) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone A⊢ m (⋃ i, A i) ⋯ = ⨆ i, m (A i) ⋯
  let D : ℕ → Set X := disjointed AX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed A⊢ m (⋃ i, A i) ⋯ = ⨆ i, m (A i) ⋯
  have hD : ∀ i, MeasurableSet (D i) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone A⊢ m (⋃ i, A i) ⋯ = ⨆ i, m (A i) ⋯
    intro iX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed Ai:ℕ⊢ MeasurableSet (D i)
    dsimp only [D]X:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed Ai:ℕ⊢ MeasurableSet (disjointed A i)
    simpa [D] using disjointedRec (fun _ j ht => MeasurableSet.diff ht <| hA j) (hA i)All goals completed! 🐙
  calc
    m (⋃ i, A i) (.iUnion hA) = m (⋃ i, D i) (.iUnion hD) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))⊢ m (⋃ i, A i) ⋯ = m (⋃ i, D i) ⋯
      simp [D, iUnion_disjointed]All goals completed! 🐙
    _ = ∑' i, m (D i) (hD i) := m_iUnion hD (disjoint_disjointed A)
    _ = ⨆ n, ∑ i ∈ Finset.range (n + 1), m (D i) (hD i) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))⊢ ∑' (i : ℕ), m (D i) ⋯ = ⨆ n, ∑ i ∈ Finset.range (n + 1), m (D i) ⋯
      exact ENNReal.tsum_eq_iSup_nat' (Filter.tendsto_add_atTop_nat 1)All goals completed! 🐙
    _ = ⨆ n, m (accumulate D n) (MeasurableSet.accumulate hD n) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))⊢ ⨆ n, ∑ i ∈ Finset.range (n + 1), m (D i) ⋯ = ⨆ n, m (accumulate D n) ⋯
      refine iSup_congr fun n ↦ ?_X:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))n:ℕ⊢ ∑ i ∈ Finset.range (n + 1), m (D i) ⋯ = m (accumulate D n) ⋯
      symmX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))n:ℕ⊢ m (accumulate D n) ⋯ = ∑ i ∈ Finset.range (n + 1), m (D i) ⋯
      exact accumulate_eq_sum_of_countablyAdditive m m_empty m_iUnion hD (disjoint_disjointed A) nAll goals completed! 🐙
    _ = ⨆ n, m (A n) (hA n) := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))⊢ ⨆ n, m (accumulate D n) ⋯ = ⨆ n, m (A n) ⋯
      refine iSup_congr fun n ↦ ?_X:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))n:ℕ⊢ m (accumulate D n) ⋯ = m (A n) ⋯
      have hacc' : accumulate D n = A n := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))⊢ ⨆ n, m (accumulate D n) ⋯ = ⨆ n, m (A n) ⋯
        calc
          accumulate D n = partialSups (disjointed A) n := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone AD:ℕ → Set X := disjointed AhD:∀ (i : ℕ), MeasurableSet (D i) := fun i => id (disjointedRec (fun x j ht => MeasurableSet.diff ht (hA j)) (hA i))n:ℕ⊢ accumulate D n = (partialSups (disjointed A)) n
            simpa [D] using congrArg (fun f => f n) (partialSups_eq_accumulate (disjointed A)).symmAll goals completed! 🐙
          _ = partialSups A n := congrArg (fun f => f n) (partialSups_disjointed A)
          _ = A n := congrArg (fun f => f n) (Monotone.partialSups_eq hmono)
      simp [hacc']All goals completed! 🐙

/-- Construct a `Measure` from a countably additive function on measurable sets. Since the current
`Measure` structure also stores continuity from below for monotone sequences, that property is
derived from countable additivity. -/
def Measure.ofCountablyAdditive
    (m : (A : Set X) → MeasurableSet A → ℝ≥0∞)
    (m_empty : m ∅ .empty = 0)
    (m_iUnion : ∀ {A : ℕ → Set X} (hA : ∀ i, MeasurableSet (A i))
      (_hAd : Pairwise (Disjoint on A)), m (⋃ i, A i) (.iUnion hA) = ∑' i, m (A i) (hA i)) :
    Measure X where
  toFun := m
  empty' := m_empty
  union' := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯⊢ ∀ {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B), Disjoint A B → m (A ∪ B) ⋯ = m A hA + m B hB
    intro A BX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set X⊢ ∀ (hA : MeasurableSet A) (hB : MeasurableSet B), Disjoint A B → m (A ∪ B) ⋯ = m A hA + m B hB hAX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet A⊢ ∀ (hB : MeasurableSet B), Disjoint A B → m (A ∪ B) ⋯ = m A hA + m B hB hBX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet B⊢ Disjoint A B → m (A ∪ B) ⋯ = m A hA + m B hB hABX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:Set XB:Set XhA:MeasurableSet AhB:MeasurableSet BhAB:Disjoint A B⊢ m (A ∪ B) ⋯ = m A hA + m B hB
    exact union_of_countablyAdditive m m_empty m_iUnion hA hB hABAll goals completed! 🐙
  iUnion_of_monotone' := byX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯⊢ ∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)), Monotone A → m (⋃ i, A i) ⋯ = ⨆ i, m (A i) ⋯
    intro A hAX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Monotone A → m (⋃ i, A i) ⋯ = ⨆ i, m (A i) ⋯ hmonoX:Type u_1inst✝:MeasurableSpace Xm:(A : Set X) → MeasurableSet A → ℝ≥0∞m_empty:m ∅ ⋯ = 0m_iUnion:∀ {A : ℕ → Set X} (hA : ∀ (i : ℕ), MeasurableSet (A i)),
  Pairwise (Disjoint on A) → m (⋃ i, A i) ⋯ = ∑' (i : ℕ), m (A i) ⋯A:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hmono:Monotone A⊢ m (⋃ i, A i) ⋯ = ⨆ i, m (A i) ⋯
    exact iUnion_of_monotone_of_countablyAdditive m m_empty m_iUnion hA hmonoAll goals completed! 🐙