-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
protected lemma MemLp.piecewise [DecidablePred (· ∈ s)] {g} (hs : MeasurableSet s)
   (hf : MemLp f p (μ.restrict s)) (hg : MemLp g p (μ.restrict sᶜ)) :
    MemLp (s.piecewise f g) p μ

Proof state:
case neg.inr.left
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖s.piecewise 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

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
a : α
ha : a ∈ sᶜ
⊢ ‖s.piecewise f g a‖ₑ ^ p.toReal = ‖g a‖ₑ ^ p.toReal

Tactic:
have ha' : a ∉ s := ha

Result:
case h
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
a : α
ha : a ∈ sᶜ
ha' : a ∉ s
⊢ ‖s.piecewise f g a‖ₑ ^ p.toReal = ‖g a‖ₑ ^ p.toReal

Proof state:
case neg.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f ⊤ (μ.restrict s)
hg : MemLp g ⊤ (μ.restrict sᶜ)
hp_zero : ¬⊤ = 0
⊢ eLpNorm f ⊤ (μ.restrict s) ⊔ eLpNorm g ⊤ (μ.restrict sᶜ) < ⊤

Tactic:
exact max_lt hf.2 hg.2

Result:
no goals

Proof state:
case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
⊢ eLpNorm (s.piecewise 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]

Result:
case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤ ∧ ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

Proof state:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : p = 0
⊢ MemLp (s.piecewise f g) p μ

Tactic:
simp only [hp_zero, memLp_zero_iff_aestronglyMeasurable]

Result:
case pos
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : p = 0
⊢ AEStronglyMeasurable (s.piecewise f g) μ

Proof state:
case neg.inr.right
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → ‖s.piecewise 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

Result:
no goals

Proof state:
case neg
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
⊢ eLpNorm (s.piecewise f g) p μ < ⊤

Tactic:
obtain rfl | hp_top := eq_or_ne p ∞

Result:
case neg.inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f ⊤ (μ.restrict s)
hg : MemLp g ⊤ (μ.restrict sᶜ)
hp_zero : ¬⊤ = 0
⊢ eLpNorm (s.piecewise f g) ⊤ μ < ⊤

case neg.inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
⊢ eLpNorm (s.piecewise f g) p μ < ⊤

Proof state:
case neg.inr.right
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

Tactic:
rw [setLIntegral_congr_fun hs.compl h]

Result:
case neg.inr.right
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖g x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in sᶜ, ‖g x‖ₑ ^ p.toReal ∂μ < ⊤

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal

Tactic:
filter_upwards with a ha using by simp [ha]

Result:
no goals

Proof state:
case neg.inr.left
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

Tactic:
have h : ∀ᵐ x ∂μ, x ∈ s → ‖Set.piecewise s f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal := by
  filter_upwards with a ha using by simp [ha]

Result:
case neg.inr.left
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup F
f : α → F
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
g : α → F
hs : MeasurableSet s
hf : MemLp f p (μ.restrict s)
hg : MemLp g p (μ.restrict sᶜ)
hp_zero : ¬p = 0
hp_top : p ≠ ⊤
h : ∀ᵐ (x : α) ∂μ, x ∈ s → ‖s.piecewise f g x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ p.toReal
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤