α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
have m := @measurable_prod_mk_left
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄,
    MeasurableSet s → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (Set.indicator s fun x => c)

case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) f →
            (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) g →
              (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f + g)

case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)) →
          (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) fun x => ⨆ (n : ℕ), f n x
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
refine' Measurable.ennreal_induction (P := fun f => Measurable fun (x : α) => ∫⁻ y, f (x, y) ∂ν)
  _ _ _
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ∫⁻ (y : β), Set.indicator s (fun x => c) (x, y) ∂ν
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄,
    MeasurableSet s → (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (Set.indicator s fun x => c)
intro c s hs
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ∫⁻ (y : β), Set.indicator (Prod.mk x ⁻¹' s) ((fun x => c) ∘ Prod.mk x) y ∂ν
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ∫⁻ (y : β), Set.indicator s (fun x => c) (x, y) ∂ν
simp only [← indicator_comp_right]
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => c * ↑↑ν (Prod.mk x ⁻¹' s)
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => ∫⁻ (y : β), Set.indicator (Prod.mk x ⁻¹' s) ((fun x => c) ∘ Prod.mk x) y ∂ν
suffices Measurable fun x => c * ν (Prod.mk x ⁻¹' s) by simpa [lintegral_indicator _ (m hs)]
no goals
case refine'_1
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x => c * ↑↑ν (Prod.mk x ⁻¹' s)
exact (measurable_measure_prod_mk_left hs).const_mul _
no goals
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
c : ℝ≥0∞
s : Set (α × β)
hs : MeasurableSet s
this : Measurable fun x => c * ↑↑ν (Prod.mk x ⁻¹' s)
⊢ Measurable fun x => ∫⁻ (y : β), Set.indicator (Prod.mk x ⁻¹' s) ((fun x => c) ∘ Prod.mk x) y ∂ν
simpa [lintegral_indicator _ (m hs)]
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), (f + g) (x, y) ∂ν
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
⊢ ∀ ⦃f g : α × β → ℝ≥0∞⦄,
    Disjoint (support f) (support g) →
      Measurable f →
        Measurable g →
          (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) f →
            (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) g →
              (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f + g)
rintro f g - hf - h2f h2g
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), (f + g) (x, y) ∂ν
simp only [Pi.add_apply]
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => (∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν) + ∫⁻ (a : β), g (x, a) ∂ν
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m :
  ∀ {α : Type ?u.3611327} {β : Type ?u.3611326} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α},
    Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), f (x, y) + g (x, y) ∂ν
conv => enter [1, x]; erw [lintegral_add_left (hf.comp m)]
no goals
case refine'_2
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f g : α × β → ℝ≥0∞
hf : Measurable f
h2f : Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
h2g : Measurable fun x => ∫⁻ (y : β), g (x, y) ∂ν
⊢ Measurable fun x => (∫⁻ (a : β), (f ∘ Prod.mk x) a ∂ν) + ∫⁻ (a : β), g (x, a) ∂ν
exact h2f.add h2g
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
⊢ ∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)) →
          (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) fun x => ⨆ (n : ℕ), f n x
intro f hf h2f h3f
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
this : Measurable fun b => ⨆ (i : ℕ), ∫⁻ (y : β), f i (b, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν
have := measurable_iSup h3f
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
this✝ : Measurable fun b => ⨆ (i : ℕ), ∫⁻ (y : β), f i (b, y) ∂ν
this : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
this : Measurable fun b => ⨆ (i : ℕ), ∫⁻ (y : β), f i (b, y) ∂ν
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν
have : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
this✝ : Measurable fun b => ⨆ (i : ℕ), ∫⁻ (y : β), f i (b, y) ∂ν
this : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ Measurable fun x => ⨆ (n : ℕ), ∫⁻ (a : β), (f n ∘ Prod.mk x) a ∂ν
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
this✝ : Measurable fun b => ⨆ (i : ℕ), ∫⁻ (y : β), f i (b, y) ∂ν
this : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ Measurable fun x => ∫⁻ (y : β), (fun x => ⨆ (n : ℕ), f n x) (x, y) ∂ν
conv => enter [1, x]; erw [lintegral_iSup (fun n => (hf n).comp m) (this x)]
no goals
case refine'_3
α : Type u_2
α' : Type ?u.3342539
β : Type u_1
β' : Type ?u.3342545
γ : Type ?u.3342548
E : Type ?u.3342551
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α
ν ν' : MeasureTheory.Measure β
τ : MeasureTheory.Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
m : ∀ {α : Type u_2} {β : Type u_1} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
f : ℕ → α × β → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h2f : Monotone f
h3f : ∀ (n : ℕ), (fun f => Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν) (f n)
this✝ : Measurable fun b => ⨆ (i : ℕ), ∫⁻ (y : β), f i (b, y) ∂ν
this : ∀ (x : α), Monotone fun n y => f n (x, y)
⊢ Measurable fun x => ⨆ (n : ℕ), ∫⁻ (a : β), (f n ∘ Prod.mk x) a ∂ν
assumption