awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
ε' : Type u_8
inst : TopologicalSpace ε
inst_1 : TopologicalSpace ε'
inst_2 : ContinuousENorm ε
inst_3 : ContinuousENorm ε'
f : α → ε
g : α → ε'
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ
⊢ MemLp f p μ ↔ MemLp g p μ

Tactic:
⟨fun h2f => h2f.congr_enorm hg h, fun h2g => h2g.congr_enorm hf <| EventuallyEq.symm h⟩

Premises used: MeasureTheory.MemLp.congr_enorm, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
f : α → E
g : α → F
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f a‖ = ‖g a‖
⊢ MemLp f p μ ↔ MemLp g p μ

Tactic:
⟨fun h2f => h2f.congr_norm hg h, fun h2g => h2g.congr_norm hf <| EventuallyEq.symm h⟩

Premises used: MeasureTheory.MemLp.congr_norm, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑C : ℝ≥0∞)
⊢ eLpNormEssSup f μ < ∞

Tactic:
eLpNormEssSup_lt_top_of_ae_enorm_bound hfC

Premises used: MeasureTheory.eLpNormEssSup_lt_top_of_ae_enorm_bound
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ (↑C : ℝ≥0∞)
⊢ eLpNormEssSup f μ < ∞

Tactic:
exact eLpNormEssSup_lt_top_of_ae_enorm_bound hfC

Premises used: MeasureTheory.eLpNormEssSup_lt_top_of_ae_enorm_bound
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNormEssSup f μ < ∞

Tactic:
eLpNormEssSup_lt_top_of_ae_bound hfC

Premises used: MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNormEssSup f μ < ∞

Tactic:
exact eLpNormEssSup_lt_top_of_ae_bound hfC

Premises used: MeasureTheory.eLpNormEssSup_lt_top_of_ae_bound
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
apply : ∀ (_x : α) (hx : ‖f _x‖ₑ ≤ C), ‖f _x‖ₑ ≤ ‖C‖ₑ
⊢ MemLp f p μ

Tactic:
apply (memLp_const_enorm hC).of_le_enorm (ε' := ℝ≥0∞) hf <| hfC.mono fun _x hx ↦ ?_

Premises used: Filter.Eventually.mono, MeasureTheory.MemLp.of_le_enorm, MeasureTheory.memLp_const_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
_x : α
hx rw : ‖f _x‖ₑ ≤ C
⊢ ‖f _x‖ₑ ≤ ‖C‖ₑ

Tactic:
rw [enorm_eq_self]

Premises used: enorm_eq_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
_x : α
hx : ‖f _x‖ₑ ≤ C
⊢ ‖f _x‖ₑ ≤ C

Tactic:
hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : IsFiniteMeasure μ
f : α → ε
hf : AEStronglyMeasurable f μ
C : ℝ≥0∞
hC : C ≠ ∞
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ C
_x : α
hx : ‖f _x‖ₑ ≤ C
⊢ ‖f _x‖ₑ ≤ C

Tactic:
exact hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
f : α → E
hf : AEStronglyMeasurable f μ
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ MemLp f p μ

Tactic:
(memLp_const C).of_le hf (hfC.mono fun _x hx => le_trans hx (le_abs_self _))

Premises used: le_abs_self, MeasureTheory.MemLp.of_le, Filter.Eventually.mono, le_trans, MeasureTheory.memLp_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
f : α → ℝ
h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b
hX : AEStronglyMeasurable f μ
p : ℝ≥0∞
ha : ∀ᵐ (x : α) ∂μ, a ≤ f x
hb : ∀ᵐ (x : α) ∂μ, f x ≤ b
x : α
⊢ a ≤ f x → f x ≤ b → ‖f x‖ ≤ max |a| |b|

Tactic:
abs_le_max_abs_abs

Premises used: abs_le_max_abs_abs
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
a b : ℝ
f : α → ℝ
h : ∀ᵐ (x : α) ∂μ, f x ∈ Set.Icc a b
hX : AEStronglyMeasurable f μ
p : ℝ≥0∞
ha : ∀ᵐ (x : α) ∂μ, a ≤ f x
hb : ∀ᵐ (x : α) ∂μ, f x ≤ b
h₁ :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ a ≤ f x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ b) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a_4 : α) ↦ ‖f a_4‖ ≤ max |a| |b|) x} x}
            x}
      a_1
h₂ h₃ : ∀ (x : α), a ≤ f x → f x ≤ b → ‖f x‖ ≤ max |a| |b|
⊢ ∀ᵐ (a_1 : α) ∂μ, ‖f a_1‖ ≤ max |a| |b|

Tactic:
filter_upwards [ha, hb] with x using abs_le_max_abs_abs

Premises used: abs_le_max_abs_abs
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hq : 0 ≤ q
h₂ : 0 ≤ 1 / q
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂ν) ^ (1 / q) ≤ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ LE.le (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) ν) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
essSup_mono_measure hμν

Premises used: essSup_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ LE.le (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) ν) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
exact essSup_mono_measure hμν

Premises used: essSup_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
pos : ∀ (hp0 : p = 0), eLpNorm f p ν ≤ eLpNorm f p μ
neg : ∀ (hp0 : ¬p = 0), eLpNorm f p ν ≤ eLpNorm f p μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : p = 0
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp [hp0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p ν ≤ eLpNorm f p μ
neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p ν ≤ eLpNorm f p μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp [hp_top, eLpNormEssSup_mono_measure f (Measure.absolutelyContinuous_of_le hμν)]

Premises used: MeasureTheory.eLpNormEssSup_mono_measure, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg : eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ

Tactic:
eLpNorm'_mono_measure f hμν ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, MeasureTheory.eLpNorm'_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ

Tactic:
exact eLpNorm'_mono_measure f hμν ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, MeasureTheory.eLpNorm'_mono_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hf : MemLp f p μ
⊢ MemLp f p ν

Tactic:
⟨hf.1.mono_measure hμν, (eLpNorm_mono_measure f hμν).trans_lt hf.2⟩

Premises used: MeasureTheory.MemLp, And.right, MeasureTheory.AEStronglyMeasurable.mono_measure, And.left, And.intro, MeasureTheory.eLpNorm_mono_measure, 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 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
pos : ∀ (hp0 : p = 0), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
neg : ∀ (hp0 : ¬p = 0), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : p = 0
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
simp [hp0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p (μ.restrict s) = eLpNorm f p μ
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ∞
pos : Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.restrict s)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
simp only [hp_top, eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_eq_essSup_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ∞
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.restrict s)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx

Premises used: enorm_ne_zero, Iff.mp, ENNReal.essSup_restrict_eq_of_support_subset
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : p = ∞
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (μ.restrict s)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
exact ENNReal.essSup_restrict_eq_of_support_subset fun x hx ↦ hsf <| enorm_ne_zero.1 hx

Premises used: enorm_ne_zero, Iff.mp, ENNReal.essSup_restrict_eq_of_support_subset
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg : (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ eLpNorm f p (μ.restrict s) = eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top, eLpNorm'_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm', MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg : ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
neg : (Function.support (M := ℝ≥0∞) fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s
⊢ ∫⁻ (a : α) in s, ‖f a‖ₑ ^ p.toReal ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ

Tactic:
apply setLIntegral_eq_of_support_subset

Premises used: MeasureTheory.setLIntegral_eq_of_support_subset
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ ¬p.toReal ≤ 0

Tactic:
simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top

Premises used: not_le, ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ ¬p.toReal ≤ 0

Tactic:
have : ¬(p.toReal ≤ 0) := by simpa only [not_le] using ENNReal.toReal_pos hp0 hp_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
s : Set α
f : α → ε
hsf : Function.support f ⊆ s
hp0 : ¬p = 0
hp_top : ¬p = ∞
this : ¬p.toReal ≤ 0
⊢ (Function.support (M := ℝ≥0∞) fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) ⊆ s

Tactic:
simpa [this] using hsf
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
s : Set α
f : α → ε
hf : MemLp f p μ
⊢ MemLp f p (μ.restrict s)

Tactic:
hf.mono_measure Measure.restrict_le_self

Premises used: MeasureTheory.MemLp.mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ
hp : 0 ≤ p
f : α → ε
c : ℝ≥0∞
⊢ eLpNorm' f p (c • μ) = c ^ (1 / p) * eLpNorm' f p μ

Tactic:
simp [eLpNorm', ENNReal.mul_rpow_of_nonneg, hp]

Premises used: ENNReal.mul_rpow_of_nonneg, MeasureTheory.eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
R : Type u_7
inst_1 : Semiring R
inst_2 : IsDomain R
inst_3 : Module R ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → ε
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (c • μ)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
essSup_smul_measure hc _

Premises used: essSup_smul_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
R : Type u_7
inst_1 : Semiring R
inst_2 : IsDomain R
inst_3 : Module R ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
f : α → ε
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (c • μ)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
exact essSup_smul_measure hc _

Premises used: essSup_smul_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (c • μ)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
essSup_ennreal_smul_measure hc _

Premises used: essSup_ennreal_smul_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : ENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖f x‖ₑ) (c • μ)) (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ)

Tactic:
exact essSup_ennreal_smul_measure hc _

Premises used: essSup_ennreal_smul_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
simp_rw : eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp_ne_zero hp_ne_top]

Premises used: MeasureTheory.eLpNorm_eq_eLpNorm'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
rw : c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ
⊢ eLpNorm' f p.toReal (c • μ) = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Tactic:
rw [eLpNorm'_smul_measure ENNReal.toReal_nonneg]

Premises used: MeasureTheory.eLpNorm'_smul_measure, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
e_a : 1 / p.toReal = (1 / p).toReal
⊢ c ^ (1 / p.toReal) * eLpNorm' f p.toReal μ = c ^ (1 / p).toReal • eLpNorm' f p.toReal μ

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
e_a : p.toReal⁻¹ = p⁻¹.toReal
⊢ 1 / p.toReal = (1 / p).toReal

Tactic:
simp_rw [one_div]

Premises used: one_div
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
p : ℝ≥0∞
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
f : α → ε
c : ℝ≥0∞
e_a e_a₁ : p.toReal⁻¹ = p.toReal⁻¹
⊢ p.toReal⁻¹ = p⁻¹.toReal

Tactic:
rw [ENNReal.toReal_inv]

Premises used: ENNReal.toReal_inv
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
pos : ∀ (hp0 : p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
neg : ∀ (hp0 : ¬p = 0), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp0 : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : p = 0
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp [hp0]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
pos : ∀ (hp_top : p = ∞), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
neg : ∀ (hp_top : ¬p = ∞), eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
by_cases hp_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c

Premises used: _private.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0∞
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p (c • μ) = c ^ (1 / p).toReal • eLpNorm f p μ

Tactic:
exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c

Premises used: _private.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
simp : (↑c : ℝ≥0∞) ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
⊢ (↑c : ℝ≥0∞) ^ (1 / p).toReal • eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
c : ℝ≥0
hc : c ≠ 0
f : α → ε
p : ℝ≥0∞
μ : Measure α
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑(c ^ p.toReal⁻¹) : ℝ≥0∞) * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ
⊢ (↑c : ℝ≥0∞) ^ p.toReal⁻¹ * eLpNorm f p μ = c ^ p.toReal⁻¹ • eLpNorm f p μ

Tactic:
norm_cast