α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ↑(toSimpleFunc (posPart f)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f))
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ↑(toSimpleFunc (posPart f)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f))
have eq : ∀ a, (toSimpleFunc f).posPart a = max ((toSimpleFunc f) a) 0 := fun a => rfl
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ↑(toSimpleFunc (posPart f)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f))
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ↑(toSimpleFunc (posPart f)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f))
have ae_eq : ∀ᵐ a ∂μ, toSimpleFunc (posPart f) a = max ((toSimpleFunc f) a) 0 := by
  filter_upwards [toSimpleFunc_eq_toFun (posPart f), Lp.coeFn_posPart (f : α →₁[μ] ℝ),
    toSimpleFunc_eq_toFun f]with _ _ h₂ h₃
  convert h₂ using 1
  rw [h₃]
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
a : α
h : ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ↑(toSimpleFunc (posPart f)) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ↑(toSimpleFunc (posPart f)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f))
refine' ae_eq.mono fun a h => _
no goals
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
ae_eq : ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
a : α
h : ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ↑(toSimpleFunc (posPart f)) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a
rw [h, eq]
case h
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
a✝¹ : α
a✝ : ↑(toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : ↑(toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ ↑(toSimpleFunc (posPart f)) a✝¹ = max (↑(toSimpleFunc f) a✝¹) 0
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
⊢ ∀ᵐ (a : α) ∂μ, ↑(toSimpleFunc (posPart f)) a = max (↑(toSimpleFunc f) a) 0
filter_upwards [toSimpleFunc_eq_toFun (posPart f), Lp.coeFn_posPart (f : α →₁[μ] ℝ),
  toSimpleFunc_eq_toFun f]with _ _ h₂ h₃
case h.e'_3
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
a✝¹ : α
a✝ : ↑(toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : ↑(toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ max (↑(toSimpleFunc f) a✝¹) 0 = max (↑↑↑f a✝¹) 0
case h
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
a✝¹ : α
a✝ : ↑(toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : ↑(toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ ↑(toSimpleFunc (posPart f)) a✝¹ = max (↑(toSimpleFunc f) a✝¹) 0
convert h₂ using 1
no goals
case h.e'_3
α : Type u_1
E : Type ?u.352084
F : Type ?u.352087
𝕜 : Type ?u.352090
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.354465
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.354561
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
eq : ∀ (a : α), ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc f)) a = max (↑(toSimpleFunc f) a) 0
a✝¹ : α
a✝ : ↑(toSimpleFunc (posPart f)) a✝¹ = ↑↑↑(posPart f) a✝¹
h₂ : ↑↑(Lp.posPart ↑f) a✝¹ = max (↑↑↑f a✝¹) 0
h₃ : ↑(toSimpleFunc f) a✝¹ = ↑↑↑f a✝¹
⊢ max (↑(toSimpleFunc f) a✝¹) 0 = max (↑↑↑f a✝¹) 0
rw [h₃]