awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp' : p ≠ ∞
hs : MeasurableSet s
f g : α → β
c : ℝ
hc : 0 ≤ c
hf : ∀ x ∈ s, dist (f x) (g x) ≤ c
hp : ¬p = 0
this : ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
neg :
  eLpNorm (ε := ℝ) (s.indicator fun (x : α) ↦ c) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₁ :
  ‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₂ :
  ENNReal.ofReal ‖c‖ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₃ :
  ENNReal.ofReal |c| * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg₄ neg₅ :
  ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal) ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
grw [eLpNorm_mono this, eLpNorm_indicator_const hs hp hp', ← ofReal_norm,
    Real.norm_eq_abs, abs_of_nonneg hc]

Premises used: MeasureTheory.eLpNorm_mono, abs_of_nonneg, ofReal_norm, Real.norm_eq_abs, MeasureTheory.eLpNorm_indicator_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
rw : Function.support (f - g) ⊆ s
⊢ s.indicator (f - g) = f - g

Tactic:
rw [Set.indicator_eq_self]

Premises used: Set.indicator_eq_self
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ Function.support (f - g) ⊆ s

Tactic:
(Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)

Premises used: Function.support_sub, HasSubset.Subset.trans, Set.union_subset
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ Function.support (f - g) ⊆ s

Tactic:
exact (Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)

Premises used: Function.support_sub, HasSubset.Subset.trans, Set.union_subset
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
⊢ s.indicator (f - g) = f - g

Tactic:
have hs₃ : s.indicator (f - g) = f - g := by
    rw [Set.indicator_eq_self]
    exact (Function.support_sub _ _).trans (Set.union_subset hs₁ hs₂)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
rw :
  eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
⊢ eLpNorm (f - g) p μ ≤ ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
rw [← hs₃]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
eLpNorm_indicator_sub_le_of_dist_bdd μ hp hs hc (fun x _ ↦ h x)

Premises used: MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
s : Set α
β : Type u_9
inst : NormedAddCommGroup β
μ : Measure α
hp : p ≠ ∞
hs : MeasurableSet s
c : ℝ
hc : 0 ≤ c
f g : α → β
h : ∀ (x : α), dist (f x) (g x) ≤ c
hs₁ : Function.support f ⊆ s
hs₂ : Function.support g ⊆ s
hs₃ : s.indicator (f - g) = f - g
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
exact eLpNorm_indicator_sub_le_of_dist_bdd μ hp hs hc (fun x _ ↦ h x)

Premises used: MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
inl :
  ∀ (hp_top : Ne (α := ℝ≥0∞) 0 ∞) (hf : MemLp f 0 μ),
    ∃ (s : Set α),
      MeasurableSet s ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε
inr :
  ∀ (hp₀ : p ≠ 0),
    ∃ (s : Set α),
      MeasurableSet s ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
rcases eq_or_ne p 0 with rfl | hp₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : Ne (α := ℝ≥0∞) 0 ∞
hf : MemLp f 0 μ
h :
  MeasurableSet.{u_1} (α := α) ∅ ∧
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (Set.indicator ∅ᶜ f) 0 μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) 0 μ < ε

Tactic:
use ∅
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
f : α → β
ε : ℝ≥0∞
hε : ε ≠ 0
hp_top : Ne (α := ℝ≥0∞) 0 ∞
hf : MemLp f 0 μ
⊢ MeasurableSet.{u_1} (α := α) ∅ ∧
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (Set.indicator ∅ᶜ f) 0 μ < ε

Tactic:
simp [pos_iff_ne_zero.2 hε]

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
hf₁ : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞
hε₁ : ε ^ p.toReal ≠ 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal

Tactic:
apply exists_setLIntegral_compl_lt

Premises used: MeasureTheory.exists_setLIntegral_compl_lt
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne

Premises used: And.right, Iff.mp, MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞

Tactic:
exact ((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne

Premises used: And.right, Iff.mp, MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
⊢ ε ^ p.toReal ≠ 0

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε : ε ≠ 0
hp₀ : p ≠ 0
inr :
  ∀ (s : Set α) (hsm : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
    (hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal),
    ∃ (s : Set α),
      MeasurableSet s ∧
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
obtain ⟨s, hsm, hs, hε⟩ :
        ∃ s, MeasurableSet s ∧ μ s < ∞ ∧ ∫⁻ a in sᶜ, (‖f a‖ₑ) ^ p.toReal ∂μ < ε ^ p.toReal := by
      apply exists_setLIntegral_compl_lt
      · exact ((eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp₀ hp_top).1 hf.2).ne
      · simp [*]

Premises used: ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε_1 : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
⟨s, hsm, hs, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε_1 : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
inr : eLpNorm (sᶜ.indicator f) p μ < ε
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
refine ⟨s, hsm, hs, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε_1 : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
inr : 0 < p.toReal
⊢ eLpNorm (sᶜ.indicator f) p μ < ε

Tactic:
rwa [eLpNorm_indicator_eq_eLpNorm_restrict hsm.compl,
      eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp_top, one_div, ENNReal.rpow_inv_lt_iff]

Premises used: MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, MeasurableSet.compl, one_div, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, ENNReal.rpow_inv_lt_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
β : Type u_7
inst : NormedAddCommGroup β
hp_top : p ≠ ∞
f : α → β
hf : MemLp f p μ
ε : ℝ≥0∞
hε_1 : ε ≠ 0
hp₀ : p ≠ 0
s : Set α
hsm : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ∫⁻ (a : α) in sᶜ, ‖f a‖ₑ ^ p.toReal ∂μ < ε ^ p.toReal
⊢ 0 < p.toReal

Tactic:
simp [ENNReal.toReal_pos, *]

Premises used: ENNReal.toReal_pos
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
rw : (eLpNorm f p μ).toReal = if AEStronglyMeasurable f μ then (eLpNorm f p μ).toReal else 0
rw₁ rw₂ : (eLpNorm f p μ).toReal = (eLpNorm f p μ).toReal
⊢ (eLpNorm f p μ).toReal = lpNorm f p μ

Tactic:
rw [lpNorm, if_pos hf]

Premises used: if_pos, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
rw : ENNReal.ofReal (eLpNorm f p μ).toReal = eLpNorm f p μ
rw₁ rw₂ : eLpNorm f p μ = eLpNorm f p μ
⊢ ENNReal.ofReal (lpNorm f p μ) = eLpNorm f p μ

Tactic:
rw [← toReal_eLpNorm hf.aestronglyMeasurable, ENNReal.ofReal_toReal hf.eLpNorm_ne_top]

Premises used: ENNReal.ofReal_toReal, MeasureTheory.toReal_eLpNorm, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : ¬AEStronglyMeasurable f μ
⊢ lpNorm f p μ = 0

Tactic:
if_neg hf

Premises used: if_neg, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf' : ¬MemLp f p μ
⊢ lpNorm f p μ = 0

Tactic:
simp_all [MemLp, lpNorm]

Premises used: MeasureTheory.MemLp, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
⊢ 0 ≤ lpNorm f p μ

Tactic:
simp [lpNorm, apply_ite]

Premises used: apply_ite, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
rw :
  HPow.hPow (α := ℝ) (∫ (a : α), (‖f a‖ₑ ^ p.toReal).toReal ∂μ) (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹
hfm : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ
hf₁ : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ^ p.toReal < ∞
⊢ lpNorm f p μ = HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹

Tactic:
rw [← toReal_eLpNorm hf, eLpNorm_eq_lintegral_rpow_enorm_toReal hp₀ hp, ← ENNReal.toReal_rpow,
    ← integral_toReal]

Premises used: MeasureTheory.toReal_eLpNorm, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, ENNReal.toReal_rpow, MeasureTheory.integral_toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ HPow.hPow (α := ℝ) (∫ (a : α), (‖f a‖ₑ ^ p.toReal).toReal ∂μ) (1 / p.toReal) =
    HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) p.toReal⁻¹

Tactic:
simp [← ENNReal.toReal_rpow]

Premises used: ENNReal.toReal_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
hfm : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal ‖f x‖ ^ p.toReal) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ ^ p.toReal) μ

Tactic:
simp_rw [← ofReal_norm]

Premises used: ofReal_norm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal ‖f x‖ ^ p.toReal) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
x : α
⊢ 0 ≤ p.toReal

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
x : α
⊢ ‖f x‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hp₀ : p ≠ 0
hp : p ≠ ∞
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ^ p.toReal < ∞

Tactic:
exact .of_forall fun x ↦ ENNReal.rpow_lt_top_of_nonneg (by positivity) (by simp)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0
hp : p ≠ 0
hf : AEStronglyMeasurable f μ
⊢ (↑p : ℝ≥0∞) ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0
hp : p ≠ 0
hf : AEStronglyMeasurable f μ
⊢ (↑p : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0
hp : p ≠ 0
hf : AEStronglyMeasurable f μ
rw :
  HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ≥0∞).toReal ∂μ) (↑p : ℝ≥0∞).toReal⁻¹ =
    HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ) ∂μ) (↑p : ℝ)⁻¹
⊢ lpNorm f (↑p : ℝ≥0∞) μ = HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ) ∂μ) (↑p : ℝ)⁻¹

Tactic:
rw [lpNorm_eq_integral_norm_rpow_toReal (by positivity) (by simp) hf]

Premises used: MeasureTheory.lpNorm_eq_integral_norm_rpow_toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
p : ℝ≥0
hp : p ≠ 0
hf : AEStronglyMeasurable f μ
⊢ HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ≥0∞).toReal ∂μ) (↑p : ℝ≥0∞).toReal⁻¹ =
    HPow.hPow (α := ℝ) (∫ (x : α), ‖f x‖ ^ (↑p : ℝ) ∂μ) (↑p : ℝ)⁻¹

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : AEStronglyMeasurable f μ
⊢ lpNorm f 1 μ = ∫ (x : α), ‖f x‖ ∂μ

Tactic:
simp [lpNorm_eq_integral_norm_rpow_toReal one_ne_zero ENNReal.coe_ne_top hf]

Premises used: MeasureTheory.lpNorm_eq_integral_norm_rpow_toReal, one_ne_zero, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
⊢ lpNorm f 0 μ = 0

Tactic:
simp [lpNorm]

Premises used: MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
inst : NormedAddCommGroup E
f : α → E
⊢ lpNorm (m0 := m) f p 0 = 0

Tactic:
simp [lpNorm]

Premises used: MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ lpNorm f ∞ μ

Tactic:
simpa only [← toReal_eLpNorm hf.aestronglyMeasurable, ← ENNReal.ofReal_le_iff_le_toReal hf.2.ne,
    ofReal_norm] using ae_le_eLpNormEssSup

Premises used: ENNReal.ofReal_le_iff_le_toReal, MeasureTheory.toReal_eLpNorm, MeasureTheory.ae_le_eLpNormEssSup, And.right, MeasureTheory.MemLp.aestronglyMeasurable, ofReal_norm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
simp : ENNReal.toReal (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) = essSup (fun (x : α) ↦ ‖f x‖) μ
⊢ lpNorm f ∞ μ = essSup (fun (x : α) ↦ ‖f x‖) μ

Tactic:
simp only [← toReal_eLpNorm hf.aestronglyMeasurable, eLpNorm_exponent_top, eLpNormEssSup]

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.toReal_eLpNorm, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ ∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
refine : ∀ᶠ (x : ℝ) in map (fun (i : α) ↦ ‖f i‖ₑ.toReal) (ae μ), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (lpNorm f ∞ μ)
⊢ ENNReal.toReal (essSup (fun (x : α) ↦ ‖f x‖ₑ) μ) = essSup (fun (x : α) ↦ ‖f x‖) μ

Tactic:
refine ENNReal.toReal_essSup (by simp) ⟨lpNorm f ∞ μ, ?_⟩

Premises used: ENNReal.toReal_essSup, Exists.intro, Top.top, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f ∞ μ
⊢ ∀ᶠ (x : ℝ) in map (fun (i : α) ↦ ‖f i‖ₑ.toReal) (ae μ), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (lpNorm f ∞ μ)

Tactic:
simpa [-toReal_enorm, lpNorm] using ae_le_lpNorm_exponent_top hf

Premises used: toReal_enorm, MeasureTheory.ae_le_lpNorm_exponent_top, MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_2} (E := E) 0 p μ = 0

Tactic:
simp [lpNorm]

Premises used: MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
⊢ lpNorm.{u_1, u_2} (E := E) (fun (x : α) ↦ 0) p μ = 0

Tactic:
simp [lpNorm]

Premises used: MeasureTheory.lpNorm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
hp : p ≠ 0
⊢ lpNorm f p μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
simp [← toReal_eLpNorm hf.aestronglyMeasurable, ENNReal.toReal_eq_zero_iff, hf.eLpNorm_ne_top,
    eLpNorm_eq_zero_iff hf.1 hp]

Premises used: MeasureTheory.eLpNorm_eq_zero_iff, MeasureTheory.toReal_eLpNorm, And.left, MeasureTheory.MemLp.aestronglyMeasurable, ENNReal.toReal_eq_zero_iff, MeasureTheory.MemLp.eLpNorm_ne_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsEmpty α
f : α → E
p : ℝ≥0∞
⊢ lpNorm f p μ = 0

Tactic:
simp [Subsingleton.elim f 0]

Premises used: Subsingleton.elim, OfNat.ofNat