-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem eLpNorm_one_condExp_le_eLpNorm (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
⊢ eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm f 1 μ

Tactic:
rw [condExp_of_not_le hm, eLpNorm_zero]

Result:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ 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:
simp_rw [Real.norm_eq_abs]

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:
α : 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 ∂μ

Tactic:
refine integral_congr_ae ?_

Result:
α : 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]

Proof state:
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ 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 μ

Tactic:
by_cases hm : m ≤ m0

Result:
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 μ

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 μ

Tactic:
by_cases hsig : SigmaFinite (μ.trim hm)

Result:
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 μ

Proof state:
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‖

Tactic:
exact abs_le_abs hx₁ hx₂

Result:
no goals

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 μ

Tactic:
calc
  eLpNorm (μ[f|m]) 1 μ ≤ eLpNorm (μ[(|f|)|m]) 1 μ := by
    refine eLpNorm_mono_ae ?_
    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₂
    exact abs_le_abs hx₁ hx₂
  _ = eLpNorm f 1 μ := by
    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]
    simp_rw [Real.norm_eq_abs]
    rw (config := {occs := .pos [2]}) [← integral_condExp hm]
    refine integral_congr_ae ?_
    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|))
    filter_upwards [this] with x hx
    exact abs_eq_self.2 hx

Result:
no goals

Proof state:
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

Tactic:
exact abs_eq_self.2 hx

Result:
no goals

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

Tactic:
rw [← condExp_zero]

Result:
α : 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 α