-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem norm_integral_le_lintegral_norm (f : α → G) :
    ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ)

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : Integrable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : ¬Integrable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : ¬Integrable f μ
⊢ 0 ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
exact toReal_nonneg

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : ¬CompleteSpace G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : ¬Integrable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
rw [integral_undef hf, norm_zero]

Result:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : ¬Integrable f μ
⊢ 0 ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : Integrable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
rw [integral_eq f hf, ← Integrable.norm_toL1_eq_lintegral_norm f hf]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : Integrable f μ
⊢ ‖L1.integral (Integrable.toL1 f hf)‖ ≤ ‖Integrable.toL1 f hf‖

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : ¬CompleteSpace G
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
hf : Integrable f μ
⊢ ‖L1.integral (Integrable.toL1 f hf)‖ ≤ ‖Integrable.toL1 f hf‖

Tactic:
exact L1.norm_integral_le _

Result:
no goals