awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
inr : ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖ₑ ^ p.toReal ≤ (↑c : ℝ≥0∞)
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_

Premises used: IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
inr : ∃ (c : ℝ≥0), ∀ (x : α), (↑(‖f x‖₊ ^ p.toReal) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)
⊢ ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖ₑ ^ p.toReal ≤ (↑c : ℝ≥0∞)

Tactic:
simp_rw [enorm, ← ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg]

Premises used: ENNReal.coe_rpow_of_nonneg, ENNReal.toReal_nonneg, ENorm.enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
inr : ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c
⊢ ∃ (c : ℝ≥0), ∀ (x : α), (↑(‖f x‖₊ ^ p.toReal) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup F
f : α → F
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c

Tactic:
Finite.exists_le _

Premises used: Finite.exists_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
inst_1 : Finite α
inst_2 : IsFiniteMeasure μ
hp₀ : p ≠ 0
hp : p ≠ ∞
⊢ ∃ (c : ℝ≥0), ∀ (x : α), ‖f x‖₊ ^ p.toReal ≤ c

Tactic:
exact Finite.exists_le _

Premises used: Finite.exists_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
inst_1 : DiscreteMeasurableSpace α
inst_2 : Finite α
inst_3 : IsFiniteMeasure μ
⊢ MemLp f p μ

Tactic:
let ⟨C, hC⟩ := Finite.exists_le (‖f ·‖₊); .of_bound .of_discrete C <| .of_forall hC

Premises used: Finite.exists_le, NNNorm.nnnorm, MeasureTheory.AEStronglyMeasurable.of_discrete, _private.0.MeasureTheory.MemLp.of_discrete.match_1, Filter.Eventually.of_forall, MeasureTheory.MemLp, MeasureTheory.MemLp.of_bound, NNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : IsEmpty α
f : α → ε
p : ℝ≥0∞
⊢ eLpNorm f p μ = 0

Tactic:
simp [Subsingleton.elim f 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : eLpNorm' f q μ = 0
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q

Tactic:
simp only [eLpNorm'_eq_lintegral_enorm, lintegral_eq_zero_iff' (hf.enorm.pow_const q), one_div,
    ENNReal.rpow_eq_zero_iff, inv_pos, inv_neg'', hq0.not_gt, and_false, or_false] at h

Premises used: AEMeasurable.pow_const, ENNReal.rpow_eq_zero_iff, MeasureTheory.lintegral_eq_zero_iff', inv_pos, inv_neg'', LE.le.not_gt, one_div, MeasureTheory.AEStronglyMeasurable.enorm, or_false, and_false, MeasureTheory.eLpNorm'_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
⊢ f =ᶠ[ae μ] 0

Tactic:
h.left.mono fun x hx ↦ ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
refine : ∀ (x : α) (hx : Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖f a‖ₑ ^ q) x) (0 x)), f x = 0 x
⊢ f =ᶠ[ae μ] 0

Tactic:
refine h.left.mono fun x hx ↦ ?_

Premises used: Filter.Eventually.mono, And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
x : α
hx : Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖f a‖ₑ ^ q) x) (0 x)
⊢ f x = 0 ∧ 0 < q

Tactic:
simp only [Pi.ofNat_apply, ENNReal.rpow_eq_zero_iff, enorm_eq_zero, h.2.not_gt, and_false,
    or_false] at hx

Premises used: ENNReal.rpow_eq_zero_iff, Pi.ofNat_apply, And.right, LT.lt.not_gt, or_false, and_false, enorm_eq_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hq0 : 0 ≤ q
hf : AEStronglyMeasurable f μ
h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖f a‖ₑ ^ q) 0 ∧ 0 < q
x : α
hx : f x = 0 ∧ 0 < q
⊢ f x = 0 x

Tactic:
simp [hx.1]

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
q : ℝ
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
hq0_lt : 0 < q
f : α → ε
hf : AEStronglyMeasurable f μ
⊢ eLpNorm' f q μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
⟨ae_eq_zero_of_eLpNorm'_eq_zero (le_of_lt hq0_lt) hf, eLpNorm'_eq_zero_of_ae_zero hq0_lt⟩

Premises used: le_of_lt, MeasureTheory.eLpNorm'_eq_zero_of_ae_zero, Iff.intro, MeasureTheory.ae_eq_zero_of_eLpNorm'_eq_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
ε : Type u_8
inst : ENorm ε
x : MeasurableSpace α
f : α → ε
μ : Measure α
⊢ ∀ᵐ (x_1 : α) ∂μ, ‖f x_1‖ₑ ≤ eLpNormEssSup f μ

Tactic:
ENNReal.ae_le_essSup fun x => ‖f x‖ₑ

Premises used: ENorm.enorm, MeasureTheory.eLpNormEssSup, ENNReal.ae_le_essSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
⊢ eLpNormEssSup f μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
simp [EventuallyEq, eLpNormEssSup_eq_essSup_enorm]

Premises used: Filter.EventuallyEq, 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 ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
pos : ∀ (h_top : p = ∞), eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
neg : ∀ (h_top : ¬p = ∞), eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
by_cases h_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 ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : p = ∞
pos : eLpNorm f ∞ μ = 0 ↔ f =ᶠ[ae μ] 0
pos₁ : eLpNormEssSup f μ = 0 ↔ f =ᶠ[ae μ] 0
pos₂ pos₃ : f =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [h_top, eLpNorm_exponent_top, eLpNormEssSup_eq_zero_iff]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ∞
neg : eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0
⊢ eLpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
rw [eLpNorm_eq_eLpNorm' h0 h_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 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
eLpNorm'_eq_zero_iff (ENNReal.toReal_pos h0 h_top) hf

Premises used: ENNReal.toReal_pos, MeasureTheory.eLpNorm'_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : α → ε
hf : AEStronglyMeasurable f μ
h0 : p ≠ 0
h_top : ¬p = ∞
⊢ eLpNorm' f p.toReal μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
exact eLpNorm'_eq_zero_iff (ENNReal.toReal_pos h0 h_top) hf

Premises used: ENNReal.toReal_pos, MeasureTheory.eLpNorm'_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
essSup_map_measure hg.enorm hf

Premises used: essSup_map_measure, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
pos : ∀ (hp_zero : p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
neg : ∀ (hp_zero : ¬p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp_zero : 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 ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : p = 0
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp only [hp_zero, eLpNorm_exponent_zero]

Premises used: MeasureTheory.eLpNorm_exponent_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
pos : ∀ (hp_top : p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
neg : ∀ (hp_top : ¬p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ 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 ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ∞
pos : eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [hp_top, eLpNorm_exponent_top]

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
eLpNormEssSup_map_measure hg hf

Premises used: MeasureTheory.eLpNormEssSup_map_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : p = ∞
⊢ eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
exact eLpNormEssSup_map_measure hg hf

Premises used: MeasureTheory.eLpNormEssSup_map_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
hp_zero : ¬p = 0
hp_top : ¬p = ∞
neg :
  (∫⁻ (x : β), ‖g x‖ₑ ^ p.toReal ∂Measure.map f μ) ^ (1 / p.toReal) =
    (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
neg₁ :
  (∫⁻ (a : α), ‖g (f a)‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) = (∫⁻ (x : α), ‖(g ∘ f) x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal)
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp_top,
    lintegral_map' (hg.enorm.pow_const p.toReal) hf, Function.comp_apply]

Premises used: AEMeasurable.pow_const, ENNReal.toReal, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, MeasureTheory.AEStronglyMeasurable.enorm, Function.comp_apply, MeasureTheory.lintegral_map'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp (m0 := mβ) g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Tactic:
simp [MemLp, eLpNorm_map_measure hg hf, hg.comp_aemeasurable hf, hg]

Premises used: MeasureTheory.MemLp, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable, MeasureTheory.eLpNorm_map_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hg : MemLp (m0 := mβ) g p (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp (g ∘ f) p μ

Tactic:
(memLp_map_measure_iff hg.aestronglyMeasurable hf).1 hg

Premises used: Iff.mp, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
ν : Measure β
hg : AEStronglyMeasurable g ν
hf : MeasurePreserving f μ ν
⊢ eLpNorm (g ∘ f) p μ = eLpNorm g p ν

Tactic:
Eq.symm <| hf.map_eq ▸ eLpNorm_map_measure (hf.map_eq ▸ hg) hf.aemeasurable

Premises used: MeasureTheory.MeasurePreserving.aemeasurable, Eq.rec, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.eLpNorm_map_measure, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
rw : eLpNorm ((↑g : β → E) ∘ f) p μ = eLpNorm (↑g : β → E) p ν
⊢ eLpNorm (↑(g.compMeasurePreserving f hf) : α → E) p μ = eLpNorm (↑g : β → E) p ν

Tactic:
rw [eLpNorm_congr_ae (g.coeFn_compMeasurePreserving _)]

Premises used: MeasureTheory.AEEqFun.coeFn_compMeasurePreserving, MeasureTheory.eLpNorm_congr_ae
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm ((↑g : β → E) ∘ f) p μ = eLpNorm (↑g : β → E) p ν

Tactic:
eLpNorm_comp_measurePreserving g.aestronglyMeasurable hf

Premises used: MeasureTheory.AEEqFun.aestronglyMeasurable, MeasureTheory.eLpNorm_comp_measurePreserving
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm ((↑g : β → E) ∘ f) p μ = eLpNorm (↑g : β → E) p ν

Tactic:
exact eLpNorm_comp_measurePreserving g.aestronglyMeasurable hf

Premises used: MeasureTheory.AEEqFun.aestronglyMeasurable, MeasureTheory.eLpNorm_comp_measurePreserving
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
ν : Measure β
hg : MemLp g p ν
hf : MeasurePreserving f μ ν
⊢ MemLp (g ∘ f) p μ

Tactic:
.comp_of_map (hf.map_eq.symm ▸ hg) hf.aemeasurable

Premises used: MeasureTheory.MeasurePreserving.aemeasurable, MeasureTheory.MemLp.comp_of_map
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
⊢ eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
hf.essSup_map_measure

Premises used: MeasurableEmbedding.essSup_map_measure, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
pos : ∀ (hp_zero : p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
neg : ∀ (hp_zero : ¬p = 0), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp_zero : 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 ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : p = 0
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp only [hp_zero, eLpNorm_exponent_zero]

Premises used: MeasureTheory.eLpNorm_exponent_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
pos : ∀ (hp : p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
neg : ∀ (hp : ¬p = ∞), @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
by_cases hp : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
pos : eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp_rw [hp, eLpNorm_exponent_top]

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
hf.essSup_map_measure

Premises used: MeasurableEmbedding.essSup_map_measure, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : p = ∞
⊢ eLpNormEssSup (m0 := mβ) g (Measure.map f μ) = eLpNormEssSup (g ∘ f) μ

Tactic:
exact hf.essSup_map_measure

Premises used: MeasurableEmbedding.essSup_map_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
hp_zero : ¬p = 0
hp : ¬p = ∞
⊢ @eLpNorm _ _ _ mβ g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ

Tactic:
simp [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_zero hp, hf.lintegral_map]

Premises used: MeasurableEmbedding.lintegral_map, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
f : α → β
g : β → ε
hf : MeasurableEmbedding f
simp_rw :
  AEStronglyMeasurable (m₀ := mβ) g (Measure.map f μ) ∧ @eLpNorm _ _ _ mβ g p (Measure.map f μ) < ∞ ↔
    AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞
simp_rw₁ :
  AEStronglyMeasurable (g ∘ f) μ ∧ @eLpNorm _ _ _ mβ g p (Measure.map f μ) < ∞ ↔
    AEStronglyMeasurable (g ∘ f) μ ∧ eLpNorm (g ∘ f) p μ < ∞
⊢ MemLp (m0 := mβ) g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ

Tactic:
simp_rw [MemLp, hf.aestronglyMeasurable_map_iff, hf.eLpNorm_map_measure]

Premises used: MeasurableEmbedding.aestronglyMeasurable_map_iff, MeasureTheory.MemLp, MeasurableEmbedding.eLpNorm_map_measure
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
β : Type u_8
mβ : MeasurableSpace β
g : β → ε
f : α ≃ᵐ β
⊢ MemLp (m0 := mβ) g p (Measure.map (⇑f : (a : α) → β) μ) ↔ MemLp (g ∘ (⇑f : (a : α) → β)) p μ

Tactic:
f.measurableEmbedding.memLp_map_measure_iff

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
pos : ∀ (hp0 : p.toReal = 0), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
neg : ∀ (hp0 : ¬p.toReal = 0), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞

Tactic:
by_cases hp0 : p.toReal = 0

Premises used: ENNReal.toReal