awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (x_1 : ℕ) ↦ ‖f x_1 x‖ₑ) atTop) p.toReal ^ p.toReal⁻¹ < ∞

Tactic:
ENNReal.rpow_lt_top_of_nonneg (inv_nonneg.2 hppos.le) hx.ne

Premises used: Iff.mpr, LT.lt.le, inv_nonneg, ENNReal.rpow_lt_top_of_nonneg, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (x_1 : ℕ) ↦ ‖f x_1 x‖ₑ) atTop) p.toReal ^ p.toReal⁻¹ < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (inv_nonneg.2 hppos.le) hx.ne

Premises used: Iff.mpr, LT.lt.le, inv_nonneg, ENNReal.rpow_lt_top_of_nonneg, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
rcases : ∀ (C : ℝ) (hC : ∀ (x : X), ‖f x‖ ≤ C), MemLp f ∞ μ
⊢ MemLp f ∞ μ

Tactic:
rcases hf.bounded_above_of_compact_support h'f with ⟨C, hC⟩

Premises used: Continuous.bounded_above_of_compact_support
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
apply : AEStronglyMeasurable f μ
⊢ MemLp f ∞ μ

Tactic:
apply memLp_top_of_bound ?_ C (Filter.Eventually.of_forall hC)

Premises used: MeasureTheory.memLp_top_of_bound, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ AEStronglyMeasurable f μ

Tactic:
(hf.stronglyMeasurable_of_hasCompactSupport h'f).aestronglyMeasurable

Premises used: Continuous.stronglyMeasurable_of_hasCompactSupport, MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
X : Type u_7
inst_1 : TopologicalSpace X
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
f : X → E
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
μ : Measure X
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ AEStronglyMeasurable f μ

Tactic:
exact (hf.stronglyMeasurable_of_hasCompactSupport h'f).aestronglyMeasurable

Premises used: Continuous.stronglyMeasurable_of_hasCompactSupport, MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
rw :
  HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    eLpNorm f p μ

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top]

Premises used: MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
h₁ :
  HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤
    ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤
    ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const _) ε

Premises used: AEMeasurable.pow_const, MeasureTheory.mul_meas_ge_le_lintegral₀, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤
    ∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ

Tactic:
exact mul_meas_ge_le_lintegral₀ (hf.enorm.pow_const _) ε

Premises used: AEMeasurable.pow_const, MeasureTheory.mul_meas_ge_le_lintegral₀, MeasureTheory.AEStronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ 1 / p.toReal * p.toReal = 1

Tactic:
one_div_mul_cancel ?_

Premises used: one_div_mul_cancel
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
refine : p.toReal ≠ 0
⊢ 1 / p.toReal * p.toReal = 1

Tactic:
refine one_div_mul_cancel ?_

Premises used: one_div_mul_cancel
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
rw : ¬(p = 0 ∨ p = ∞)
⊢ p.toReal ≠ 0

Tactic:
rw [Ne, ENNReal.toReal_eq_zero_iff]

Premises used: Ne, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ¬(p = 0 ∨ p = ∞)

Tactic:
not_or_intro hp_ne_zero hp_ne_top

Premises used: not_or_intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ¬(p = 0 ∨ p = ∞)

Tactic:
exact not_or_intro hp_ne_zero hp_ne_top

Premises used: not_or_intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ 1 / p.toReal * p.toReal = 1

Tactic:
have : 1 / p.toReal * p.toReal = 1 := by
    refine one_div_mul_cancel ?_
    rw [Ne, ENNReal.toReal_eq_zero_iff]
    exact not_or_intro hp_ne_zero hp_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
rw :
  (HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal)) ^
      p.toReal ≤
    eLpNorm f p μ ^ p.toReal
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal

Tactic:
rw [← ENNReal.rpow_one (ε * μ { x | ε ≤ ‖f x‖ₑ ^ p.toReal }), ← this, ENNReal.rpow_mul]

Premises used: ENNReal.rpow_mul, HMul.hMul, ENNReal.rpow_one, setOf, LE.le, ENorm.enorm, ENNReal.toReal, HPow.hPow, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
h₁ :
  HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    eLpNorm f p μ
⊢ (HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal)) ^
      p.toReal ≤
    eLpNorm f p μ ^ p.toReal

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    eLpNorm f p μ

Tactic:
pow_mul_meas_ge_le_eLpNorm μ hp_ne_zero hp_ne_top hf ε

Premises used: MeasureTheory.pow_mul_meas_ge_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
this : 1 / p.toReal * p.toReal = 1
⊢ HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ^ (1 / p.toReal) ≤
    eLpNorm f p μ

Tactic:
exact pow_mul_meas_ge_le_eLpNorm μ hp_ne_zero hp_ne_top hf ε

Premises used: MeasureTheory.pow_mul_meas_ge_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal} : ℝ≥0∞) ≤
    eLpNorm f p μ ^ p.toReal

Tactic:
mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top hf (ε ^ p.toReal)

Premises used: ENNReal.toReal, HPow.hPow, MeasureTheory.mul_meas_ge_le_pow_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
h : Eq.{u_1 + 1} (α := α → Prop) (fun (x : α) ↦ ε ≤ ‖f x‖ₑ) fun (x : α) ↦ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal

Tactic:
convert! mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top hf (ε ^ p.toReal) using 4

Premises used: ENNReal.toReal, HPow.hPow, MeasureTheory.mul_meas_ge_le_pow_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
h : ∀ (x : α), ε ≤ ‖f x‖ₑ ↔ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal
⊢ Eq.{u_1 + 1} (α := α → Prop) (fun (x : α) ↦ ε ≤ ‖f x‖ₑ) fun (x : α) ↦ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
x : α
h h₁ : ε ≤ ‖f x‖ₑ ↔ ε ≤ ‖f x‖ₑ
⊢ ε ≤ ‖f x‖ₑ ↔ ε ^ p.toReal ≤ ‖f x‖ₑ ^ p.toReal

Tactic:
rw [ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]

Premises used: ENNReal.toReal_pos, ENNReal.rpow_le_rpow_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
pos : ∀ (h : ε = ∞), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
neg : ∀ (h : ¬ε = ∞), (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
by_cases h : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ε = ∞
rw rw₁ : Eq (α := ℝ≥0∞) 0 0
⊢ HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0

Tactic:
rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]

Premises used: ENNReal.zero_rpow_of_pos, ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ε = ∞
⊢ HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0

Tactic:
have : (0 : ℝ≥0∞) ^ p.toReal = 0 := by
      rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ε = ∞
this : HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

Tactic:
simp [h, this, hmeas_top]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
⊢ ε ^ p.toReal ≠ 0

Tactic:
have hεpow : ε ^ p.toReal ≠ 0 := (ENNReal.rpow_pos (pos_iff_ne_zero.2 hε) h).ne.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
⊢ ε ^ p.toReal ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
⊢ ε ^ p.toReal ≠ ∞

Tactic:
have hεpow' : ε ^ p.toReal ≠ ∞ := by finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
neg :
  HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal

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

Premises used: ENNReal.inv_rpow, mul_assoc, ENNReal.mul_inv_cancel, ENNReal.mul_le_mul_iff_right, one_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal

Tactic:
mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top hf ε

Premises used: MeasureTheory.mul_meas_ge_le_pow_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε'
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hmeas_top : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
h : ¬ε = ∞
hεpow : ε ^ p.toReal ≠ 0
hεpow' : ε ^ p.toReal ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) ≤ eLpNorm f p μ ^ p.toReal

Tactic:
exact mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top hf ε

Premises used: MeasureTheory.mul_meas_ge_le_pow_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
apply : ε⁻¹ ^ p.toReal < ∞
apply₁ : eLpNorm f p μ ^ p.toReal < ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f x‖ₑ} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply meas_ge_le_mul_pow_eLpNorm_enorm μ hp_ne_zero hp_ne_top hℒp.aestronglyMeasurable hε hε'
    |>.trans_lt (ENNReal.mul_lt_top ?_ ?_)

Premises used: ENNReal.mul_lt_top, MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm, MeasureTheory.MemLp.aestronglyMeasurable, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ε⁻¹ ^ p.toReal < ∞

Tactic:
simp [hε, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
ε' : Type u_3
m0 : MeasurableSpace α
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
p : ℝ≥0∞
μ : Measure α
f : α → ε'
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm f p μ ^ p.toReal < ∞

Tactic:
simp [hℒp.eLpNorm_lt_top.ne, lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top, MeasureTheory.MemLp.eLpNorm_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
pos : ∀ (h : ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
neg : ∀ (h : ¬ε = ∞), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_cases h : ε = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ε = ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hℒp : MemLp f p μ
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
h : ¬ε = ∞
⊢ ε = ∞ → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ‖f x‖ₑ = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp