[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => ↑↑(f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map (fun μ => ↑↑μ s) (MeasurableSpace.map f inst✝)
[PROOFSTEP]
rw [MeasurableSpace.map_comp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → Measure α
h : ∀ (s : Set α), MeasurableSet s → Measurable fun b => ↑↑(f b) s
s : Set α
hs : MeasurableSet s
⊢ borel ℝ≥0∞ ≤ MeasurableSpace.map ((fun μ => ↑↑μ s) ∘ f) inst✝
[PROOFSTEP]
exact h s hs
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
⊢ MeasurableAdd₂ (Measure α)
[PROOFSTEP]
refine' ⟨Measure.measurable_of_measurable_coe _ fun s hs => _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(b.fst + b.snd) s
[PROOFSTEP]
simp_rw [Measure.coe_add, Pi.add_apply]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b.fst s + ↑↑b.snd s
[PROOFSTEP]
refine' Measurable.add _ _
[GOAL]
case refine'_1
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b.fst s
[PROOFSTEP]
exact (Measure.measurable_coe hs).comp measurable_fst
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α✝
inst✝ : MeasurableSpace β
α : Type u_3
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b.snd s
[PROOFSTEP]
exact (Measure.measurable_coe hs).comp measurable_snd
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ Measurable fun μ => map f μ
[PROOFSTEP]
refine' measurable_of_measurable_coe _ fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(map f b) s
[PROOFSTEP]
simp_rw [map_apply hf hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑b (f ⁻¹' s)
[PROOFSTEP]
exact measurable_coe (hf hs)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ Measurable dirac
[PROOFSTEP]
refine' measurable_of_measurable_coe _ fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(dirac b) s
[PROOFSTEP]
simp_rw [dirac_apply' _ hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => indicator s 1 b
[PROOFSTEP]
exact measurable_one.indicator hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ => ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
simp only [lintegral_eq_iSup_eapprox_lintegral, hf, SimpleFunc.lintegral]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun μ =>
    ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n),
        x * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {x})
[PROOFSTEP]
refine' measurable_iSup fun n => Finset.measurable_sum _ fun i _ => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => i * ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
[PROOFSTEP]
refine' Measurable.const_mul _ _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → ℝ≥0∞
hf : Measurable f
n : ℕ
i : ℝ≥0∞
x✝ : i ∈ SimpleFunc.range (SimpleFunc.eapprox (fun x => f x) n)
⊢ Measurable fun μ => ↑↑μ (↑(SimpleFunc.eapprox (fun x => f x) n) ⁻¹' {i})
[PROOFSTEP]
exact measurable_coe ((SimpleFunc.eapprox f n).measurableSet_preimage _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
⊢ (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) ∅ (_ : MeasurableSet ∅) = 0
[PROOFSTEP]
simp only [measure_empty, lintegral_const, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
⊢ ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
        ∑' (i : ℕ), (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (f i) (_ : MeasurableSet (f i))
[PROOFSTEP]
intro f hf h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
⊢ (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (⋃ (i : ℕ), f i) (_ : MeasurableSet (⋃ (b : ℕ), f b)) =
    ∑' (i : ℕ), (fun s x => ∫⁻ (μ : Measure α), ↑↑μ s ∂m) (f i) (_ : MeasurableSet (f i))
[PROOFSTEP]
simp_rw [measure_iUnion h hf]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
⊢ ∫⁻ (μ : Measure α), ∑' (i : ℕ), ↑↑μ (f i) ∂m = ∑' (i : ℕ), ∫⁻ (μ : Measure α), ↑↑μ (f i) ∂m
[PROOFSTEP]
apply lintegral_tsum
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
⊢ ∀ (i : ℕ), AEMeasurable fun a => ↑↑a (f i)
[PROOFSTEP]
intro i
[GOAL]
case hf
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
h : Pairwise (Disjoint on f)
i : ℕ
⊢ AEMeasurable fun a => ↑↑a (f i)
[PROOFSTEP]
exact (measurable_coe (hf i)).aemeasurable
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ join 0 = 0
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ ↑↑(join 0) s = ↑↑0 s
[PROOFSTEP]
simp only [hs, join_apply, lintegral_zero_measure, coe_zero, Pi.zero_apply]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ↑↑(join b) s
[PROOFSTEP]
simp only [join_apply hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (μ : Measure α), ↑↑μ s ∂b
[PROOFSTEP]
exact measurable_lintegral (measurable_coe hs)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : α), f x ∂join m = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
[PROOFSTEP]
simp_rw [lintegral_eq_iSup_eapprox_lintegral hf, SimpleFunc.lintegral,
  join_apply (SimpleFunc.measurableSet_preimage _ _)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n),
        x * ∫⁻ (μ : Measure α), ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α),
      ⨆ (n : ℕ), ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n), x * ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
[PROOFSTEP]
suffices
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ n r, Measurable (f n r)) →
      Monotone (fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ n, ∑ r in s n, r * ∫⁻ μ, f n r μ ∂m = ∫⁻ μ, ⨆ n, ∑ r in s n, r * f n r μ ∂m
  by
  refine'
    this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' { r })) _ _
  · exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
  · exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
⊢ ⨆ (n : ℕ),
      ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n),
        x * ∫⁻ (μ : Measure α), ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m =
    ∫⁻ (μ : Measure α),
      ⨆ (n : ℕ), ∑ x in SimpleFunc.range (SimpleFunc.eapprox f n), x * ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
[PROOFSTEP]
refine'
  this (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) (fun n r μ => μ (SimpleFunc.eapprox f n ⁻¹' { r })) _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
⊢ ∀ (n : ℕ) (r : ℝ≥0∞), Measurable ((fun n r μ => ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {r})) n r)
[PROOFSTEP]
exact fun n r => measurable_coe (SimpleFunc.measurableSet_preimage _ _)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
this :
  ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
⊢ Monotone fun n μ =>
    ∑ r in (fun n => SimpleFunc.range (SimpleFunc.eapprox f n)) n,
      r * (fun n r μ => ↑↑μ (↑(SimpleFunc.eapprox f n) ⁻¹' {r})) n r μ
[PROOFSTEP]
exact fun n m h μ => SimpleFunc.lintegral_mono (SimpleFunc.monotone_eapprox _ h) le_rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (s : ℕ → Finset ℝ≥0∞) (f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞),
    (∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)) →
      (Monotone fun n μ => ∑ r in s n, r * f n r μ) →
        ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m =
          ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
[PROOFSTEP]
intro s f hf hm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ (n : ℕ), ∑ r in s n, r * f n r μ ∂m
[PROOFSTEP]
rw [lintegral_iSup _ hm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ => ∑ r in s n, r * f n r μ
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ∀ (n : ℕ), Measurable fun μ => ∑ r in s n, r * f n r μ
[PROOFSTEP]
exact fun n => Finset.measurable_sum _ fun r _ => (hf _ _).const_mul _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ ⨆ (n : ℕ), ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ (n : ℕ), ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
⊢ (fun n => ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) = fun n => ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
[PROOFSTEP]
funext n
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
n : ℕ
⊢ ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r in s n, r * f n r a ∂m
[PROOFSTEP]
rw [lintegral_finset_sum (s n)]
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
n : ℕ
⊢ ∑ r in s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b in s n, ∫⁻ (a : Measure α), b * f n b a ∂m
[PROOFSTEP]
simp_rw [lintegral_const_mul _ (hf _ _)]
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure (Measure α)
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
s : ℕ → Finset ℝ≥0∞
f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞
hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)
hm : Monotone fun n μ => ∑ r in s n, r * f n r μ
n : ℕ
⊢ ∀ (b : ℝ≥0∞), b ∈ s n → Measurable fun a => b * f n b a
[PROOFSTEP]
exact fun r _ => (hf _ _).const_mul _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
⊢ bind 0 f = 0
[PROOFSTEP]
simp [bind]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
⊢ bind m 0 = 0
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(bind m 0) s = ↑↑0 s
[PROOFSTEP]
simp only [bind, hs, join_apply, coe_zero, Pi.zero_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (μ : Measure β), ↑↑μ s ∂map 0 m = 0
[PROOFSTEP]
rw [lintegral_map (measurable_coe hs) measurable_zero]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ↑↑(OfNat.ofNat 0 a) s ∂m = 0
[PROOFSTEP]
simp only [Pi.zero_apply, coe_zero, lintegral_const, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
f : α → Measure β
s : Set β
hs : MeasurableSet s
hf : Measurable f
⊢ ↑↑(bind m f) s = ∫⁻ (a : α), ↑↑(f a) s ∂m
[PROOFSTEP]
rw [bind, join_apply hs, lintegral_map (measurable_coe hs) hf]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
⊢ bind (bind m f) g = bind m fun a => bind (f a) g
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ↑↑(bind (bind m f) g) s = ↑↑(bind m fun a => bind (f a) g) s
[PROOFSTEP]
erw [bind_apply hs hg, bind_apply hs ((measurable_bind' hg).comp hf), lintegral_bind hf ((measurable_coe hs).comp hg)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (a : α), ∫⁻ (x : β), ((fun μ => ↑↑μ s) ∘ g) x ∂f a ∂m = ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
conv_rhs => enter [2, a]; erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
| ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
enter [2, a]; erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
| ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
enter [2, a]; erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
| ∫⁻ (a : α), ↑↑(((fun m => bind m g) ∘ f) a) s ∂m
[PROOFSTEP]
enter [2, a]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
γ : Type u_3
inst✝ : MeasurableSpace γ
m : Measure α
f : α → Measure β
g : β → Measure γ
hf : Measurable f
hg : Measurable g
s : Set γ
hs : MeasurableSet s
a : α
| ↑↑(((fun m => bind m g) ∘ f) a) s
[PROOFSTEP]
erw [bind_apply hs hg]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
⊢ bind (dirac a) f = f a
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ↑↑(bind (dirac a) f) s = ↑↑(f a) s
[PROOFSTEP]
erw [bind_apply hs hf, lintegral_dirac' a ((measurable_coe hs).comp hf)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → Measure β
hf : Measurable f
a : α
s : Set β
hs : MeasurableSet s
⊢ ((fun μ => ↑↑μ s) ∘ f) a = ↑↑(f a) s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
⊢ bind m dirac = m
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
m : Measure α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(bind m dirac) s = ↑↑m s
[PROOFSTEP]
simp only [bind_apply hs measurable_dirac, dirac_apply' _ hs, lintegral_indicator 1 hs, Pi.one_apply, lintegral_one,
  restrict_apply, MeasurableSet.univ, univ_inter]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure α)
⊢ join μ = bind μ id
[PROOFSTEP]
rw [bind, map_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
⊢ join (map (map f) μ) = map f (join μ)
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ↑↑(join (map (map f) μ)) s = ↑↑(map f (join μ)) s
[PROOFSTEP]
rw [join_apply hs, map_apply hf hs, join_apply (hf hs), lintegral_map (measurable_coe hs) (measurable_map f hf)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : Measure α), ↑↑(map f a) s ∂μ = ∫⁻ (μ : Measure α), ↑↑μ (f ⁻¹' s) ∂μ
[PROOFSTEP]
simp_rw [map_apply hf hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join (map join μ) = join (join μ)
[PROOFSTEP]
show bind μ join = join (join μ)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = join (join μ)
[PROOFSTEP]
rw [join_eq_bind, join_eq_bind, bind_bind measurable_id measurable_id]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ bind μ join = bind μ fun a => bind (id a) id
[PROOFSTEP]
apply congr_arg (bind μ)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
⊢ join = fun a => bind (id a) id
[PROOFSTEP]
funext ν
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure (Measure (Measure α))
ν : Measure (Measure α)
⊢ join ν = bind (id ν) id
[PROOFSTEP]
exact join_eq_bind ν
