α : Type u_1
E : Type ?u.8095959
F : Type ?u.8095962
G : Type ?u.8095965
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
f : { x // x ∈ Lp ℝ p }
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(posPart (-f)) a = max (-↑↑f a) 0
α : Type u_1
E : Type ?u.8095959
F : Type ?u.8095962
G : Type ?u.8095965
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
f : { x // x ∈ Lp ℝ p }
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(negPart f) a = max (-↑↑f a) 0
rw [negPart]
case h
α : Type u_1
E : Type ?u.8095959
F : Type ?u.8095962
G : Type ?u.8095965
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
f : { x // x ∈ Lp ℝ p }
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ ↑↑(posPart (-f)) a✝ = max (-↑↑f a✝) 0
α : Type u_1
E : Type ?u.8095959
F : Type ?u.8095962
G : Type ?u.8095965
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
f : { x // x ∈ Lp ℝ p }
⊢ ∀ᵐ (a : α) ∂μ, ↑↑(posPart (-f)) a = max (-↑↑f a) 0
filter_upwards [coeFn_posPart (-f), coeFn_neg f] with _ h₁ h₂
no goals
case h
α : Type u_1
E : Type ?u.8095959
F : Type ?u.8095962
G : Type ?u.8095965
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
f : { x // x ∈ Lp ℝ p }
a✝ : α
h₁ : ↑↑(posPart (-f)) a✝ = max (↑↑(-f) a✝) 0
h₂ : ↑↑(-f) a✝ = (-↑↑f) a✝
⊢ ↑↑(posPart (-f)) a✝ = max (-↑↑f a✝) 0
rw [h₁, h₂, Pi.neg_apply]