-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_lt_top_of_finite [Finite α] [IsFiniteMeasure μ] : eLpNorm f p μ < ∞

Proof state:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ eLpNorm f p μ < ⊤

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp]

Result:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

Proof state:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∃ c, ∀ (x : α), ↑(‖f x‖₊ ^ p.toReal) ≤ ↑c

Tactic:
norm_cast

Result:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∃ c, ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c

Proof state:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f 0 μ < ⊤

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∃ c, ∀ (x : α), ‖f x‖ₑ ^ p.toReal ≤ ↑c

Tactic:
simp_rw [enorm, ← ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg]

Result:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∃ c, ∀ (x : α), ↑(‖f x‖₊ ^ p.toReal) ≤ ↑c

Proof state:
case inr.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ⊤ ≠ 0
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => ‖f x‖₊

Tactic:
exact .le_of_finite

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤

Tactic:
refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_

Result:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∃ c, ∀ (x : α), ‖f x‖ₑ ^ p.toReal ≤ ↑c

Proof state:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
⊢ eLpNorm f p μ < ⊤

Tactic:
obtain rfl | hp := eq_or_ne p ∞

Result:
case inr.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ⊤ ≠ 0
⊢ eLpNorm f ⊤ μ < ⊤

case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ eLpNorm f p μ < ⊤

Proof state:
case inr.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ⊤
⊢ ∃ c, ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c

Tactic:
exact Finite.exists_le _

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ⊤ ≠ 0
⊢ eLpNorm f ⊤ μ < ⊤

Tactic:
simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder]

Result:
case inr.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : ⊤ ≠ 0
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => ‖f x‖₊

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f p μ < ⊤

Tactic:
obtain rfl | hp₀ := eq_or_ne p 0

Result:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm f 0 μ < ⊤

case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedAddCommGroup F
f : α → F
inst✝¹ : Finite α
inst✝ : IsFiniteMeasure μ
hp₀ : p ≠ 0
⊢ eLpNorm f p μ < ⊤