-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem eLpNorm_one_condExp_le_eLpNorm (f : α → ℝ) : eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∀ᵐ (x : α) ∂μ, ‖(μ[f|m]) x‖ ≤ ‖(μ[|f| |m]) x‖

Tactic:
filter_upwards [condExp_mono hf hf.abs
  (ae_of_all μ (fun x => le_abs_self (f x) : ∀ x, f x ≤ |f x|)),
  (condExp_neg ..).symm.le.trans (condExp_mono hf.neg hf.abs
    (ae_of_all μ (fun x => neg_le_abs (f x) : ∀ x, -f x ≤ |f x|)))] with x hx₁ hx₂

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
x : α
hx₁ : (μ[f|?m.9696]) x ≤ (μ[fun a => |f a| |?m.9696]) x
hx₂ : (-μ[f|?m.8598]) x ≤ (μ[fun a => |f a| |?m.8598]) x
⊢ ‖(μ[f|m]) x‖ ≤ ‖(μ[|f| |m]) x‖

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm (μ[|f| |m]) 1 μ

Tactic:
refine eLpNorm_mono_ae ?_

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∀ᵐ (x : α) ∂μ, ‖(μ[f|m]) x‖ ≤ ‖(μ[|f| |m]) x‖

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
by_cases hf : Integrable f μ

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

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
exact zero_le _

Result:
no goals

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

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
swap

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

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

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

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
swap

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
exact zero_le _

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ?m.15243[0|?m.15241] ≤ᶠ[ae μ] μ[|f| |m]

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ MeasurableSpace α

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ MeasurableSpace α

α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ Measure α

Tactic:
exact condExp_mono (integrable_zero _ _ _) hf.abs
  (ae_of_all μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))

Result:
no goals

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
rw [condExp_of_not_integrable hf, eLpNorm_zero]

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ 0 ≤ eLpNorm f 1 μ

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

Tactic:
have : 0 ≤ᵐ[μ] μ[(|f|)|m] := by
  rw [← condExp_zero]
  exact condExp_mono (integrable_zero _ _ _) hf.abs
    (ae_of_all μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
this : 0 ≤ᶠ[ae μ] μ[|f| |m]
⊢ (fun x => |(μ[|f| |m]) x|) =ᶠ[ae μ] μ[fun x => |f x| |m]

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

Tactic:
filter_upwards [this] with x hx

Result:
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
this : 0 ≤ᶠ[ae μ] μ[|f| |m]
x : α
hx : 0 x ≤ (μ[|f| |m]) x
⊢ |(μ[|f| |m]) x| = (μ[fun x => |f x| |m]) x

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[|f| |m]) 1 μ = eLpNorm f 1 μ

Tactic:
rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm,
  ← ENNReal.toReal_eq_toReal (hasFiniteIntegral_iff_enorm.mp integrable_condExp.2).ne
    (hasFiniteIntegral_iff_enorm.mp hf.2).ne,
  ← integral_norm_eq_lintegral_enorm
    (stronglyMeasurable_condExp.mono hm).aestronglyMeasurable,
  ← integral_norm_eq_lintegral_enorm hf.1]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), ‖(μ[|f| |m]) x‖ ∂μ = ∫ (x : α), ‖f x‖ ∂μ

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

case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
swap

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

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

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
rw [condExp_of_not_sigmaFinite hm hsig, eLpNorm_zero]

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ eLpNorm f 1 μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |(μ[|f| |m]) x| ∂μ = ∫ (x : α), |f x| ∂μ

Tactic:
rw (config := {occs := .pos [2]}) [← integral_condExp hm]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ ∫ (x : α), |(μ[|f| |m]) x| ∂μ = ∫ (x : α), (μ[fun x => |f x| |m]) x ∂μ