7.3. ディラック測度🔗

定義.

X を可測空間とし、x \in X とする。 ディラック測度 \delta_x とは、任意の可測集合 A \subseteq X に対して \delta_x(A) \coloneqq 1_A(x) で定まる X 上の測度である。

Lean code

def Measure.dirac (x : X) : Measure X :=
  Measure.ofMeasurable (fun A _ ↦ indicator A (fun _ ↦ 1) x) (byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:X⊢ (fun A x_1 => A.indicator (fun x => 1) x) ∅ ⋯ = 0 simpAll goals completed! 🐙) <| byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:X⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
  Pairwise (Function.onFun Disjoint f) →
    (fun A x_1 => A.indicator (fun x => 1) x) (⋃ i, f i) ⋯ =
      ∑' (i : ℕ), (fun A x_1 => A.indicator (fun x => 1) x) (f i) ⋯
    intro A hAX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)⊢ Pairwise (Function.onFun Disjoint A) →
  (fun A x_1 => A.indicator (fun x => 1) x) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x_1 => A.indicator (fun x => 1) x) (A i) ⋯ hAdX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (fun A x_1 => A.indicator (fun x => 1) x) (⋃ i, A i) ⋯ = ∑' (i : ℕ), (fun A x_1 => A.indicator (fun x => 1) x) (A i) ⋯
    simp onlyX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)⊢ (⋃ i, A i).indicator (fun x => 1) x = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
    by_cases hx : x ∈ (⋃ i, A i)posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:x ∈ ⋃ i, A i⊢ (⋃ i, A i).indicator (fun x => 1) x = ∑' (i : ℕ), (A i).indicator (fun x => 1) xnegX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:x ∉ ⋃ i, A i⊢ (⋃ i, A i).indicator (fun x => 1) x = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
    ·posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:x ∈ ⋃ i, A i⊢ (⋃ i, A i).indicator (fun x => 1) x = ∑' (i : ℕ), (A i).indicator (fun x => 1) x rw [indicator_of_mem hx]posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:x ∈ ⋃ i, A i⊢ 1 = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
      simp only [mem_iUnion] at hxposX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A i⊢ 1 = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
      have ⟨i, hi⟩ := hxposX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A i⊢ 1 = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
      have : ∑' (i : ℕ), (A i).indicator (fun x ↦ (1 : ℝ≥0∞)) x =
          (A i).indicator (fun x ↦ (1 : ℝ≥0∞)) x +
            ∑' k : ℕ, if k = i then 0 else (A k).indicator (fun x ↦ (1 : ℝ≥0∞)) x := byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:X⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
  Pairwise (Function.onFun Disjoint f) →
    (fun A x_1 => A.indicator (fun x => 1) x) (⋃ i, f i) ⋯ =
      ∑' (i : ℕ), (fun A x_1 => A.indicator (fun x => 1) x) (f i) ⋯
        convert tsum_eq_add_tsum_ite (f := fun i ↦ (A i).indicator (fun x ↦ (1 : ℝ≥0∞)) x) iAll goals completed! 🐙
      rw [this]posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)⊢ 1 = (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x
      rw [indicator_of_mem hi]posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)⊢ 1 = 1 + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x
      suffices (∑' k : ℕ, if k = i then 0 else (A k).indicator (fun x ↦ (1 : ℝ≥0∞)) x) = 0 byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis✝:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)this:(∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x) = 0 := ?m.345⊢ 1 = 1 + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x
        rw [this]X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis✝:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)this:(∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x) = 0 := ?m.345⊢ 1 = 1 + 0
        simpAll goals completed! 🐙
      refine ENNReal.tsum_eq_zero.mpr ?_posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)⊢ ∀ (i_1 : ℕ), (if i_1 = i then 0 else (A i_1).indicator (fun x => 1) x) = 0
      intro kposX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕ⊢ (if k = i then 0 else (A k).indicator (fun x => 1) x) = 0
      simp only [ite_eq_left_iff, indicator_apply_eq_zero, one_ne_zero, imp_false]posX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕ⊢ ¬k = i → x ∉ A k
      intro hik hAkposX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕhik:¬k = ihAk:x ∈ A k⊢ False
      have hx : x ∈ A i ∩ A k := byX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:X⊢ ∀ ⦃f : ℕ → Set X⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
  Pairwise (Function.onFun Disjoint f) →
    (fun A x_1 => A.indicator (fun x => 1) x) (⋃ i, f i) ⋯ =
      ∑' (i : ℕ), (fun A x_1 => A.indicator (fun x => 1) x) (f i) ⋯
        exact mem_inter hi hAkAll goals completed! 🐙
      apply hAd hik _ _ hxX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx✝:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕhik:¬k = ihAk:x ∈ A khx:x ∈ A i ∩ A k := mem_inter hi hAk⊢ A i ∩ A k ≤ A kX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx✝:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕhik:¬k = ihAk:x ∈ A khx:x ∈ A i ∩ A k := mem_inter hi hAk⊢ A i ∩ A k ≤ A i
      ·X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx✝:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕhik:¬k = ihAk:x ∈ A khx:x ∈ A i ∩ A k := mem_inter hi hAk⊢ A i ∩ A k ≤ A k simpAll goals completed! 🐙
      ·X:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx✝:∃ i, x ∈ A ii:ℕhi:x ∈ A ithis:∑' (i : ℕ), (A i).indicator (fun x => 1) x =
  (A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x := 
  Eq.mpr
    (eq_of_heq
      ((fun α a a_1 a' e'_3 =>
          Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a')) e'_3
            (fun h =>
              Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a'))
                (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3)
            (Eq.refl a') (HEq.refl e'_3))
        ℝ≥0∞ (∑' (i : ℕ), (A i).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
        ((A i).indicator (fun x => 1) x + ∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
        (eq_of_heq
          ((fun α β γ self a a_1 a' e'_6 =>
              Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_6 ≍ x → a + a_1 ≍ a + a') e'_6
                (fun h =>
                  Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a + a_1 ≍ a + a')
                    (fun e_6 h => HEq.refl (a + a_1)) (Eq.symm h) e'_6)
                (Eq.refl a') (HEq.refl e'_6))
            ℝ≥0∞ ℝ≥0∞ ℝ≥0∞ instHAdd ((A i).indicator (fun x => 1) x)
            (∑' (k : ℕ), if k = i then 0 else (A k).indicator (fun x => 1) x)
            (∑' (x_1 : ℕ), if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
            (eq_of_heq
              ((fun α β inst inst_1 f f' e'_5 L =>
                  Eq.casesOn (motive := fun a x => f' = a → e'_5 ≍ x → tsum f L ≍ tsum f' L) e'_5
                    (fun h =>
                      Eq.ndrec (motive := fun f' => ∀ (e_5 : f = f'), e_5 ≍ Eq.refl f → tsum f L ≍ tsum f' L)
                        (fun e_5 h => HEq.refl (tsum f L)) (Eq.symm h) e'_5)
                    (Eq.refl f') (HEq.refl e'_5))
                ℝ≥0∞ ℕ instAddCommMonoid instTopologicalSpace
                (fun k => if k = i then 0 else (A k).indicator (fun x => 1) x)
                (fun x_1 => if x_1 = i then 0 else (A x_1).indicator (fun x => 1) x)
                (funext fun x_1 =>
                  ite_congr (Eq.refl (x_1 = i)) (fun a => Eq.refl 0) fun a =>
                    Eq.refl ((A x_1).indicator (fun x => 1) x))))))))
    (tsum_eq_add_tsum_ite i)k:ℕhik:¬k = ihAk:x ∈ A khx:x ∈ A i ∩ A k := mem_inter hi hAk⊢ A i ∩ A k ≤ A i simpAll goals completed! 🐙
    ·negX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:x ∉ ⋃ i, A i⊢ (⋃ i, A i).indicator (fun x => 1) x = ∑' (i : ℕ), (A i).indicator (fun x => 1) x rw [indicator_of_notMem hx]negX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:x ∉ ⋃ i, A i⊢ 0 = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
      simp only [mem_iUnion, not_exists] at hxnegX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∀ (x_1 : ℕ), x ∉ A x_1⊢ 0 = ∑' (i : ℕ), (A i).indicator (fun x => 1) x
      symmnegX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∀ (x_1 : ℕ), x ∉ A x_1⊢ ∑' (i : ℕ), (A i).indicator (fun x => 1) x = 0
      refine ENNReal.tsum_eq_zero.mpr ?_negX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∀ (x_1 : ℕ), x ∉ A x_1⊢ ∀ (i : ℕ), (A i).indicator (fun x => 1) x = 0
      intro inegX:Type u_1Y:Type u_2Z:Type u_3inst✝²:MeasurableSpace Xinst✝¹:MeasurableSpace Yinst✝:MeasurableSpace Zx:XA:ℕ → Set XhA:∀ (i : ℕ), MeasurableSet (A i)hAd:Pairwise (Function.onFun Disjoint A)hx:∀ (x_1 : ℕ), x ∉ A x_1i:ℕ⊢ (A i).indicator (fun x => 1) x = 0
      rw [indicator_of_notMem (hx i)]All goals completed! 🐙

@[simp]
theorem Measure.dirac_apply (x : X) (A : Set X) (hA : MeasurableSet A) :
    Measure.dirac x A = indicator A (fun _ ↦ 1) x := byX:Type u_1inst✝:MeasurableSpace Xx:XA:Set XhA:MeasurableSet A⊢ (dirac x) A = A.indicator (fun x => 1) x
  rw [Measure.dirac, Measure.ofMeasurable_apply _ hA]All goals completed! 🐙

補題.

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

Lean code

theorem Measure.dirac_lintegral (f : X → ℝ≥0∞) (hf : Measurable f) (x : X) :
    ∫⁻ y, f y ∂(dirac x) = f x := byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ ∫⁻ (y : X), f y ∂dirac x = f x
  have : f =ᶠ[ae (dirac x)] Function.const X (f x) := byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ ∫⁻ (y : X), f y ∂dirac x = f x
    have : ∀ᵐ y ∂(dirac x), y ∈ { y | f y = f x } := byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ ∫⁻ (y : X), f y ∂dirac x = f x
      rw [eventually_mem_set, mem_ae_iff, dirac_apply]X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ {y | f y = f x}ᶜ.indicator (fun x => 1) x = 0hAX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ MeasurableSet {y | f y = f x}ᶜ
      ·X:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ {y | f y = f x}ᶜ.indicator (fun x => 1) x = 0 simpAll goals completed! 🐙
      ·hAX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ MeasurableSet {y | f y = f x}ᶜ apply MeasurableSet.complhA.aX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ MeasurableSet {y | f y = f x}
        suffices MeasurableSet (f ⁻¹' {f x}) from thishA.aX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:X⊢ MeasurableSet (f ⁻¹' {f x})
        apply hf (measurableSet_singleton (f x))All goals completed! 🐙
    filter_upwards [this] with y hyhX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:Xthis:∀ᵐ (y : X) ∂dirac x, y ∈ {y | f y = f x} := 
  Eq.mpr (id (congrArg (fun _a => _a) (propext eventually_mem_set)))
    (Eq.mpr (id (congrArg (fun _a => _a) (propext mem_ae_iff)))
      (Eq.mpr
        (id
          (congrArg (fun _a => _a = 0)
            (dirac_apply x {y | f y = f x}ᶜ
              (MeasurableSet.compl
                (have this := hf (measurableSet_singleton (f x));
                this)))))
        (of_eq_true
          (Eq.trans
            (congrFun'
              (congrArg Eq
                (indicator_of_notMem
                  (of_eq_true
                    (Eq.trans
                      (congrArg Not
                        (Eq.trans (mem_compl_iff._simp_1 {y | f y = f x} x)
                          (Eq.trans (congrArg Not (eq_self (f x))) not_true_eq_false)))
                      not_false_eq_true))
                  fun x => 1))
              0)
            (eq_self 0)))))y:Xhy:f y = f x⊢ f y = Function.const X (f x) y using byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:Xthis:∀ᵐ (y : X) ∂dirac x, y ∈ {y | f y = f x} := 
  Eq.mpr (id (congrArg (fun _a => _a) (propext eventually_mem_set)))
    (Eq.mpr (id (congrArg (fun _a => _a) (propext mem_ae_iff)))
      (Eq.mpr
        (id
          (congrArg (fun _a => _a = 0)
            (dirac_apply x {y | f y = f x}ᶜ
              (MeasurableSet.compl
                (have this := hf (measurableSet_singleton (f x));
                this)))))
        (of_eq_true
          (Eq.trans
            (congrFun'
              (congrArg Eq
                (indicator_of_notMem
                  (of_eq_true
                    (Eq.trans
                      (congrArg Not
                        (Eq.trans (mem_compl_iff._simp_1 {y | f y = f x} x)
                          (Eq.trans (congrArg Not (eq_self (f x))) not_true_eq_false)))
                      not_false_eq_true))
                  fun x => 1))
              0)
            (eq_self 0)))))y:Xhy:f y = f x⊢ f y = Function.const X (f x) y simpa using hyAll goals completed! 🐙
  apply (lintegral_congr_ae this).trans (byX:Type u_1inst✝:MeasurableSpace Xf:X → ℝ≥0∞hf:Measurable fx:Xthis:f =ᶠ[ae (dirac x)] Function.const X (f x) := 
  have this :=
    Eq.mpr (id (congrArg (fun _a => _a) (propext eventually_mem_set)))
      (Eq.mpr (id (congrArg (fun _a => _a) (propext mem_ae_iff)))
        (Eq.mpr
          (id
            (congrArg (fun _a => _a = 0)
              (dirac_apply x {y | f y = f x}ᶜ
                (MeasurableSet.compl
                  (have this := hf (measurableSet_singleton (f x));
                  this)))))
          (of_eq_true
            (Eq.trans
              (congrFun'
                (congrArg Eq
                  (indicator_of_notMem
                    (of_eq_true
                      (Eq.trans
                        (congrArg Not
                          (Eq.trans (mem_compl_iff._simp_1 {y | f y = f x} x)
                            (Eq.trans (congrArg Not (eq_self (f x))) not_true_eq_false)))
                        not_false_eq_true))
                    fun x => 1))
                0)
              (eq_self 0)))));
  mp_mem this (univ_mem' (id fun y hy => id hy))⊢ ∫⁻ (a : X), Function.const X (f x) a ∂dirac x = f x simpAll goals completed! 🐙)