-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem memLp_of_finite_measure_preimage (p : ℝ≥0∞) {f : α →ₛ E}
    (hf : ∀ y, y ≠ 0 → μ (f ⁻¹' {y}) < ∞) : MemLp f p μ

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
hy0 : y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
simp [hy0, ENNReal.toReal_pos hp0 hp_top]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ AEStronglyMeasurable (⇑f) μ

Tactic:
exact f.aestronglyMeasurable

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ 0 ≤ 1 / p.toReal

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ MemLp (⇑f) p μ

Tactic:
refine ⟨f.aestronglyMeasurable, ?_⟩

Result:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm (⇑f) p μ < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
by_cases hy0 : y = 0

Result:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
hy0 : y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤

case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ MemLp (⇑f) p μ

Tactic:
rw [hp_top]

Result:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ MemLp ⇑f ⊤ μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∑ y ∈ f.range, ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y})) ^ (1 / p.toReal) < ⊤

Tactic:
refine ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top.mpr fun y _ => ?_).ne

Result:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ MemLp ⇑f ⊤ μ

Tactic:
exact memLp_top f μ

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ MemLp (⇑f) p μ

Tactic:
rw [hp0, memLp_zero_iff_aestronglyMeasurable]

Result:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ AEStronglyMeasurable (⇑f) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
⊢ MemLp (⇑f) p μ

Tactic:
by_cases hp0 : p = 0

Result:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : p = 0
⊢ MemLp (⇑f) p μ

case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
⊢ MemLp (⇑f) p μ

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ eLpNorm (⇑f) p μ < ⊤

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]

Result:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ (∑ y ∈ f.range, ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y})) ^ (1 / p.toReal) < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
refine ENNReal.mul_lt_top ?_ (hf y hy0)

Result:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
y : E
x✝ : y ∈ f.range
hy0 : ¬y = 0
⊢ ‖y‖ₑ ^ p.toReal < ⊤

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
⊢ MemLp (⇑f) p μ

Tactic:
by_cases hp_top : p = ∞

Result:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : p = ⊤
⊢ MemLp (⇑f) p μ

case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
f : α →ₛ E
hf : ∀ (y : E), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
hp0 : ¬p = 0
hp_top : ¬p = ⊤
⊢ MemLp (⇑f) p μ