α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ (∫⁻ (a : α), ⨆ (s : Finset β), ∑ i in s, f i a ∂μ) = ⨆ (s : Finset β), ∑ i in s, ∫⁻ (a : α), f i a ∂μ
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ (∫⁻ (a : α), ∑' (i : β), f i a ∂μ) = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
simp only [ENNReal.tsum_eq_iSup_sum]
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i in b, f i a ∂μ) = ⨆ (s : Finset β), ∑ i in s, ∫⁻ (a : α), f i a ∂μ

case hf
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ ∀ (b : Finset β), AEMeasurable fun a => ∑ i in b, f i a

case h_directed
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun s a => ∑ i in s, f i a
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ (∫⁻ (a : α), ⨆ (s : Finset β), ∑ i in s, f i a ∂μ) = ⨆ (s : Finset β), ∑ i in s, ∫⁻ (a : α), f i a ∂μ
rw [lintegral_iSup_directed]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ (⨆ (b : Finset β), ∫⁻ (a : α), ∑ i in b, f i a ∂μ) = ⨆ (s : Finset β), ∑ i in s, ∫⁻ (a : α), f i a ∂μ
simp [lintegral_finset_sum' _ fun i _ => hf i]
case hf
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
b : Finset β
⊢ AEMeasurable fun a => ∑ i in b, f i a
case hf
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ ∀ (b : Finset β), AEMeasurable fun a => ∑ i in b, f i a
intro b
no goals
case hf
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
b : Finset β
⊢ AEMeasurable fun a => ∑ i in b, f i a
exact Finset.aemeasurable_sum _ fun i _ => hf i
case h_directed
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) s) ((fun s a => ∑ i in s, f i a) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) t) ((fun s a => ∑ i in s, f i a) z)
case h_directed
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
⊢ Directed (fun x x_1 => x ≤ x_1) fun s a => ∑ i in s, f i a
intro s t
case h_directed
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) s) ((fun s a => ∑ i in s, f i a) (s ∪ t)) ∧
    (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) t) ((fun s a => ∑ i in s, f i a) (s ∪ t))
case h_directed
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) s) ((fun s a => ∑ i in s, f i a) z) ∧
      (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) t) ((fun s a => ∑ i in s, f i a) z)
use s ∪ t
case h_directed.left
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) s) ((fun s a => ∑ i in s, f i a) (s ∪ t))

case h_directed.right
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) t) ((fun s a => ∑ i in s, f i a) (s ∪ t))
case h_directed
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) s) ((fun s a => ∑ i in s, f i a) (s ∪ t)) ∧
    (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) t) ((fun s a => ∑ i in s, f i a) (s ∪ t))
constructor
no goals
case h_directed.left
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) s) ((fun s a => ∑ i in s, f i a) (s ∪ t))
exact fun a => Finset.sum_le_sum_of_subset (Finset.subset_union_left _ _)
no goals
case h_directed.right
α : Type u_2
β : Type u_1
γ : Type ?u.1015473
δ : Type ?u.1015476
m : MeasurableSpace α
μ ν : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (i : β), AEMeasurable (f i)
s t : Finset β
⊢ (fun x x_1 => x ≤ x_1) ((fun s a => ∑ i in s, f i a) t) ((fun s a => ∑ i in s, f i a) (s ∪ t))
exact fun a => Finset.sum_le_sum_of_subset (Finset.subset_union_right _ _)