-- 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:
α : 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ᶜ)
⊢ MemLp (s.piecewise f g) p μ

Tactic:
by_cases hp_zero : p = 0

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
⊢ MemLp (s.piecewise f g) p μ

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
⊢ MemLp (s.piecewise f g) p μ

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 ≠ ⊤
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤ ∧ ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

Tactic:
constructor

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 ≠ ⊤
⊢ ∫⁻ (x : α) in s, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

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 ≠ ⊤
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

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
⊢ MemLp (s.piecewise f g) p μ

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

Result:
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 μ < ⊤

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, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

Tactic:
rw [setLIntegral_congr_fun hs h]

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, ‖f x‖ₑ ^ 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 (s.piecewise f g) ⊤ μ < ⊤

Tactic:
rw [eLpNorm_top_piecewise f g hs]

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 f ⊤ (μ.restrict s) ⊔ eLpNorm g ⊤ (μ.restrict sᶜ) < ⊤

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 = ‖g x‖ₑ ^ p.toReal

Tactic:
filter_upwards with a 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ᶜ
⊢ ‖s.piecewise f g a‖ₑ ^ p.toReal = ‖g a‖ₑ ^ p.toReal

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ᶜ
ha' : a ∉ s
⊢ ‖s.piecewise f g a‖ₑ ^ p.toReal = ‖g a‖ₑ ^ p.toReal

Tactic:
simp [ha']

Result:
no goals

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 ≠ ⊤
⊢ ∫⁻ (x : α) in sᶜ, ‖s.piecewise f g x‖ₑ ^ p.toReal ∂μ < ⊤

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

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ᶜ, ‖s.piecewise f 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 ≠ ⊤
a : α
ha : a ∈ s
⊢ ‖s.piecewise f g a‖ₑ ^ p.toReal = ‖f a‖ₑ ^ p.toReal

Tactic:
simp [ha]

Result:
no goals

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
⊢ AEStronglyMeasurable (s.piecewise f g) μ

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

Result:
no goals