case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r

case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
by_cases hr : r = 0
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r

case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
by_cases hμ : IsFiniteMeasure μ
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r

case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r

case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
swap
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
haveI := hμ
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
have hposbdd : (∫ ω, max (f ω) 0 ∂μ) ≤ (μ Set.univ).toReal • (r : ℝ) := by
  rw [← integral_const]
  refine' integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) _
  filter_upwards [hf]with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ (∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) ^ (ENNReal.toReal 1)⁻¹ ≤ ENNReal.toReal (2 * ↑↑μ univ * ↑r)
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
rw [Memℒp.snorm_eq_integral_rpow_norm one_ne_zero ENNReal.one_ne_top
    (memℒp_one_iff_integrable.2 hfint),
  ENNReal.ofReal_le_iff_le_toReal
    (ENNReal.mul_ne_top (ENNReal.mul_ne_top ENNReal.two_ne_top <| @measure_ne_top _ _ _ hμ _)
      ENNReal.coe_ne_top)]
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ (∫ (a : α), ↑(Real.toNNReal (f a)) + ↑(Real.toNNReal (-f a)) ∂μ) ≤ ENNReal.toReal (2 * ↑↑μ univ * ↑r)
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ (∫ (a : α), ‖f a‖ ^ ENNReal.toReal 1 ∂μ) ^ (ENNReal.toReal 1)⁻¹ ≤ ENNReal.toReal (2 * ↑↑μ univ * ↑r)
simp_rw [ENNReal.one_toReal, _root_.inv_one, Real.rpow_one, Real.norm_eq_abs, ←
  max_zero_add_max_neg_zero_eq_abs_self, ← Real.coe_toNNReal']
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ ((∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ) + ∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ENNReal.toReal (2 * ↑↑μ univ * ↑r)

case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ Integrable fun a => ↑(Real.toNNReal (-f a))
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ (∫ (a : α), ↑(Real.toNNReal (f a)) + ↑(Real.toNNReal (-f a)) ∂μ) ≤ ENNReal.toReal (2 * ↑↑μ univ * ↑r)
rw [integral_add hfint.real_toNNReal]
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
⊢ f =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
suffices f =ᵐ[μ] 0 by
  rw [snorm_congr_ae this, snorm_zero, hr, ENNReal.coe_zero, MulZeroClass.mul_zero]
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑0
hr : r = 0
⊢ f =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
⊢ f =ᵐ[μ] 0
rw [hr] at hf
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ f =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑0
hr : r = 0
⊢ f =ᵐ[μ] 0
norm_cast at hf
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
⊢ f =ᵐ[μ] 0
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ f =ᵐ[μ] 0
have hnegf : (∫ x, -f x ∂μ) = 0 := by
  rw [integral_neg, neg_eq_zero]
  exact le_antisymm (integral_nonpos_of_ae hf) hfint'
case pos.refine_2
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
this : -f =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0

case pos.refine_1
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
⊢ 0 ≤ᵐ[μ] -f
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
⊢ f =ᵐ[μ] 0
have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
no goals
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : r = 0
this : f =ᵐ[μ] 0
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
rw [snorm_congr_ae this, snorm_zero, hr, ENNReal.coe_zero, MulZeroClass.mul_zero]
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ (∫ (a : α), f a ∂μ) = 0
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ (∫ (x : α), -f x ∂μ) = 0
rw [integral_neg, neg_eq_zero]
no goals
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ (∫ (a : α), f a ∂μ) = 0
exact le_antisymm (integral_nonpos_of_ae hf) hfint'
case h
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
this : -f =ᵐ[μ] 0
ω : α
hω : (-f) ω = OfNat.ofNat 0 ω
⊢ f ω = OfNat.ofNat 0 ω
case pos.refine_2
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
this : -f =ᵐ[μ] 0
⊢ f =ᵐ[μ] 0
filter_upwards [this]with ω hω
no goals
case h
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
this : -f =ᵐ[μ] 0
ω : α
hω : (-f) ω = OfNat.ofNat 0 ω
⊢ f ω = OfNat.ofNat 0 ω
rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
case h
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
ω : α
hω : f ω ≤ 0
⊢ OfNat.ofNat 0 ω ≤ (-f) ω
case pos.refine_1
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
⊢ 0 ≤ᵐ[μ] -f
filter_upwards [hf]with ω hω
no goals
case h
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
hnegf : (∫ (x : α), -f x ∂μ) = 0
ω : α
hω : f ω ≤ 0
⊢ OfNat.ofNat 0 ω ≤ (-f) ω
rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
have : μ Set.univ = ∞ := by
  by_contra hμ'
  exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ snorm f 1 μ ≤ ⊤

case neg.hnc
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ ¬↑r = 0

case neg.hnc
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ ¬2 = 0
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ snorm f 1 μ ≤ 2 * ↑↑μ univ * ↑r
rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬↑↑μ univ = ⊤
⊢ False
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
⊢ ↑↑μ univ = ⊤
by_contra hμ'
no goals
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
hμ' : ¬↑↑μ univ = ⊤
⊢ False
exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
no goals
case neg
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ snorm f 1 μ ≤ ⊤
exact le_top
no goals
case neg.hnc
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ ¬↑r = 0
simp [hr]
no goals
case neg.hnc
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ : ¬IsFiniteMeasure μ
this : ↑↑μ univ = ⊤
⊢ ¬2 = 0
norm_num
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ∫ (x : α), ↑r ∂μ
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
rw [← integral_const]
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ (fun ω => max (f ω) 0) ≤ᵐ[μ] fun x => ↑r
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ∫ (x : α), ↑r ∂μ
refine' integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) _
no goals
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ (fun ω => max (f ω) 0) ≤ᵐ[μ] fun x => ↑r
filter_upwards [hf]with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), max (-f a) 0 ∂μ) ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ ((∫ (a : α), max (f a) 0 ∂μ) + ∫ (a : α), max (-f a) 0 ∂μ) ≤ 2 * ENNReal.toReal (↑↑μ univ) * ↑r
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ ((∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ) + ∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ENNReal.toReal (2 * ↑↑μ univ * ↑r)
simp only [Real.coe_toNNReal', ENNReal.toReal_mul, ENNReal.one_toReal, ENNReal.coe_toReal,
  ge_iff_le, Left.nonneg_neg_iff, Left.neg_nonpos_iff, toReal_ofNat] at hfint' ⊢
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), max (-f a) 0 ∂μ) ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ ((∫ (a : α), max (f a) 0 ∂μ) + ∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * ENNReal.toReal (↑↑μ univ) * ↑r
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), max (-f a) 0 ∂μ) ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ ((∫ (a : α), max (f a) 0 ∂μ) + ∫ (a : α), max (-f a) 0 ∂μ) ≤ 2 * ENNReal.toReal (↑↑μ univ) * ↑r
refine' (add_le_add_left hfint' _).trans _
no goals
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), max (-f a) 0 ∂μ) ≤ ∫ (a : α), max (f a) 0 ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ ((∫ (a : α), max (f a) 0 ∂μ) + ∫ (a : α), max (f a) 0 ∂μ) ≤ 2 * ENNReal.toReal (↑↑μ univ) * ↑r
rwa [← two_mul, mul_assoc, mul_le_mul_left (two_pos : (0 : ℝ) < 2)]
no goals
case pos
α : Type u_1
E : Type ?u.1745269
F : Type ?u.1745272
𝕜 : Type ?u.1745275
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
m0 : MeasurableSpace α
μ : Measure α
r : ℝ≥0
f : α → ℝ
hfint : Integrable f
hfint' : (∫ (a : α), ↑(Real.toNNReal (-f a)) ∂μ) ≤ ∫ (a : α), ↑(Real.toNNReal (f a)) ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : (∫ (ω : α), max (f ω) 0 ∂μ) ≤ ENNReal.toReal (↑↑μ univ) • ↑r
⊢ Integrable fun a => ↑(Real.toNNReal (-f a))
exact hfint.neg.sup (integrable_zero _ _ μ)