awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
pos : ∀ (hsig : SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
neg : ∀ (hsig : ¬SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

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

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
neg : 0 ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

Tactic:
rw [condExp_of_not_sigmaFinite hm hsig, eLpNorm_zero]

Premises used: MeasureTheory.eLpNorm_zero, MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : ¬SigmaFinite (μ.trim hm)
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : 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

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : 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:
eLpNorm_mono_ae ?_

Premises used: MeasureTheory.eLpNorm_mono_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
refine : ∀ᵐ (x : α) ∂μ, ‖μ[f | m] x‖ ≤ ‖μ[|f| | m] x‖
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm μ[|f| | m] 1 μ

Tactic:
refine eLpNorm_mono_ae ?_

Premises used: MeasureTheory.eLpNorm_mono_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
h :
  ∀ (x : α) (hx₁ : μ[f | m] x ≤ μ[fun (a : α) ↦ |f a| | m] x) (hx₂ : (-μ[f | m]) x ≤ μ[fun (a : α) ↦ |f a| | m] x),
    ‖μ[f | m] x‖ ≤ ‖μ[|f| | m] x‖
⊢ ∀ᵐ (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₂

Premises used: le_abs_self, MeasureTheory.Integrable.neg, MeasureTheory.condExp_neg, MeasureTheory.condExp_mono, Filter.EventuallyEq.le, MeasureTheory.Integrable.abs, MeasureTheory.ae_of_all, neg_le_abs, Filter.EventuallyLE.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
x : α
hx₁ : μ[f | m] x ≤ μ[fun (a : α) ↦ |f a| | m] x
hx₂ : (-μ[f | m]) x ≤ μ[fun (a : α) ↦ |f a| | m] x
⊢ ‖μ[f | m] x‖ ≤ ‖μ[|f| | m] x‖

Tactic:
abs_le_abs hx₁ hx₂

Premises used: abs_le_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
x : α
hx₁ : μ[f | m] x ≤ μ[fun (a : α) ↦ |f a| | m] x
hx₂ : (-μ[f | m]) x ≤ μ[fun (a : α) ↦ |f a| | m] x
⊢ ‖μ[f | m] x‖ ≤ ‖μ[|f| | m] x‖

Tactic:
exact abs_le_abs hx₁ hx₂

Premises used: abs_le_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
rw : Eq (α := ℝ) (∫ (x : α), ‖μ[|f| | m] x‖ ∂μ) (∫ (x : α), ‖f x‖ ∂μ)
⊢ eLpNorm μ[|f| | m] 1 μ = eLpNorm f 1 μ

Tactic:
rw [eLpNorm_one_eq_lintegral_enorm, eLpNorm_one_eq_lintegral_enorm,
        ← ENNReal.toReal_eq_toReal_iff' (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]

Premises used: ENNReal.toReal_eq_toReal_iff', MeasureTheory.integral_norm_eq_lintegral_enorm, MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.eLpNorm_one_eq_lintegral_enorm, And.right, And.left, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono, Iff.mp, MeasureTheory.hasFiniteIntegral_iff_enorm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
rw : Eq (α := ℝ) (∫ (x : α), |μ[|f| | m] x| ∂μ) (∫ (x : α), μ[fun (x : α) ↦ |f x| | m] x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α), |μ[|f| | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)

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

Premises used: MeasureTheory.integral_condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ Eq (α := ℝ) (∫ (x : α), |μ[|f| | m] x| ∂μ) (∫ (x : α), μ[fun (x : α) ↦ |f x| | m] x ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
refine : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[|f| | m] x|) μ[fun (x : α) ↦ |f x| | m]
⊢ Eq (α := ℝ) (∫ (x : α), |μ[|f| | m] x| ∂μ) (∫ (x : α), μ[fun (x : α) ↦ |f x| | m] x ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
rw : μ[0 | m] ≤ᶠ[ae μ] μ[|f| | m]
rw₁ rw₂ : MeasurableSpace α
rw₃ : Measure α
⊢ 0 ≤ᶠ[ae μ] μ[|f| | m]

Tactic:
rw [← condExp_zero]

Premises used: MeasureTheory.condExp_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ μ[0 | m] ≤ᶠ[ae μ] μ[|f| | m]

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

Premises used: MeasureTheory.condExp_mono, MeasureTheory.integrable_zero, MeasureTheory.Integrable.abs, MeasureTheory.ae_of_all, abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ 0 ≤ᶠ[ae μ] μ[|f| | 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|))
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
this : 0 ≤ᶠ[ae μ] μ[|f| | m]
h : ∀ (x : α) (hx : 0 x ≤ μ[|f| | m] x), |μ[|f| | m] x| = μ[fun (x : α) ↦ |f x| | m] x
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[|f| | m] x|) μ[fun (x : α) ↦ |f x| | m]

Tactic:
filter_upwards [this] with x hx
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : 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:
abs_eq_self.2 hx

Premises used: Iff.mpr, abs, abs_eq_self
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : 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

Premises used: Iff.mpr, abs_eq_self
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
eLpNorm : MeasureTheory.eLpNorm μ[f | m] 1 μ ≤ MeasureTheory.eLpNorm μ[|f| | m] 1 μ
eLpNorm₁ : MeasureTheory.eLpNorm μ[|f| | m] 1 μ = MeasureTheory.eLpNorm f 1 μ
⊢ MeasureTheory.eLpNorm μ[f | m] 1 μ ≤ MeasureTheory.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_iff' (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

Premises used: abs, MeasureTheory.condExp, OfNat.ofNat, MeasureTheory.eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
pos : ∀ (hm : m ≤ m0), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
neg : ∀ (hm : ¬m ≤ m0), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)

Tactic:
by_cases hm : m ≤ m0
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
neg : LE.le (α := ℝ) 0 (∫ (x : α), |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)

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

Premises used: Pi.zero_apply, MeasureTheory.condExp_of_not_le, abs_zero, MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ LE.le (α := ℝ) 0 (∫ (x : α), |f x| ∂μ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
pos : ∀ (hfint : Integrable f μ), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
neg : ∀ (hfint : ¬Integrable f μ), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)

Tactic:
by_cases hfint : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
neg : LE.le (α := ℝ) 0 (∫ (x : α), |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)

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

Premises used: Pi.zero_apply, MeasureTheory.condExp_of_not_integrable, MulZeroClass.mul_zero, abs_zero, MeasureTheory.integral_const, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ LE.le (α := ℝ) 0 (∫ (x : α), |f x| ∂μ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos : (∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal
pos₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |f x|
pos₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ |f x|) μ
pos₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |μ[f | m] x|
pos₄ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ |μ[f | m] x|) μ
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos : ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≠ ∞
pos₁ : ∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ
⊢ (∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal

Tactic:
apply ENNReal.toReal_mono

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos : ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≠ ∞

Tactic:
simp_rw [← Real.norm_eq_abs, ofReal_norm]

Premises used: ofReal_norm, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos : ∫⁻ (a : α), ‖μ[f | m] a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
⊢ ∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ

Tactic:
simp_rw [← Real.norm_eq_abs, ofReal_norm]

Premises used: ofReal_norm, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≠ ∞

Tactic:
hfint.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≠ ∞

Tactic:
exact hfint.2.ne

Premises used: And.right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos : eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
⊢ ∫⁻ (a : α), ‖μ[f | m] a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ

Tactic:
rw [← eLpNorm_one_eq_lintegral_enorm, ← eLpNorm_one_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

Tactic:
eLpNorm_one_condExp_le_eLpNorm _

Premises used: MeasureTheory.eLpNorm_one_condExp_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : 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 _

Premises used: MeasureTheory.eLpNorm_one_condExp_le_eLpNorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
x : α
⊢ 0 x ≤ |f x|

Tactic:
abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos :
  ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ |f x|) x)) x} a
pos₁ pos₂ : ∀ (x : α), 0 x ≤ |f x|
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |f x|

Tactic:
filter_upwards with x using abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
hfint.1.norm

Premises used: MeasureTheory.AEStronglyMeasurable.norm, And.left
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ ‖f x‖) μ

Tactic:
exact hfint.1.norm

Premises used: MeasureTheory.AEStronglyMeasurable.norm, And.left
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
x : α
⊢ 0 x ≤ |μ[f | m] x|

Tactic:
abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos :
  ∀ (a : α),
    Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ |μ[f | m] x|) x)) x} a
pos₁ pos₂ : ∀ (x : α), 0 x ≤ |μ[f | m] x|
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |μ[f | m] x|

Tactic:
filter_upwards with x using abs_nonneg _

Premises used: abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ ‖μ[f | m] x‖) μ

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

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : 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

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.norm, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
pos : ∀ (hnm : m ≤ m0), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
neg : ∀ (hnm : ¬m ≤ m0), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)

Tactic:
by_cases hnm : m ≤ m0
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : ¬m ≤ m0
neg : LE.le (α := ℝ) 0 (∫ (x : α) in s, |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)

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

Premises used: Pi.zero_apply, MeasureTheory.condExp_of_not_le, abs_zero, MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : ¬m ≤ m0
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, |f x| ∂μ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
pos : ∀ (hfint : Integrable f μ), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
neg : ∀ (hfint : ¬Integrable f μ), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)

Tactic:
by_cases hfint : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : ¬Integrable f μ
neg : LE.le (α := ℝ) 0 (∫ (x : α) in s, |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)

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

Premises used: Pi.zero_apply, MeasureTheory.condExp_of_not_integrable, MulZeroClass.mul_zero, abs_zero, MeasureTheory.integral_const, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : ¬Integrable f μ
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, |f x| ∂μ)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
rw : Eq (α := ℝ) (∫ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)

Tactic:
rw [← integral_indicator (hnm _ hs)]

Premises used: MeasureTheory.integral_indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
refine : (ae μ).EventuallyEq (β := ℝ) (s.indicator fun (x : α) ↦ |μ[f | m] x|) fun (x : α) ↦ |μ[s.indicator f | m] x|
⊢ Eq (α := ℝ) (∫ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[s.indicator f | m] x|) fun (x : α) ↦ |s.indicator μ[f | m] x|

Tactic:
have : (fun x => |(μ[s.indicator f | m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f | m]) x| :=
      (condExp_indicator hfint hs).fun_comp abs