case intro
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : β → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun i => ↑(f i)) b
hf : Summable fun i => ↑(f i)
⊢ Summable g
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ Summable g
lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)
case intro.intro
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
f : β → ℝ≥0
hf : Summable fun i => ↑(f i)
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable fun i => ↑(g i)
case intro
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : β → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun i => ↑(f i)) b
hf : Summable fun i => ↑(f i)
⊢ Summable g
lift g to β → ℝ≥0 using hg
case intro.intro
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
f : β → ℝ≥0
hf : Summable fun i => f i
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable fun i => g i
case intro.intro
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
f : β → ℝ≥0
hf : Summable fun i => ↑(f i)
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable fun i => ↑(g i)
rw [NNReal.summable_coe] at hf⊢
no goals
case intro.intro
α : Type ?u.339900
β : Type u_1
γ : Type ?u.339906
f : β → ℝ≥0
hf : Summable fun i => f i
g : β → ℝ≥0
hgf : ∀ (b : β), (fun i => ↑(g i)) b ≤ (fun i => ↑(f i)) b
⊢ Summable fun i => g i
exact NNReal.summable_of_le (fun b => NNReal.coe_le_coe.1 (hgf b)) hf