awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
p : ℝ≥0∞
hs : MeasurableSet s
c : E
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ MemLp.{u_1, u_4} (ε := E) (fun (x : α) ↦ c) p (μ.restrict s)

Tactic:
apply memLp_const

Premises used: MeasureTheory.memLp_const
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
simp :
  Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ) μ)
    (essSup (s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖g x‖ₑ) μ)
⊢ eLpNormEssSup (s.piecewise (β := fun (a : α) ↦ ε) f g) μ =
    max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))

Tactic:
simp only [eLpNormEssSup, ← ENNReal.essSup_piecewise hs]

Premises used: ENNReal.essSup_piecewise, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
e_f :
  ∀ (x : α),
    ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
      s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
⊢ Eq (α := ℝ≥0∞) (essSup (fun (x : α) ↦ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ) μ)
    (essSup (s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) fun (x : α) ↦ ‖g x‖ₑ) μ)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
x : α
pos :
  ∀ (hx : x ∈ s),
    ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
      s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
neg :
  ∀ (hx : x ∉ s),
    ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
      s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x
⊢ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
x : α
hx : x ∈ s
⊢ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
x : α
hx : x ∉ s
⊢ ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ =
    s.piecewise (β := fun (a : α) ↦ ℝ≥0∞) (fun (x : α) ↦ ‖f x‖ₑ) (fun (x : α) ↦ ‖g x‖ₑ) x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f g : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) ∞ μ = max (eLpNorm f ∞ (μ.restrict s)) (eLpNorm g ∞ (μ.restrict sᶜ))

Tactic:
eLpNormEssSup_piecewise f g hs

Premises used: Filter.limsSup, MeasureTheory.eLpNormEssSup_piecewise, Filter.limsup, MeasureTheory.eLpNormEssSup, essSup, MeasureTheory.eLpNorm, ite
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
pos : ∀ (hp_zero : p = 0), MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
neg : ∀ (hp_zero : ¬p = 0), MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ

Tactic:
by_cases hp_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : p = 0
pos : AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ ε) f g) μ
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ

Tactic:
simp only [hp_zero, memLp_zero_iff_aestronglyMeasurable]

Premises used: MeasureTheory.memLp_zero_iff_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : p = 0
⊢ AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ ε) f g) μ

Tactic:
AEStronglyMeasurable.piecewise hs hf.1 hg.1

Premises used: MeasureTheory.AEStronglyMeasurable.piecewise, And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : p = 0
⊢ AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ ε) f g) μ

Tactic:
exact AEStronglyMeasurable.piecewise hs hf.1 hg.1

Premises used: MeasureTheory.AEStronglyMeasurable.piecewise, And.left
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ

Tactic:
⟨AEStronglyMeasurable.piecewise hs hf.1 hg.1, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.piecewise, MeasureTheory.MemLp, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
neg : eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
⊢ MemLp (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ

Tactic:
refine ⟨AEStronglyMeasurable.piecewise hs hf.1 hg.1, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
neg :
  ∀ (hf : MemLp f ∞ (μ.restrict s)) (hg : MemLp g ∞ (μ.restrict sᶜ)) (hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0),
    eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) ∞ μ < ∞
neg₁ : ∀ (hp_top : p ≠ ∞), eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞

Tactic:
obtain rfl | hp_top := eq_or_ne p ∞

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f ∞ (μ.restrict s)
hg : MemLp g ∞ (μ.restrict sᶜ)
hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0
neg : max (eLpNorm f ∞ (μ.restrict s)) (eLpNorm g ∞ (μ.restrict sᶜ)) < ∞
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) ∞ μ < ∞

Tactic:
rw [eLpNorm_top_piecewise f g hs]

Premises used: MeasureTheory.eLpNorm_top_piecewise
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f ∞ (μ.restrict s)
hg : MemLp g ∞ (μ.restrict sᶜ)
hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0
⊢ max (eLpNorm f ∞ (μ.restrict s)) (eLpNorm g ∞ (μ.restrict sᶜ)) < ∞

Tactic:
max_lt hf.2 hg.2

Premises used: max_lt, And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f ∞ (μ.restrict s)
hg : MemLp g ∞ (μ.restrict sᶜ)
hp_zero : ¬Eq (α := ℝ≥0∞) ∞ 0
⊢ max (eLpNorm f ∞ (μ.restrict s)) (eLpNorm g ∞ (μ.restrict sᶜ)) < ∞

Tactic:
exact max_lt hf.2 hg.2

Premises used: max_lt, And.right
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
neg :
  ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞ ∧
    ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
⊢ eLpNorm (s.piecewise (β := fun (a : α) ↦ ε) f g) p μ < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp_zero hp_top, ← lintegral_add_compl _ hs,
    ENNReal.add_lt_top]

Premises used: MeasureTheory.lintegral_add_compl, ENNReal.add_lt_top, MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
neg : ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
neg₁ : ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞
⊢ ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞ ∧
    ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
x : α
hx : x ∈ s
⊢ ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∀ (x : α) (hx : x ∈ s), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal

Tactic:
have h (x) (hx : x ∈ s) : ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal := by
      simp [hx]
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ s), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
neg : ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ < ∞
⊢ ∫⁻ (x : α) in s, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
rw [setLIntegral_congr_fun hs h]

Premises used: MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ s), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hf.2

Premises used: And.right, MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ s), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in s, ‖f x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
exact lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hf.2

Premises used: And.right, MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
x : α
hx : x ∈ sᶜ
⊢ x ∉ s

Tactic:
have hx' : x ∉ s := hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
x : α
hx : x ∈ sᶜ
hx' : x ∉ s
⊢ ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal

Tactic:
simp [hx']
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
⊢ ∀ (x : α) (hx : x ∈ sᶜ), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal

Tactic:
have h (x) (hx : x ∈ sᶜ) : ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal := by
      have hx' : x ∉ s := hx
      simp [hx']
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ sᶜ), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
neg : ∫⁻ (x : α) in sᶜ, ‖g x‖ₑ ^ p.toReal ∂μ < ∞
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise (β := fun (a : α) ↦ ε) f g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
rw [setLIntegral_congr_fun hs.compl h]

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ sᶜ), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hg.2

Premises used: And.right, MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
Goal:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
g : α → ε
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ∞
h : ∀ (x : α) (hx : x ∈ sᶜ), ‖s.piecewise (β := fun (i : α) ↦ ε) f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖g x‖ₑ ^ p.toReal ∂μ < ∞

Tactic:
exact lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_zero hp_top hg.2

Premises used: And.right, MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top
-- 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
pos :
  ∀ (hp : p = 0),
    eLpNorm (s.indicator (f - g)) p μ ≤
      ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
neg :
  ∀ (hp : ¬p = 0),
    eLpNorm (s.indicator (f - g)) p μ ≤
      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:
by_cases hp : p = 0
-- 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
⊢ eLpNorm (s.indicator (f - g)) p μ ≤
    ENNReal.ofReal c * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)

Tactic:
simp [hp]
-- 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
x : α
pos : ∀ (hx : x ∈ s), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
neg : ∀ (hx : x ∉ s), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)
⊢ ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)

Tactic:
by_cases hx : x ∈ s
-- 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
x : α
hx : x ∈ s
pos : dist (f x) (g x) ≤ c
⊢ ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)

Tactic:
rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
        Real.norm_eq_abs, abs_of_nonneg hc]

Premises used: dist_eq_norm, Set.indicator_of_mem, abs_of_nonneg, Real.norm_eq_abs, Pi.sub_apply
-- 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
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ c

Tactic:
hf x hx
-- 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
x : α
hx : x ∈ s
⊢ dist (f x) (g x) ≤ c

Tactic:
exact hf x hx
-- 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
x : α
hx : x ∉ s
⊢ ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)

Tactic:
simp [Set.indicator_of_notMem hx]

Premises used: Set.indicator_of_notMem
-- 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
⊢ ∀ (x : α), ‖s.indicator (f - g) x‖ ≤ norm (E := ℝ) (s.indicator (fun (x : α) ↦ c) x)

Tactic:
have : ∀ x, ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun _ => c) x‖ := by
    intro x
    by_cases hx : x ∈ s
    · rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm,
        Real.norm_eq_abs, abs_of_nonneg hc]
      exact hf x hx
    · simp [Set.indicator_of_notMem hx]