awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
pos : eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
refine lt_of_le_of_lt (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos) ?_

Premises used: lt_of_le_of_lt, MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞

Tactic:
ENNReal.mul_lt_top hfq_lt_top ?_

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
pos : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞
⊢ eLpNormEssSup f μ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞

Tactic:
refine ENNReal.mul_lt_top hfq_lt_top ?_

Premises used: ENNReal.mul_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ 0 ≤ 1 / p.toReal

Tactic:
simp [hp_pos.le]

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNormEssSup f μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : q = ∞
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (by simp [hp_pos.le]) (by finiteness)

Premises used: ENNReal.rpow_lt_top_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
by_contra : ∀ (hq_eq_zero : q = 0), False
⊢ q ≠ 0

Tactic:
by_contra hq_eq_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hpq : p ≤ 0) (hfq_m : AEStronglyMeasurable f μ) (hfq_lt_top : eLpNorm f q μ < ∞) (hp0 : p ≠ 0) (hp_top : ¬p = ∞)
    (hp_pos : 0 < p.toReal) (hq_top : ¬q = ∞) (hq_eq_zero : q = 0), p ≤ 0
⊢ p ≤ 0

Tactic:
rwa [hq_eq_zero] at hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
⊢ 0 ≤ q

Tactic:
obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le

Premises used: zero_le, le_antisymm, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq₁ : 0 ≤ q
⊢ Ne (α := ℝ≥0∞) 0 0

Tactic:
obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le

Premises used: zero_le, le_antisymm, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq₁ : 0 ≤ q
hp0₁ : Ne (α := ℝ≥0∞) 0 0
⊢ ¬Eq (α := ℝ≥0∞) 0 ∞

Tactic:
obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le

Premises used: zero_le, le_antisymm, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq₁ : 0 ≤ q
hp0₁ : Ne (α := ℝ≥0∞) 0 0
hp_top₁ : ¬Eq (α := ℝ≥0∞) 0 ∞
⊢ 0 < ENNReal.toReal 0

Tactic:
obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le

Premises used: zero_le, le_antisymm, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq : 0 ≤ q
hp0 : Ne (α := ℝ≥0∞) 0 0
hp_top : ¬Eq (α := ℝ≥0∞) 0 ∞
hp_pos : 0 < ENNReal.toReal 0
⊢ LT.lt (α := ℝ) 0 0

Tactic:
rw [ENNReal.toReal_zero] at hp_pos

Premises used: ENNReal.toReal_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq : 0 ≤ q
hp0 : Ne (α := ℝ≥0∞) 0 0
hp_top : ¬Eq (α := ℝ≥0∞) 0 ∞
hp_pos : LT.lt (α := ℝ) 0 0
⊢ False

Tactic:
(lt_irrefl _) hp_pos

Premises used: lt_irrefl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hq_top : ¬q = ∞
hq_eq_zero : q = 0
hpq : 0 ≤ q
hp0 : Ne (α := ℝ≥0∞) 0 0
hp_top : ¬Eq (α := ℝ≥0∞) 0 ∞
hp_pos : LT.lt (α := ℝ) 0 0
⊢ False

Tactic:
exact (lt_irrefl _) hp_pos

Premises used: lt_irrefl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
⊢ q ≠ 0

Tactic:
have hq0 : q ≠ 0 := by
    by_contra hq_eq_zero
    obtain rfl : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) zero_le
    rw [ENNReal.toReal_zero] at hp_pos
    exact (lt_irrefl _) hp_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
⊢ p.toReal ≤ q.toReal

Tactic:
have hpq_real : p.toReal ≤ q.toReal := ENNReal.toReal_mono hq_top hpq
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
neg : eLpNorm' f p.toReal μ < ∞
⊢ eLpNorm f p μ < ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f q.toReal μ < ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
⊢ p ≠ 0

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
hp0₁ : p ≠ 0
⊢ ¬p = ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
hp0₁ : p ≠ 0
hp_top₁ : ¬p = ∞
⊢ 0 < p.toReal

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
hp0₁ : p ≠ 0
hp_top₁ : ¬p = ∞
hp_pos₁ : 0 < p.toReal
⊢ ¬q = ∞

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
hp0₁ : p ≠ 0
hp_top₁ : ¬p = ∞
hp_pos₁ : 0 < p.toReal
hq_top₁ : ¬q = ∞
⊢ q ≠ 0

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm f q μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
hfq_lt_top₁ : eLpNorm' f q.toReal μ < ∞
hp0₁ : p ≠ 0
hp_top₁ : ¬p = ∞
hp_pos₁ : 0 < p.toReal
hq_top₁ : ¬q = ∞
hq0₁ : q ≠ 0
⊢ p.toReal ≤ q.toReal

Tactic:
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q.toReal μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le hfq_m hfq_lt_top hp_pos.le hpq_real

Premises used: MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le, LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p q : ℝ≥0∞
inst_2 : IsFiniteMeasure μ
hpq : p ≤ q
hfq_m : AEStronglyMeasurable f μ
hfq_lt_top : eLpNorm' f q.toReal μ < ∞
hp0 : p ≠ 0
hp_top : ¬p = ∞
hp_pos : 0 < p.toReal
hq_top : ¬q = ∞
hq0 : q ≠ 0
hpq_real : p.toReal ≤ q.toReal
⊢ eLpNorm' f p.toReal μ < ∞

Tactic:
exact eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le hfq_m hfq_lt_top hp_pos.le hpq_real

Premises used: MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le, LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
apply : Function.support f ⊆ toMeasurable μ s
⊢ (toMeasurable μ s).indicator f = f

Tactic:
apply Set.indicator_eq_self.2

Premises used: Iff.mpr, Set.indicator_eq_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
apply : ∀ (x : α) (hx : x ∉ toMeasurable μ s), x ∉ s
⊢ Function.support f ⊆ toMeasurable μ s

Tactic:
apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_

Premises used: Iff.mpr, Function.support_subset_iff'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
x : α
hx : x ∉ toMeasurable μ s
contrapose : ∀ (hx : x ∈ s), x ∈ toMeasurable μ s
⊢ x ∉ s

Tactic:
contrapose hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
x : α
hx : x ∈ s
⊢ x ∈ toMeasurable μ s

Tactic:
subset_toMeasurable μ s hx

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
x : α
hx : x ∈ s
⊢ x ∈ toMeasurable μ s

Tactic:
exact subset_toMeasurable μ s hx

Premises used: MeasureTheory.subset_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
⊢ (toMeasurable μ s).indicator f = f

Tactic:
have : (toMeasurable μ s).indicator f = f := by
    apply Set.indicator_eq_self.2
    apply Function.support_subset_iff'.2 fun x hx ↦ hf x ?_
    contrapose hx
    exact subset_toMeasurable μ s hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
hfq : MemLp f q μ
s : Set α
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
rw :
  ∀ (hfq : MemLp f q (μ.restrict (toMeasurable μ s))) (hf : ∀ x ∉ s, f x = 0)
    (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)) (hpq : p ≤ q)
    (this : (toMeasurable μ s).indicator f = f), MemLp f p (μ.restrict (toMeasurable μ s))
⊢ MemLp f p μ

Tactic:
rw [← this, memLp_indicator_iff_restrict (measurableSet_toMeasurable μ s)] at hfq ⊢

Premises used: MeasureTheory.memLp_indicator_iff_restrict, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa [lt_top_iff_ne_top] using hs

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this : (toMeasurable μ s).indicator f = f
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : Fact (μ (toMeasurable μ s) < ∞) := ⟨by simpa [lt_top_iff_ne_top] using hs⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this_1 : (toMeasurable μ s).indicator f = f
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Tactic:
hfq.mono_exponent hpq

Premises used: MeasureTheory.MemLp.mono_exponent
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
ε' : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε'
inst_1 : ESeminormedAddMonoid ε'
p q : ℝ≥0∞
f : α → ε'
s : Set α
hfq : MemLp f q (μ.restrict (toMeasurable μ s))
hf : ∀ x ∉ s, f x = 0
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hpq : p ≤ q
this_1 : (toMeasurable μ s).indicator f = f
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ MemLp f p (μ.restrict (toMeasurable μ s))

Tactic:
exact hfq.mono_exponent hpq

Premises used: MeasureTheory.MemLp.mono_exponent
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) p μ ≤
    eLpNorm (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) p μ

Tactic:
eLpNorm_mono_ae_real h

Premises used: MeasureTheory.eLpNorm_mono_ae_real
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) p μ ≤ (↑c : ℝ≥0∞) * eLpNorm f ∞ μ * eLpNorm g p μ

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
eLpNorm :
  MeasureTheory.eLpNorm (ε := ℝ) (fun (x : α) ↦ (↑c : ℝ) • ‖f x‖ * ‖g x‖) p μ ≤
    (↑c : ℝ≥0∞) * MeasureTheory.eLpNorm f ∞ μ * MeasureTheory.eLpNorm g p μ
⊢ MeasureTheory.eLpNorm.{u_1, u_4} (ε := G) (fun (x : α) ↦ b (f x) (g x)) p μ ≤
    (↑c : ℝ≥0∞) * MeasureTheory.eLpNorm f ∞ μ * MeasureTheory.eLpNorm g p μ

Tactic:
calc
    eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm (fun x => (c : ℝ) • ‖f x‖ * ‖g x‖) p μ :=
      eLpNorm_mono_ae_real h
    _ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ := ?_

Premises used: Norm.norm, HMul.hMul, MeasureTheory.eLpNorm_mono_ae_real, HSMul.hSMul, Top.top, NNReal.toReal, MeasureTheory.eLpNorm