awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
⊢ ¬p < 0

Tactic:
have hp' : ¬(p < 0) := by linarith
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
pos : ∀ (hc : c = ∞), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
neg : ∀ (hc : ¬c = ∞), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
by_cases hc : c = ⊤
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
pos : ∀ (hg' : eLpNorm' g p μ = 0), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
neg : ∀ (hg' : ¬eLpNorm' g p μ = 0), eLpNorm' f p μ ≤ c * eLpNorm' g p μ
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
by_cases hg' : eLpNorm' g p μ = 0

Premises used: MeasureTheory.eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
⊢ ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ = 0

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'

Premises used: ENNReal.rpow_eq_zero_iff, and_true, inv_pos, inv_neg'', one_div, or_false, and_false, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ = 0
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ ^ p) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : ∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ = 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ ^ p) 0

Tactic:
rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'

Premises used: MeasureTheory.lintegral_eq_zero_iff'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ ^ p) 0
x : α
hx : Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖g a‖ₑ ^ p) x) (0 x)
⊢ ‖g x‖ₑ = 0

Tactic:
simpa [hp, hp'] using hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖g a‖ₑ ^ p) 0
⊢ ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0

Tactic:
exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0

Tactic:
have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 := by
        simp only [eLpNorm'_eq_lintegral_enorm, one_div, ENNReal.rpow_eq_zero_iff, inv_pos, hp,
          and_true, inv_neg'', hp', and_false, or_false] at hg'
        rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
        exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h_1 : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
x : α
h_2 : ‖g x‖ₑ = 0 ∧ ‖f x‖ₑ ≤ c * ‖g x‖ₑ
h : ‖g x‖ₑ = 0
h' : ‖f x‖ₑ ≤ c * ‖g x‖ₑ
⊢ ‖f x‖ₑ = 0

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0

Tactic:
have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : eLpNorm' g p μ = 0
this_1 : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
simpa only [hg', mul_zero, nonpos_iff_eq_zero] using eLpNorm'_eq_zero_of_ae_eq_zero hp this

Premises used: MeasureTheory.eLpNorm'_eq_zero_of_ae_eq_zero, MulZeroClass.mul_zero, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : c = ∞
hg' : ¬eLpNorm' g p μ = 0
⊢ eLpNorm' f p μ ≤ c * eLpNorm' g p μ

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
⊢ c ^ p ≠ ∞

Tactic:
simp [hp.le, hc]

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
⊢ c ^ p ≠ ∞

Tactic:
have : c ^ p ≠ ⊤ := by simp [hp.le, hc]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
neg : ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p) ≤ c * (∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)

Tactic:
rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.mul_rpow_of_nonneg _ _ hp.le]

Premises used: ENNReal.mul_rpow_of_nonneg, LT.lt.le, ENNReal.rpow_le_rpow_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
neg : ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), c ^ p * ‖g a‖ₑ ^ p ∂μ
⊢ ((∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p ≤ c ^ p * ((∫⁻ (a : α), ‖g a‖ₑ ^ p ∂μ) ^ (1 / p)) ^ p

Tactic:
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one,
    ← lintegral_const_mul' _ _ this]

Premises used: ENNReal.rpow_mul, MeasureTheory.lintegral_const_mul', ENNReal.rpow_one, LT.lt.ne', one_div, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
neg : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ c ^ p * ‖g a‖ₑ ^ p
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ ≤ ∫⁻ (a : α), c ^ p * ‖g a‖ₑ ^ p ∂μ

Tactic:
apply lintegral_mono_ae

Premises used: MeasureTheory.lintegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
x : α
⊢ c ^ p * ‖g x‖ₑ ^ p = (c * ‖g x‖ₑ) ^ p

Tactic:
simp [ENNReal.mul_rpow_eq_ite, hp']

Premises used: ENNReal.mul_rpow_eq_ite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
⊢ ∀ (x : α), c ^ p * ‖g x‖ₑ ^ p = (c * ‖g x‖ₑ) ^ p

Tactic:
have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by
    simp [ENNReal.mul_rpow_eq_ite, hp']
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε' : Type u_6
inst : TopologicalSpace ε'
inst_1 : ContinuousENorm ε'
ε : Type u_7
inst_2 : TopologicalSpace ε
inst_3 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
g : α → ε'
p : ℝ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
hp : 0 < p
hp' : ¬p < 0
hc : ¬c = ∞
this : c ^ p ≠ ∞
aux : ∀ (x : α), c ^ p * ‖g x‖ₑ ^ p = (c * ‖g x‖ₑ) ^ p
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ^ p ≤ c ^ p * ‖g a‖ₑ ^ p

Tactic:
simpa [ENNReal.coe_rpow_of_nonneg _ hp.le, aux, ENNReal.rpow_le_rpow_iff hp]

Premises used: ENNReal.coe_rpow_of_nonneg, LT.lt.le, ENNReal.rpow_le_rpow_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ
⊢ eLpNormEssSup f μ ≤ c • eLpNormEssSup g μ

Tactic:
calc
    essSup (‖f ·‖ₑ) μ ≤ essSup (c * ‖g ·‖ₑ) μ := essSup_mono_ae <| h
    _ = c • essSup (‖g ·‖ₑ) μ := ENNReal.essSup_const_mul

Premises used: Trans.trans, ENNReal.essSup_const_mul, essSup_mono_ae, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
pos : ∀ (h0 : p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
neg : ∀ (h0 : ¬p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : p = 0
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
pos : eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
rw [h_top]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ

Tactic:
eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h

Premises used: Filter.limsSup, MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul', Filter.limsup, MeasureTheory.eLpNormEssSup, essSup, MeasureTheory.eLpNorm, ite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ

Tactic:
exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h

Premises used: MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
neg : eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ

Tactic:
eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul' h (ENNReal.toReal_pos h0 h_top)

Premises used: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : TopologicalSpace ε'
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑c : ℝ≥0∞) * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ

Tactic:
exact eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul' h (ENNReal.toReal_pos h0 h_top)

Premises used: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul', ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
pos : ∀ (h0 : p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
neg : ∀ (h0 : ¬p = 0), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : p = 0
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
simp [h0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ ≤ c • eLpNorm g p μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
by_cases h_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
pos : eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
rw [h_top]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ

Tactic:
eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul h

Premises used: Filter.limsSup, MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul, Filter.limsup, MeasureTheory.eLpNormEssSup, essSup, MeasureTheory.eLpNorm, ite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ

Tactic:
exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul h

Premises used: MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
neg : eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ

Tactic:
eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h (ENNReal.toReal_pos h0 h_top)

Premises used: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup F
inst_1 : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ ≤ c • eLpNorm' g p.toReal μ

Tactic:
exact eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h (ENNReal.toReal_pos h0 h_top)

Premises used: MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul, ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_7
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
mp : a ≤ b * c → a = 0 ∧ c = 0
mpr : a = 0 ∧ c = 0 → a ≤ b * c
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_7
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0

Tactic:
⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
        (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩

Premises used: mul_nonpos_of_nonpos_of_nonneg, LE.le.antisymm, LT.lt.le, nonpos_of_mul_nonneg_right, And.intro, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_7
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0

Tactic:
exact
      ⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
        (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
Goal:
α : Type u_7
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
b : α
hb : b < 0
ha hc mpr mpr₁ : LE.le.{u_7} (α := α) 0 0
⊢ 0 ≤ b * 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero