α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ↑(toSimpleFunc (posPart (-f))) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f))
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ↑(toSimpleFunc (negPart f)) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.negPart (toSimpleFunc f))
rw [SimpleFunc.negPart, MeasureTheory.SimpleFunc.negPart]
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ∀ (a : α),
    ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a →
      ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a →
        ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f)) a
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ↑(toSimpleFunc (posPart (-f))) =ᵐ[μ] ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f))
filter_upwards [posPart_toSimpleFunc (-f), neg_toSimpleFunc f]
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f)) a
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
⊢ ∀ (a : α),
    ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a →
      ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a →
        ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f)) a
intro a h₁ h₂
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f)) a
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f)) a
rw [h₁]
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ max (↑(toSimpleFunc (-f)) a) 0 = max (↑(-toSimpleFunc f) a) 0
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (-toSimpleFunc f)) a
show max _ _ = max _ _
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ max ((-↑(toSimpleFunc f)) a) 0 = max (↑(-toSimpleFunc f) a) 0
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ max (↑(toSimpleFunc (-f)) a) 0 = max (↑(-toSimpleFunc f) a) 0
rw [h₂]
no goals
case h
α : Type u_1
E : Type ?u.357414
F : Type ?u.357417
𝕜 : Type ?u.357420
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F
m : MeasurableSpace α
μ : Measure α
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
F' : Type ?u.359795
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace ℝ F'
E' : Type ?u.359891
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : NormedSpace 𝕜 E'
f : { x // x ∈ simpleFunc ℝ 1 μ }
a : α
h₁ : ↑(toSimpleFunc (posPart (-f))) a = ↑(MeasureTheory.SimpleFunc.posPart (toSimpleFunc (-f))) a
h₂ : ↑(toSimpleFunc (-f)) a = (-↑(toSimpleFunc f)) a
⊢ max ((-↑(toSimpleFunc f)) a) 0 = max (↑(-toSimpleFunc f) a) 0
rfl