awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε'' : Type u_8
inst : TopologicalSpace ε''
inst_1 : ESeminormedAddMonoid ε''
p : ℝ≥0∞
c : ε''
hc : ‖c‖ₑ ≠ ∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ MemLp.{u_1, u_8} (ε := ε'') (fun (x : α) ↦ c) p μ ↔
    ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp_all [MemLp, aestronglyMeasurable_const,
    eLpNorm_const_lt_top_iff_enorm hc hp_ne_zero hp_ne_top]

Premises used: MeasureTheory.aestronglyMeasurable_const, MeasureTheory.eLpNorm_const_lt_top_iff_enorm, MeasureTheory.MemLp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
rw :
  ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p μ ↔
    c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [memLp_const_iff_enorm enorm_ne_top hp_ne_zero hp_ne_top]

Premises used: MeasureTheory.memLp_const_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
⊢ ‖c‖ₑ = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    c = 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h₁ : ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q) ≤ (∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr ?_ ^ (1 / q)

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ

Tactic:
lintegral_mono_ae (h.mono fun x hx => ?_)

Premises used: MeasureTheory.lintegral_mono_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h₁ : ∀ (x : α) (hx : ‖f x‖ₑ ≤ ‖g x‖ₑ), ‖f x‖ₑ ^ q ≤ ‖g x‖ₑ ^ q
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ ≤ ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ

Tactic:
refine lintegral_mono_ae (h.mono fun x hx => ?_)

Premises used: MeasureTheory.lintegral_mono_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
x : α
hx : ‖f x‖ₑ ≤ ‖g x‖ₑ
h₁ : 0 ≤ q
⊢ ‖f x‖ₑ ^ q ≤ ‖g x‖ₑ ^ q

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ eLpNorm' f q μ ≤ eLpNorm' g q μ

Tactic:
eLpNorm'_mono_enorm_ae hq <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx

Premises used: Iff.mpr, MeasureTheory.eLpNorm'_mono_enorm_ae, ENNReal.coe_le_coe, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
hq : 0 ≤ q
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ

Tactic:
simpa only [enorm_le_iff_norm_le] using h

Premises used: enorm_le_iff_norm_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
x : α
hx : ‖f x‖ₑ = ‖g x‖ₑ
⊢ Eq (α := ℝ≥0∞) ((fun (x : α) ↦ ‖f x‖ₑ ^ q) x) ((fun (x : α) ↦ ‖g x‖ₑ ^ q) x)

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) fun (x : α) ↦ ‖g x‖ₑ ^ q

Tactic:
have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = ‖g x‖ₑ
this : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) fun (x : α) ↦ ‖g x‖ₑ ^ q
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm, lintegral_congr_ae this]

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
x : α
hx : ‖f x‖₊ = ‖g x‖₊
⊢ Eq (α := ℝ≥0∞) ((fun (x : α) ↦ ‖f x‖ₑ ^ q) x) ((fun (x : α) ↦ ‖g x‖ₑ ^ q) x)

Tactic:
simp [enorm, hx]

Premises used: ENorm.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) fun (x : α) ↦ ‖g x‖ₑ ^ q

Tactic:
have : (‖f ·‖ₑ ^ q) =ᵐ[μ] (‖g ·‖ₑ ^ q) := hfg.mono fun x hx ↦ by simp [enorm, hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊
this : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ q) fun (x : α) ↦ ‖g x‖ₑ ^ q
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm, lintegral_congr_ae this]

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ = ‖g x‖
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
eLpNorm'_congr_nnnorm_ae <| hfg.mono fun _x hx => NNReal.eq hx

Premises used: NNReal.eq, MeasureTheory.eLpNorm'_congr_nnnorm_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : f =ᶠ[ae μ] g
⊢ eLpNorm' f q μ = eLpNorm' g q μ

Tactic:
eLpNorm'_congr_enorm_ae (hfg.fun_comp _)

Premises used: MeasureTheory.eLpNorm'_congr_enorm_ae, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : f =ᶠ[ae μ] g
⊢ eLpNormEssSup f μ = eLpNormEssSup g μ

Tactic:
essSup_congr_ae (hfg.fun_comp enorm)

Premises used: ENorm.enorm, MeasureTheory.eLpNormEssSup, essSup_congr_ae, Filter.EventuallyEq.fun_comp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f g : α → ε
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

Tactic:
essSup_mono_ae <| hfg

Premises used: essSup_mono_ae, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f g : α → F
hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

Tactic:
essSup_mono_ae <| hfg.mono fun _x hx => ENNReal.coe_le_coe.mpr hx

Premises used: Iff.mpr, ENNReal.coe_le_coe, Filter.Eventually.mono, essSup_mono_ae, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
pos : p = 0 → LE.le (α := ℝ≥0∞) 0 0
pos₁ : ¬p = 0 → p = ∞ → eLpNormEssSup f μ ≤ eLpNormEssSup g μ
neg : ¬p = 0 → ¬p = ∞ → eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ
⊢ (if p = 0 then 0 else if p = ∞ then eLpNormEssSup f μ else eLpNorm' f p.toReal μ) ≤
    if p = 0 then 0 else if p = ∞ then eLpNormEssSup g μ else eLpNorm' g p.toReal μ

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h_1 : p = 0
⊢ LE.le (α := ℝ≥0∞) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h_1 : p = 0
⊢ LE.le (α := ℝ≥0∞) 0 0

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h_1 : ¬p = 0
h_2 : p = ∞
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

Tactic:
essSup_mono_ae h

Premises used: essSup_mono_ae, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h_1 : ¬p = 0
h_2 : p = ∞
⊢ eLpNormEssSup f μ ≤ eLpNormEssSup g μ

Tactic:
exact essSup_mono_ae h

Premises used: essSup_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h_1 : ¬p = 0
h_2 : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ

Tactic:
eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h

Premises used: MeasureTheory.eLpNorm'_mono_enorm_ae, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
h_1 : ¬p = 0
h_2 : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ eLpNorm' g p.toReal μ

Tactic:
exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h

Premises used: MeasureTheory.eLpNorm'_mono_enorm_ae, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
eLpNorm_mono_enorm_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx

Premises used: Iff.mpr, ENNReal.coe_le_coe, Filter.Eventually.mono, MeasureTheory.eLpNorm_mono_enorm_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ

Tactic:
simpa only [enorm_le_iff_norm_le] using h

Premises used: enorm_le_iff_norm_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
ε' : Type u_7
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ

Tactic:
simpa only [enorm_le_iff_norm_le] using h

Premises used: enorm_le_iff_norm_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
g : α → ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
eLpNorm_mono_ae <| h.mono fun _x hx =>
    hx.trans ((le_abs_self _).trans (Real.norm_eq_abs _).symm.le)

Premises used: le_abs_self, MeasureTheory.eLpNorm_mono_ae, Eq.le, Filter.Eventually.mono, LE.le.trans, Eq.symm, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
ε' : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : ENorm ε
inst_1 : ENorm ε'
f : α → ε
g : α → ε'
h : ∀ (x : α), ‖f x‖ₑ ≤ ‖g x‖ₑ
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
eLpNorm_mono_enorm_ae (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, MeasureTheory.eLpNorm_mono_enorm_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ (x : α), ‖f x‖₊ ≤ ‖g x‖₊
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
eLpNorm_mono_nnnorm_ae (Eventually.of_forall h)

Premises used: MeasureTheory.eLpNorm_mono_nnnorm_ae, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
G : Type u_6
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
h : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
eLpNorm_mono_ae (Eventually.of_forall h)

Premises used: MeasureTheory.eLpNorm_mono_ae, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
g : α → ℝ
h : ∀ (x : α), ‖f x‖ ≤ g x
⊢ eLpNorm f p μ ≤ eLpNorm g p μ

Tactic:
eLpNorm_mono_ae_real (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, MeasureTheory.eLpNorm_mono_ae_real
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
⊢ eLpNormEssSup f μ ≤ C

Tactic:
essSup_le_of_ae_le C hfC

Premises used: essSup_le_of_ae_le, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ eLpNormEssSup f μ ≤ (↑C : ℝ≥0∞)

Tactic:
essSup_le_of_ae_le (C : ℝ≥0∞) <| hfC.mono fun _x hx => ENNReal.coe_le_coe.mpr hx

Premises used: Iff.mpr, essSup_le_of_ae_le, ENNReal.ofNNReal, ENNReal.coe_le_coe, Filter.Eventually.mono, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNormEssSup f μ ≤ ENNReal.ofReal C

Tactic:
eLpNormEssSup_le_of_ae_nnnorm_bound <| hfC.mono fun _x hx => hx.trans C.le_coe_toNNReal

Premises used: ENNReal.ofReal, Filter.Eventually.mono, LE.le.trans, MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound, Real.le_coe_toNNReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
f : α → ε
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑C : ℝ≥0∞)
⊢ eLpNormEssSup f μ < ∞

Tactic:
(eLpNormEssSup_le_of_ae_enorm_bound hfC).trans_lt ENNReal.coe_lt_top

Premises used: MeasureTheory.eLpNormEssSup_le_of_ae_enorm_bound, LE.le.trans_lt, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ eLpNormEssSup f μ < ∞

Tactic:
(eLpNormEssSup_le_of_ae_nnnorm_bound hfC).trans_lt ENNReal.coe_lt_top

Premises used: LE.le.trans_lt, MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNormEssSup f μ < ∞

Tactic:
(eLpNormEssSup_le_of_ae_bound hfC).trans_lt ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top, MeasureTheory.eLpNormEssSup_le_of_ae_bound, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
inl :
  ∀ (hfC : ∀ᵐ (x : α) ∂0, ‖f x‖ₑ ≤ C),
    @eLpNorm _ _ _ m0 f p 0 ≤
      C • HPow.hPow (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
inr : ∀ (hμ : NeZero μ), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂0, ‖f x‖ₑ ≤ C
⊢ @eLpNorm _ _ _ m0 f p 0 ≤
    C • HPow.hPow (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
pos : ∀ (hp : p = 0), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg : ∀ (hp : ¬p = 0), eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : p = 0
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
simp [hp]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ

Tactic:
have : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ := hfC.mono fun x hx ↦ hx.trans (le_refl C)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
(eLpNorm_mono_enorm_ae this).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.eLpNorm_mono_enorm_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
neg :
  eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
refine (eLpNorm_mono_enorm_ae this).trans_eq ?_

Premises used: LE.le.trans_eq, MeasureTheory.eLpNorm_mono_enorm_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
C : ℝ≥0∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
hμ : NeZero μ
hp : ¬p = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ
neg :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal) =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg₁ :
  ‖C‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg₂ :
  C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
neg₃ neg₄ :
  C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ =
    C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm (ε := ℝ≥0∞) (fun (x : α) ↦ C) p μ =
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]

Premises used: one_div, MeasureTheory.eLpNorm_const, enorm_eq_self, smul_eq_mul, NeZero.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
x : α
hx : ‖f x‖₊ ≤ C
⊢ ‖f x‖ₑ ≤ (↑C : ℝ≥0∞)

Tactic:
simpa using hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C
⊢ eLpNorm f p μ ≤ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using
    (eLpNorm_le_of_ae_enorm_bound (f := f) (C := (C : ℝ≥0∞))
      (hfC.mono fun _ hx => by simpa using hx))

Premises used: ENNReal.smul_def, NNReal.enorm_eq, MeasureTheory.eLpNorm_le_of_ae_enorm_bound, Filter.Eventually.mono, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
rw : eLpNorm f p μ ≤ ENNReal.ofReal C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹
⊢ eLpNorm f p μ ≤ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal C

Tactic:
rw [← mul_comm]

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ ENNReal.ofReal C * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) p.toReal⁻¹

Tactic:
eLpNorm_le_of_ae_nnnorm_bound (hfC.mono fun x hx => hx.trans C.le_coe_toNNReal)

Premises used: MeasureTheory.eLpNorm_le_of_ae_nnnorm_bound, ENNReal.ofReal, Filter.Eventually.mono, LE.le.trans, Real.le_coe_toNNReal