-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_of_le_of_le {f g₁ g₂ : α → ℝ} (hf : AEStronglyMeasurable f μ)
    (h_le₁ : g₁ ≤ᵐ[μ] f) (h_le₂ : f ≤ᵐ[μ] g₂)
    (h_int₁ : Integrable g₁ μ) (h_int₂ : Integrable g₂ μ) :
    Integrable f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖

Tactic:
filter_upwards [h_le₁, h_le₂] with x hx1 hx2

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ Integrable f μ

Tactic:
exact Integrable.mono (h_int₁.norm.add h_int₂.norm) hf h_le_add

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
refine hx.trans ?_

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ‖g₁ x‖ ⊔ ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ 0 ≤ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
positivity

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖

Tactic:
simp only [Real.norm_eq_abs]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ |f x| ≤ |g₁ x| ⊔ |g₂ x|

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
filter_upwards [this] with x hx

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ‖g₁ x‖ ⊔ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖

Tactic:
exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ‖g₁ x‖ ⊔ ‖g₂ x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
conv_rhs => rw [Real.norm_of_nonneg (by positivity)]

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ ‖g₁ x‖ ⊔ ‖g₂ x‖ ≤ ‖g₁ x‖ + ‖g₂ x‖

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ Integrable f μ

Tactic:
have h_le_add : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖ := by
  filter_upwards [this] with x hx
  refine hx.trans ?_
  conv_rhs => rw [Real.norm_of_nonneg (by positivity)]
  exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
h_le_add : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
⊢ Integrable f μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
x : α
hx1 : g₁ x ≤ f x
hx2 : f x ≤ g₂ x
⊢ |f x| ≤ |g₁ x| ⊔ |g₂ x|

Tactic:
exact abs_le_max_abs_abs hx1 hx2

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ Integrable f μ

Tactic:
have : ∀ᵐ x ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖ := by
  filter_upwards [h_le₁, h_le₂] with x hx1 hx2
  simp only [Real.norm_eq_abs]
  exact abs_le_max_abs_abs hx1 hx2

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᶠ[ae μ] f
h_le₂ : f ≤ᶠ[ae μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ ‖g₁ x‖ ⊔ ‖g₂ x‖
⊢ Integrable f μ