α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
⊢ HasFiniteIntegral fun x => ENNReal.toReal (f x)
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ HasFiniteIntegral fun x => ENNReal.toReal (f x)
have :
  ∀ x, (‖(f x).toReal‖₊ : ℝ≥0∞) = ENNReal.some ⟨(f x).toReal, ENNReal.toReal_nonneg⟩ := by
  intro x
  rw [Real.nnnorm_of_nonneg]
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
⊢ (∫⁻ (a : α), ↑{ val := ENNReal.toReal (f a), property := (_ : 0 ≤ ENNReal.toReal (f a)) } ∂μ) < ⊤
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
⊢ HasFiniteIntegral fun x => ENNReal.toReal (f x)
simp_rw [HasFiniteIntegral, this]
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
⊢ (∫⁻ (a : α), ↑{ val := ENNReal.toReal (f a), property := (_ : 0 ≤ ENNReal.toReal (f a)) } ∂μ) < ⊤
refine' lt_of_le_of_lt (lintegral_mono fun x => _) (lt_top_iff_ne_top.2 hf)
case pos
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
hfx : f x = ⊤
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x

case neg
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
hfx : ¬f x = ⊤
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
by_cases hfx : f x = ∞
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
x : α
⊢ ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
⊢ ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
intro x
no goals
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
x : α
⊢ ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
rw [Real.nnnorm_of_nonneg]
no goals
case pos
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
hfx : f x = ⊤
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
simp [hfx]
case neg.intro
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ↑{ val := ENNReal.toReal ↑fx, property := (_ : (fun r => 0 ≤ r) (ENNReal.toReal ↑fx)) } ≤ ↑fx
case neg
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
hfx : ¬f x = ⊤
⊢ ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) } ≤ f x
lift f x to ℝ≥0 using hfx with fx h
case neg.intro
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ { val := ↑fx, property := (_ : (fun r => 0 ≤ r) ↑fx) } ≤ fx
case neg.intro
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ↑{ val := ENNReal.toReal ↑fx, property := (_ : (fun r => 0 ≤ r) (ENNReal.toReal ↑fx)) } ≤ ↑fx
simp [← h]
no goals
case neg.intro
α : Type u_1
β : Type ?u.731151
γ : Type ?u.731154
δ : Type ?u.731157
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → ℝ≥0∞
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
this :
  ∀ (x : α), ↑‖ENNReal.toReal (f x)‖₊ = ↑{ val := ENNReal.toReal (f x), property := (_ : 0 ≤ ENNReal.toReal (f x)) }
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ { val := ↑fx, property := (_ : (fun r => 0 ≤ r) ↑fx) } ≤ fx
rfl