case refine'_1
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ ∀ (n : ℕ), Measurable fun a => ⨆ (i : ℕ) (_ : i ≥ n), f i a

case refine'_2
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ Antitone fun n a => ⨆ (i : ℕ) (_ : i ≥ n), f i a

case refine'_3
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ (∫⁻ (a : α), ⨆ (i : ℕ) (_ : i ≥ 0), f i a ∂μ) ≠ ⊤
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ (⨅ (n : ℕ), ∫⁻ (a : α), ⨆ (i : ℕ) (_ : i ≥ n), f i a ∂μ) = ∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), f i a ∂μ
refine' (lintegral_iInf _ _ _).symm
case refine'_1
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
n : ℕ
⊢ Measurable fun a => ⨆ (i : ℕ) (_ : i ≥ n), f i a
case refine'_1
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ ∀ (n : ℕ), Measurable fun a => ⨆ (i : ℕ) (_ : i ≥ n), f i a
intro n
no goals
case refine'_1
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
n : ℕ
⊢ Measurable fun a => ⨆ (i : ℕ) (_ : i ≥ n), f i a
exact measurable_biSup _ (to_countable _) hf_meas
case refine'_2
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
n m : ℕ
hnm : n ≤ m
a : α
⊢ (fun n a => ⨆ (i : ℕ) (_ : i ≥ n), f i a) m a ≤ (fun n a => ⨆ (i : ℕ) (_ : i ≥ n), f i a) n a
case refine'_2
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ Antitone fun n a => ⨆ (i : ℕ) (_ : i ≥ n), f i a
intro n m hnm a
no goals
case refine'_2
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m✝ : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
n m : ℕ
hnm : n ≤ m
a : α
⊢ (fun n a => ⨆ (i : ℕ) (_ : i ≥ n), f i a) m a ≤ (fun n a => ⨆ (i : ℕ) (_ : i ≥ n), f i a) n a
exact iSup_le_iSup_of_subset fun i hi => le_trans hnm hi
case refine'_3
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, (⨆ (i : ℕ) (_ : i ≥ 0), f i a) ≤ g a
case refine'_3
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ (∫⁻ (a : α), ⨆ (i : ℕ) (_ : i ≥ 0), f i a ∂μ) ≠ ⊤
refine' ne_top_of_le_ne_top h_fin (lintegral_mono_ae _)
case refine'_3
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ (⨆ (i : ℕ) (_ : i ≥ 0), f i n) ≤ g n
case refine'_3
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, (⨆ (i : ℕ) (_ : i ≥ 0), f i a) ≤ g a
refine' (ae_all_iff.2 h_bound).mono fun n hn => _
no goals
case refine'_3
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ (⨆ (i : ℕ) (_ : i ≥ 0), f i n) ≤ g n
exact iSup_le fun i => iSup_le fun _ => hn i
no goals
α : Type u_1
β : Type ?u.996569
γ : Type ?u.996572
δ : Type ?u.996575
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : (∫⁻ (a : α), g a ∂μ) ≠ ⊤
⊢ (∫⁻ (a : α), ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), f i a ∂μ) = ∫⁻ (a : α), limsup (fun n => f n a) atTop ∂μ
simp only [limsup_eq_iInf_iSup_of_nat]