-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_const (c : E) [IsFiniteMeasure μ] : MemLp (fun _ : α => c) p μ

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤

Tactic:
refine ENNReal.mul_lt_top ENNReal.coe_lt_top ?_

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ μ Set.univ ^ (1 / p.toReal) < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ 0 ≤ 1 / p.toReal

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm (fun x => c) p μ < ⊤

Tactic:
by_cases h0 : p = 0

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : p = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

Tactic:
rw [eLpNorm_const c h0 hμ]

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ ‖c‖ₑ * μ Set.univ ^ (1 / p.toReal) < ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
⊢ MemLp (fun x => c) p μ

Tactic:
refine ⟨aestronglyMeasurable_const, ?_⟩

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
⊢ eLpNorm (fun x => c) p μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

Tactic:
by_cases hμ : μ = 0

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : p = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

Tactic:
simp [h0]

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ μ Set.univ ^ (1 / p.toReal) < ⊤

Tactic:
refine ENNReal.rpow_lt_top_of_nonneg ?_ (measure_ne_top μ Set.univ)

Result:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : ¬μ = 0
⊢ 0 ≤ 1 / p.toReal

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
c : E
inst✝ : IsFiniteMeasure μ
h0 : ¬p = 0
hμ : μ = 0
⊢ eLpNorm (fun x => c) p μ < ⊤

Tactic:
simp [hμ]

Result:
no goals