-- Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
theorem meas_ge_le_mul_pow_eLpNorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf : AEStronglyMeasurable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    μ { x | ε ≤ ‖f x‖₊ } ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ⊤
⊢ ε ^ p.toReal * μ {x | ε ≤ ↑‖f x‖₊} ≤ eLpNorm f p μ ^ p.toReal

Tactic:
exact mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top hf ε

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
by_cases h : ε = ∞

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ε = ⊤
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
hεpow : ε ^ p.toReal ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
have hεpow' : ε ^ p.toReal ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg ENNReal.toReal_nonneg h

Result:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ⊤
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
have hεpow : ε ^ p.toReal ≠ 0 := (ENNReal.rpow_pos (pos_iff_ne_zero.2 hε) h).ne.symm

Result:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
hεpow : ε ^ p.toReal ≠ 0
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ⊤
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
rw [ENNReal.inv_rpow, ← ENNReal.mul_le_mul_left hεpow hεpow', ← mul_assoc,
  ENNReal.mul_inv_cancel hεpow hεpow', one_mul]

Result:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ⊤
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ⊤
⊢ ε ^ p.toReal * μ {x | ε ≤ ↑‖f x‖₊} ≤ eLpNorm f p μ ^ p.toReal

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
h : ε = ⊤
⊢ μ {x | ε ≤ ↑‖f x‖₊} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
simp [h]

Result:
no goals