awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ)
    (∫ (x : α) in s, f x ∂μ)
have refine_2 : ∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ =
  (↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))) :
      Set α → ℝ)
    s
Tactic: conv_rhs => rw [← hf.withDensityᵥ_trim_eq_integral hm hs,
      ← SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
        (hf.withDensityᵥ_trim_absolutelyContinuous hm)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ =
    (↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))) :
        Set α → ℝ)
      s
have rw : StronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))
Tactic: rw [withDensityᵥ_apply
      (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) hs,
      ← setIntegral_trim hm _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have pos : ∀ (hf : Integrable f μ), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
pos : ∀ (hf : Integrable f μ), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have neg : ∀ (hf : ¬Integrable f μ), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have neg : 0 ≤ eLpNorm f 1 μ
Tactic: rw [condExp_of_not_integrable hf, eLpNorm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have pos : ∀ (hm : m ≤ m0), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: by_cases hm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
pos : ∀ (hm : m ≤ m0), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have neg : ∀ (hm : ¬m ≤ m0), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: by_cases hm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have neg : 0 ≤ eLpNorm f 1 μ
Tactic: rw [condExp_of_not_le hm, eLpNorm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have pos : ∀ (hsig : SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: by_cases hsig : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
have neg : ∀ (hsig : ¬SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: by_cases hsig : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 1 μ
have neg : 0 ≤ eLpNorm f 1 μ
Tactic: rw [condExp_of_not_sigmaFinite hm hsig, eLpNorm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 μ
have refine : ∀ᵐ (x : α) ∂μ, ‖μ[f | m] x‖ ≤ ‖μ[|f| | m] x‖
Tactic: refine eLpNorm_mono_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : 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‖
have 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‖
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₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 1 μ
have rw : Eq (α := ℝ) (∫ (x : α), ‖μ[|f| | m] x‖ ∂μ) (∫ (x : α), ‖f x‖ ∂μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : α), |f x| ∂μ)
have rw : Eq (α := ℝ) (∫ (x : α), |μ[|f| | m] x| ∂μ) (∫ (x : α), μ[fun (x : α) ↦ |f x| | m] x ∂μ)
Tactic: rw (config := { occs := .pos [2] }) [← integral_condExp hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[|f| | m] x|) μ[fun (x : α) ↦ |f x| | m]
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ 0 ≤ᶠ[ae μ] μ[|f| | m]
have rw : μ[0 | m] ≤ᶠ[ae μ] μ[|f| | m]
Tactic: rw [← condExp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[|f| | m] x|) μ[fun (x : α) ↦ |f x| | m]
have this : 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|))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : m ≤ m0
hsig : SigmaFinite (μ.trim hm)
this : 0 ≤ᶠ[ae μ] μ[|f| | m]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[|f| | m] x|) μ[fun (x : α) ↦ |f x| | m]
have h : ∀ (x : α) (hx : 0 x ≤ μ[|f| | m] x), |μ[|f| | m] x| = μ[fun (x : α) ↦ |f x| | m] x
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 1 μ
have eLpNorm : eLpNorm μ[f | m] 1 μ ≤ eLpNorm μ[|f| | m] 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 μ
⊢ MeasureTheory.eLpNorm μ[f | m] 1 μ ≤ MeasureTheory.eLpNorm f 1 μ
have eLpNorm₁ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos : ∀ (hm : m ≤ m0), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
Tactic: by_cases hm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
pos : ∀ (hm : m ≤ m0), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have neg : ∀ (hm : ¬m ≤ m0), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
Tactic: by_cases hm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have neg : LE.le (α := ℝ) 0 (∫ (x : α), |f x| ∂μ)
Tactic: simp_rw [condExp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos : ∀ (hfint : Integrable f μ), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have neg : ∀ (hfint : ¬Integrable f μ), LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have neg : LE.le (α := ℝ) 0 (∫ (x : α), |f x| ∂μ)
Tactic: simp only [condExp_of_not_integrable hfint, Pi.zero_apply, abs_zero, integral_const,
      smul_eq_mul, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos : (∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |f x|
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos₂ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ |f x|) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|) μ
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos₃ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |μ[f | m] x|
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[f | m] x| ∂μ) (∫ (x : α), |f x| ∂μ)
have pos₄ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ |μ[f | m] x|) μ
Tactic: rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : 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
have pos : ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≠ ∞
Tactic: apply ENNReal.toReal_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
pos : ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≠ ∞
⊢ (∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ).toReal
have pos₁ : ∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ
Tactic: apply ENNReal.toReal_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≠ ∞
have pos : ∫⁻ (a : α), ‖f a‖ₑ ∂μ ≠ ∞
Tactic: simp_rw [← Real.norm_eq_abs, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal |μ[f | m] a| ∂μ ≤ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ
have pos : ∫⁻ (a : α), ‖μ[f | m] a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
Tactic: simp_rw [← Real.norm_eq_abs, ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ ∫⁻ (a : α), ‖μ[f | m] a‖ₑ ∂μ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
have pos : eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
Tactic: rw [← eLpNorm_one_eq_lintegral_enorm, ← eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |f x|
have pos : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ |f x|) x)) x} a
Tactic: filter_upwards with x using abs_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |f x|
have pos₁ : ∀ (a : α), 0 a ≤ |f a|
Tactic: filter_upwards with x using abs_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |μ[f | m] x|
have pos : ∀ (a : α),
  Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ |μ[f | m] x|) x)) x} a
Tactic: filter_upwards with x using abs_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ |μ[f | m] x|
have pos₁ : ∀ (a : α), 0 a ≤ |μ[f | m] a|
Tactic: filter_upwards with x using abs_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have pos : ∀ (hnm : m ≤ m0), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
Tactic: by_cases hnm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have neg : ∀ (hnm : ¬m ≤ m0), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
Tactic: by_cases hnm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : ¬m ≤ m0
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have neg : LE.le (α := ℝ) 0 (∫ (x : α) in s, |f x| ∂μ)
Tactic: simp_rw [condExp_of_not_le hnm, Pi.zero_apply, abs_zero, integral_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have pos : ∀ (hfint : Integrable f μ), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have neg : ∀ (hfint : ¬Integrable f μ), LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : ¬Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have neg : LE.le (α := ℝ) 0 (∫ (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]