-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem integral_abs_condExp_le (f : α → ℝ) : ∫ x, |(μ[f|m]) x| ∂μ ≤ ∫ x, |f x| ∂μ

Proof state:
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => ‖(μ[f|m]) x‖) μ

Tactic:
exact (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable.norm

Result:
no goals

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
swap

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
by_cases hfint : Integrable f μ

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Proof state:
case pos.hb
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≠ ⊤

Tactic:
exact hfint.2.ne

Result:
no goals

Proof state:
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => ‖f x‖) μ

Tactic:
exact hfint.1.norm

Result:
no goals

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal |(μ[f|m]) a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal

Tactic:
apply ENNReal.toReal_mono <;> simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_enorm]

Result:
case pos.hb
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≠ ⊤

case pos.h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖(μ[f|m]) a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => |f x|) μ

Tactic:
simp_rw [← Real.norm_eq_abs]

Result:
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => ‖f x‖) μ

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
simp only [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero, integral_const,
  Algebra.id.smul_eq_mul, mul_zero]

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ

Proof state:
case pos.h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖(μ[f|m]) a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
rw [← eLpNorm_one_eq_lintegral_enorm, ← eLpNorm_one_eq_lintegral_enorm]

Result:
case pos.h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Proof state:
case pos.h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
exact eLpNorm_one_condExp_le_eLpNorm _

Result:
no goals

Proof state:
case pos.hf
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] fun x => |f x|

Tactic:
filter_upwards with x using abs_nonneg _

Result:
no goals

Proof state:
case pos.hf
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] fun x => |(μ[f|m]) x|

Tactic:
filter_upwards with x using abs_nonneg _

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
by_cases hm : m ≤ m0

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]

Result:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ (∫⁻ (a : α), ENNReal.ofReal |(μ[f|m]) a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal

case pos.hf
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] fun x => |f x|

case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => |f x|) μ

case pos.hf
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ 0 ≤ᶠ[ae μ] fun x => |(μ[f|m]) x|

case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => |(μ[f|m]) x|) μ

Proof state:
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
swap

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ

Tactic:
simp_rw [condExp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero]

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ

Proof state:
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => |(μ[f|m]) x|) μ

Tactic:
simp_rw [← Real.norm_eq_abs]

Result:
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (fun x => ‖(μ[f|m]) x‖) μ