[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
⊢ SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm) =ᵐ[μ] μ[f|m]
[PROOFSTEP]
refine' ae_eq_condexp_of_forall_set_integral_eq hm hf _ _ _
[GOAL]
case refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s < ⊤ →
        IntegrableOn (SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm)) s
[PROOFSTEP]
exact fun _ _ _ =>
  (integrable_of_integrable_trim hm
      (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))).integrableOn
[GOAL]
case refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
⊢ ∀ (s : Set α),
    MeasurableSet s →
      ↑↑μ s < ⊤ →
        ∫ (x : α) in s,
            SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm) x ∂μ =
          ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
intro s hs _
[GOAL]
case refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
s : Set α
hs : MeasurableSet s
a✝ : ↑↑μ s < ⊤
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm) x ∂μ =
    ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
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)]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
s : Set α
hs : MeasurableSet s
a✝ : ↑↑μ s < ⊤
| ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
rw [← hf.withDensityᵥ_trim_eq_integral hm hs, ←
    SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
      (hf.withDensityᵥ_trim_absolutelyContinuous hm)]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
s : Set α
hs : MeasurableSet s
a✝ : ↑↑μ s < ⊤
| ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
rw [← hf.withDensityᵥ_trim_eq_integral hm hs, ←
    SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
      (hf.withDensityᵥ_trim_absolutelyContinuous hm)]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
s : Set α
hs : MeasurableSet s
a✝ : ↑↑μ s < ⊤
| ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
rw [← hf.withDensityᵥ_trim_eq_integral hm hs, ←
  SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
    (hf.withDensityᵥ_trim_absolutelyContinuous hm)]
[GOAL]
case refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
s : Set α
hs : MeasurableSet s
a✝ : ↑↑μ s < ⊤
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm) x ∂μ =
    ↑(Measure.withDensityᵥ (Measure.trim μ hm)
          (SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm)))
      s
[PROOFSTEP]
rw [withDensityᵥ_apply (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) hs, ←
  set_integral_trim hm _ hs]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
s : Set α
hs : MeasurableSet s
a✝ : ↑↑μ s < ⊤
⊢ StronglyMeasurable fun x =>
    SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm) x
[PROOFSTEP]
exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable
[GOAL]
case refine'_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
f : α → ℝ
hf : Integrable f
⊢ AEStronglyMeasurable' m (SignedMeasure.rnDeriv (VectorMeasure.trim (Measure.withDensityᵥ μ f) hm) (Measure.trim μ hm))
    μ
[PROOFSTEP]
exact StronglyMeasurable.aeStronglyMeasurable' (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
by_cases hf : Integrable f μ
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
rw [condexp_undef hf, snorm_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ 0 ≤ snorm f 1 μ
[PROOFSTEP]
exact zero_le _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
by_cases hm : m ≤ m0
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : ¬m ≤ m0
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : ¬m ≤ m0
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
rw [condexp_of_not_le hm, snorm_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : ¬m ≤ m0
⊢ 0 ≤ snorm f 1 μ
[PROOFSTEP]
exact zero_le _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
by_cases hsig : SigmaFinite (μ.trim hm)
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : ¬SigmaFinite (Measure.trim μ hm)
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : ¬SigmaFinite (Measure.trim μ hm)
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
rw [condexp_of_not_sigmaFinite hm hsig, snorm_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : ¬SigmaFinite (Measure.trim μ hm)
⊢ 0 ≤ snorm f 1 μ
[PROOFSTEP]
exact zero_le _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ snorm (μ[f|m]) 1 μ ≤ snorm f 1 μ
[PROOFSTEP]
calc
  snorm (μ[f|m]) 1 μ ≤ snorm (μ[(|f|)|m]) 1 μ := by
    refine' snorm_mono_ae _
    filter_upwards [@condexp_mono _ m m0 _ _ _ _ _ _ _ _ hf hf.abs
        (@ae_of_all _ m0 _ μ (fun x => le_abs_self (f x) : ∀ x, f x ≤ |f x|)),
      EventuallyLE.trans (condexp_neg f).symm.le
        (@condexp_mono _ m m0 _ _ _ _ _ _ _ _ hf.neg hf.abs
          (@ae_of_all _ m0 _ μ (fun x => neg_le_abs_self (f x) : ∀ x, -f x ≤ |f x|)))] with
      x hx₁ hx₂
    exact abs_le_abs hx₁ hx₂
  _ = snorm f 1 μ :=
    by
    rw [snorm_one_eq_lintegral_nnnorm, snorm_one_eq_lintegral_nnnorm, ←
      ENNReal.toReal_eq_toReal (ne_of_lt integrable_condexp.2) (ne_of_lt hf.2), ←
      integral_norm_eq_lintegral_nnnorm (stronglyMeasurable_condexp.mono hm).aestronglyMeasurable, ←
      integral_norm_eq_lintegral_nnnorm hf.1]
    simp_rw [Real.norm_eq_abs]
    rw [← @integral_condexp _ _ _ _ _ m m0 μ _ hm hsig hf.abs]
    refine' integral_congr_ae _
    have : 0 ≤ᵐ[μ] μ[(|f|)|m] := by
      rw [← @condexp_zero α ℝ _ _ _ m m0 μ]
      exact
        condexp_mono (integrable_zero _ _ _) hf.abs (@ae_of_all _ m0 _ μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))
    filter_upwards [this] with x hx
    exact abs_eq_self.2 hx
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ snorm (μ[f|m]) 1 μ ≤ snorm (μ[|f||m]) 1 μ
[PROOFSTEP]
refine' snorm_mono_ae _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ ∀ᵐ (x : α) ∂μ, ‖(μ[f|m]) x‖ ≤ ‖(μ[|f||m]) x‖
[PROOFSTEP]
filter_upwards [@condexp_mono _ m m0 _ _ _ _ _ _ _ _ hf hf.abs
    (@ae_of_all _ m0 _ μ (fun x => le_abs_self (f x) : ∀ x, f x ≤ |f x|)),
  EventuallyLE.trans (condexp_neg f).symm.le
    (@condexp_mono _ m m0 _ _ _ _ _ _ _ _ hf.neg hf.abs
      (@ae_of_all _ m0 _ μ (fun x => neg_le_abs_self (f x) : ∀ x, -f x ≤ |f x|)))] with
  x hx₁ hx₂
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.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‖
[PROOFSTEP]
exact abs_le_abs hx₁ hx₂
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ snorm (μ[|f||m]) 1 μ = snorm f 1 μ
[PROOFSTEP]
rw [snorm_one_eq_lintegral_nnnorm, snorm_one_eq_lintegral_nnnorm, ←
  ENNReal.toReal_eq_toReal (ne_of_lt integrable_condexp.2) (ne_of_lt hf.2), ←
  integral_norm_eq_lintegral_nnnorm (stronglyMeasurable_condexp.mono hm).aestronglyMeasurable, ←
  integral_norm_eq_lintegral_nnnorm hf.1]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ ∫ (x : α), ‖(μ[|f||m]) x‖ ∂μ = ∫ (x : α), ‖f x‖ ∂μ
[PROOFSTEP]
simp_rw [Real.norm_eq_abs]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ ∫ (x : α), |(μ[|f||m]) x| ∂μ = ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
rw [← @integral_condexp _ _ _ _ _ m m0 μ _ hm hsig hf.abs]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ ∫ (x : α), |(μ[|f||m]) x| ∂μ = ∫ (x : α), (μ[fun a => |f a||m]) x ∂μ
[PROOFSTEP]
refine' integral_congr_ae _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ (fun x => |(μ[|f||m]) x|) =ᵐ[μ] fun x => (μ[fun a => |f a||m]) x
[PROOFSTEP]
have : 0 ≤ᵐ[μ] μ[(|f|)|m] := by
  rw [← @condexp_zero α ℝ _ _ _ m m0 μ]
  exact condexp_mono (integrable_zero _ _ _) hf.abs (@ae_of_all _ m0 _ μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ 0 ≤ᵐ[μ] μ[|f||m]
[PROOFSTEP]
rw [← @condexp_zero α ℝ _ _ _ m m0 μ]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
⊢ μ[0|m] ≤ᵐ[μ] μ[|f||m]
[PROOFSTEP]
exact condexp_mono (integrable_zero _ _ _) hf.abs (@ae_of_all _ m0 _ μ (fun x => abs_nonneg (f x) : ∀ x, 0 ≤ |f x|))
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
this : 0 ≤ᵐ[μ] μ[|f||m]
⊢ (fun x => |(μ[|f||m]) x|) =ᵐ[μ] fun x => (μ[fun a => |f a||m]) x
[PROOFSTEP]
filter_upwards [this] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f
hm : m ≤ m0
hsig : SigmaFinite (Measure.trim μ hm)
this : 0 ≤ᵐ[μ] μ[|f||m]
x : α
hx : OfNat.ofNat 0 x ≤ (μ[|f||m]) x
⊢ |(μ[|f||m]) x| = (μ[fun a => |f a||m]) x
[PROOFSTEP]
exact abs_eq_self.2 hx
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
by_cases hm : m ≤ m0
[GOAL]
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| ∂μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
simp_rw [condexp_of_not_le hm, Pi.zero_apply, abs_zero, integral_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => abs_nonneg _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
by_cases hfint : Integrable f μ
[GOAL]
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| ∂μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
simp only [condexp_undef hfint, Pi.zero_apply, abs_zero, integral_const, Algebra.id.smul_eq_mul, mul_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : ¬Integrable f
⊢ 0 ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => abs_nonneg _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ∫ (x : α), |(μ[f|m]) x| ∂μ ≤ ∫ (x : α), |f x| ∂μ
[PROOFSTEP]
rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal |(μ[f|m]) a| ∂μ) ≤ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ)
[PROOFSTEP]
rw [ENNReal.toReal_le_toReal]
[GOAL]
case pos
α : 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| ∂μ
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_coe_nnnorm]
[GOAL]
case pos.ha
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ∫⁻ (a : α), ENNReal.ofReal |(μ[f|m]) a| ∂μ ≠ ⊤
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_coe_nnnorm]
[GOAL]
case pos.hb
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ∫⁻ (a : α), ENNReal.ofReal |f a| ∂μ ≠ ⊤
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs, ofReal_norm_eq_coe_nnnorm]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ∫⁻ (a : α), ↑‖(μ[f|m]) a‖₊ ∂μ ≤ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
[PROOFSTEP]
rw [← snorm_one_eq_lintegral_nnnorm, ← snorm_one_eq_lintegral_nnnorm]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ snorm (fun a => (μ[f|m]) a) 1 μ ≤ snorm (fun a => f a) 1 μ
[PROOFSTEP]
exact snorm_one_condexp_le_snorm _
[GOAL]
case pos.ha
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ∫⁻ (a : α), ↑‖(μ[f|m]) a‖₊ ∂μ ≠ ⊤
[PROOFSTEP]
exact ne_of_lt integrable_condexp.2
[GOAL]
case pos.hb
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ ∫⁻ (a : α), ↑‖f a‖₊ ∂μ ≠ ⊤
[PROOFSTEP]
exact ne_of_lt hfint.2
[GOAL]
case pos.hf
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ 0 ≤ᵐ[μ] fun x => |f x|
[PROOFSTEP]
exact eventually_of_forall fun x => abs_nonneg _
[GOAL]
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ AEStronglyMeasurable (fun x => |f x|) μ
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs]
[GOAL]
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ AEStronglyMeasurable (fun x => ‖f x‖) μ
[PROOFSTEP]
exact hfint.1.norm
[GOAL]
case pos.hf
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ 0 ≤ᵐ[μ] fun x => |(μ[f|m]) x|
[PROOFSTEP]
exact eventually_of_forall fun x => abs_nonneg _
[GOAL]
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ AEStronglyMeasurable (fun x => |(μ[f|m]) x|) μ
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs]
[GOAL]
case pos.hfm
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hm : m ≤ m0
hfint : Integrable f
⊢ AEStronglyMeasurable (fun x => ‖(μ[f|m]) x‖) μ
[PROOFSTEP]
exact (stronglyMeasurable_condexp.mono hm).aestronglyMeasurable.norm
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
by_cases hnm : m ≤ m0
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : ¬m ≤ m0
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : ¬m ≤ m0
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
simp_rw [condexp_of_not_le hnm, Pi.zero_apply, abs_zero, integral_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : ¬m ≤ m0
⊢ 0 ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => abs_nonneg _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
by_cases hfint : Integrable f μ
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : ¬Integrable f
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : ¬Integrable f
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
simp only [condexp_undef hfint, Pi.zero_apply, abs_zero, integral_const, Algebra.id.smul_eq_mul, mul_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : ¬Integrable f
⊢ 0 ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
exact integral_nonneg fun x => abs_nonneg _
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
have : ∫ x in s, |(μ[f|m]) x| ∂μ = ∫ x, |(μ[s.indicator f|m]) x| ∂μ :=
  by
  rw [← integral_indicator]
  swap; · exact hnm _ hs
  refine' integral_congr_ae _
  have : (fun x => |(μ[s.indicator f|m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f|m]) x| :=
    EventuallyEq.fun_comp (condexp_indicator hfint hs) _
  refine' EventuallyEq.trans (eventually_of_forall fun x => _) this.symm
  rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
  rfl
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
[PROOFSTEP]
rw [← integral_indicator]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ ∫ (x : α), Set.indicator s (fun x => |(μ[f|m]) x|) x ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ MeasurableSet s
[PROOFSTEP]
swap
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ MeasurableSet s
[PROOFSTEP]
exact hnm _ hs
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ ∫ (x : α), Set.indicator s (fun x => |(μ[f|m]) x|) x ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
[PROOFSTEP]
refine' integral_congr_ae _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
⊢ (fun x => Set.indicator s (fun x => |(μ[f|m]) x|) x) =ᵐ[μ] fun x => |(μ[Set.indicator s f|m]) x|
[PROOFSTEP]
have : (fun x => |(μ[s.indicator f|m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f|m]) x| :=
  EventuallyEq.fun_comp (condexp_indicator hfint hs) _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : (fun x => |(μ[Set.indicator s f|m]) x|) =ᵐ[μ] fun x => |Set.indicator s (μ[f|m]) x|
⊢ (fun x => Set.indicator s (fun x => |(μ[f|m]) x|) x) =ᵐ[μ] fun x => |(μ[Set.indicator s f|m]) x|
[PROOFSTEP]
refine' EventuallyEq.trans (eventually_of_forall fun x => _) this.symm
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : (fun x => |(μ[Set.indicator s f|m]) x|) =ᵐ[μ] fun x => |Set.indicator s (μ[f|m]) x|
x : α
⊢ (fun x => Set.indicator s (fun x => |(μ[f|m]) x|) x) x = |Set.indicator s (μ[f|m]) x|
[PROOFSTEP]
rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : (fun x => |(μ[Set.indicator s f|m]) x|) =ᵐ[μ] fun x => |Set.indicator s (μ[f|m]) x|
x : α
⊢ (fun x => Set.indicator s (fun x => |(μ[f|m]) x|) x) x = Set.indicator s (fun a => ‖(μ[f|m]) a‖) x
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
⊢ ∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
[PROOFSTEP]
rw [this, ← integral_indicator]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
⊢ ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ ≤ ∫ (x : α), Set.indicator s (fun x => |f x|) x ∂μ
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
⊢ MeasurableSet s
[PROOFSTEP]
swap
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
⊢ MeasurableSet s
[PROOFSTEP]
exact hnm _ hs
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
⊢ ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ ≤ ∫ (x : α), Set.indicator s (fun x => |f x|) x ∂μ
[PROOFSTEP]
refine' (integral_abs_condexp_le _).trans (le_of_eq <| integral_congr_ae <| eventually_of_forall fun x => _)
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f
this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[Set.indicator s f|m]) x| ∂μ
x : α
⊢ (fun x => |Set.indicator s f x|) x = (fun x => Set.indicator s (fun x => |f x|) x) x
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
by_cases hnm : m ≤ m0
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
simp_rw [condexp_of_not_le hnm, Pi.zero_apply, abs_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ ↑R
[PROOFSTEP]
refine' eventually_of_forall fun _ => R.coe_nonneg
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
by_cases hfint : Integrable f μ
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
simp_rw [condexp_undef hfint]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f
⊢ ∀ᵐ (x : α) ∂μ, |OfNat.ofNat 0 x| ≤ ↑R
[PROOFSTEP]
filter_upwards [hbdd] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f
x : α
hx : |f x| ≤ ↑R
⊢ |OfNat.ofNat 0 x| ≤ ↑R
[PROOFSTEP]
rw [Pi.zero_apply, abs_zero]
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : ¬Integrable f
x : α
hx : |f x| ≤ ↑R
⊢ 0 ≤ ↑R
[PROOFSTEP]
exact (abs_nonneg _).trans hx
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
⊢ ∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
[PROOFSTEP]
by_contra h
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : ¬∀ᵐ (x : α) ∂μ, |(μ[f|m]) x| ≤ ↑R
⊢ False
[PROOFSTEP]
change μ _ ≠ 0 at h 
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : ↑↑μ {x | (fun x => |(μ[f|m]) x| ≤ ↑R) x}ᶜ ≠ 0
⊢ False
[PROOFSTEP]
simp only [← zero_lt_iff, Set.compl_def, Set.mem_setOf_eq, not_le] at h 
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ False
[PROOFSTEP]
suffices (μ {x | ↑R < |(μ[f|m]) x|}).toReal * ↑R < (μ {x | ↑R < |(μ[f|m]) x|}).toReal * ↑R by exact this.ne rfl
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
this : ENNReal.toReal (↑↑μ {x | ↑R < |(μ[f|m]) x|}) * ↑R < ENNReal.toReal (↑↑μ {x | ↑R < |(μ[f|m]) x|}) * ↑R
⊢ False
[PROOFSTEP]
exact this.ne rfl
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ ENNReal.toReal (↑↑μ {x | ↑R < |(μ[f|m]) x|}) * ↑R < ENNReal.toReal (↑↑μ {x | ↑R < |(μ[f|m]) x|}) * ↑R
[PROOFSTEP]
refine' lt_of_lt_of_le (set_integral_gt_gt R.coe_nonneg _ _ h.ne.symm) _
[GOAL]
case pos.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ Measurable fun x => |(μ[f|m]) x|
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs]
[GOAL]
case pos.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ Measurable fun x => ‖(μ[f|m]) x‖
[PROOFSTEP]
exact (stronglyMeasurable_condexp.mono hnm).measurable.norm
[GOAL]
case pos.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ IntegrableOn (fun x => |(μ[f|m]) x|) {x | ↑R < |(μ[f|m]) x|}
[PROOFSTEP]
exact integrable_condexp.abs.integrableOn
[GOAL]
case pos.refine'_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ ∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, |(μ[f|m]) x| ∂μ ≤ ENNReal.toReal (↑↑μ {x | ↑R < |(μ[f|m]) x|}) * ↑R
[PROOFSTEP]
refine' (set_integral_abs_condexp_le _ _).trans _
[GOAL]
case pos.refine'_3.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ MeasurableSet {x | ↑R < |(μ[f|m]) x|}
[PROOFSTEP]
simp_rw [← Real.norm_eq_abs]
[GOAL]
case pos.refine'_3.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ MeasurableSet {x | ↑R < ‖(μ[f|m]) x‖}
[PROOFSTEP]
exact @measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const stronglyMeasurable_condexp.norm.measurable
[GOAL]
case pos.refine'_3.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ ∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, |f x| ∂μ ≤ ENNReal.toReal (↑↑μ {x | ↑R < |(μ[f|m]) x|}) * ↑R
[PROOFSTEP]
simp only [← smul_eq_mul, ← set_integral_const, NNReal.val_eq_coe, IsROrC.ofReal_real_eq_id, id.def]
[GOAL]
case pos.refine'_3.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ ∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, |f x| ∂μ ≤ ∫ (x : α) in {x | ↑R < |(μ[f|m]) x|}, ↑R ∂μ
[PROOFSTEP]
refine' set_integral_mono_ae hfint.abs.integrableOn _ _
[GOAL]
case pos.refine'_3.refine'_2.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ IntegrableOn (fun x => ↑R) {x | ↑R < |(μ[f|m]) x|}
[PROOFSTEP]
refine'
  ⟨aestronglyMeasurable_const,
    lt_of_le_of_lt _ (integrable_condexp.integrableOn : IntegrableOn (μ[f|m]) {x | ↑R < |(μ[f|m]) x|} μ).2⟩
[GOAL]
case pos.refine'_3.refine'_2.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ ∫⁻ (a : α) in {x | ↑R < |(μ[f|m]) x|}, ↑‖(fun x => ↑R) a‖₊ ∂μ ≤
    ∫⁻ (a : α) in {x | ↑R < |(μ[f|m]) x|}, ↑‖(μ[f|m]) a‖₊ ∂μ
[PROOFSTEP]
refine'
  set_lintegral_mono (Measurable.nnnorm _).coe_nnreal_ennreal
    (stronglyMeasurable_condexp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal fun x hx => _
[GOAL]
case pos.refine'_3.refine'_2.refine'_1.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ Measurable fun a => (fun x => ↑R) a
[PROOFSTEP]
exact measurable_const
[GOAL]
case pos.refine'_3.refine'_2.refine'_1.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
x : α
hx : x ∈ {x | ↑R < |(μ[f|m]) x|}
⊢ ↑‖(fun x => ↑R) x‖₊ ≤ ↑‖(μ[f|m]) x‖₊
[PROOFSTEP]
rw [ENNReal.coe_le_coe, Real.nnnorm_of_nonneg R.coe_nonneg]
[GOAL]
case pos.refine'_3.refine'_2.refine'_1.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
x : α
hx : x ∈ {x | ↑R < |(μ[f|m]) x|}
⊢ { val := ↑R, property := (_ : 0 ≤ ↑R) } ≤ ‖(μ[f|m]) x‖₊
[PROOFSTEP]
exact Subtype.mk_le_mk.2 (le_of_lt hx)
[GOAL]
case pos.refine'_3.refine'_2.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ ↑R
hnm : m ≤ m0
hfint : Integrable f
h : 0 < ↑↑μ {x | ↑R < |(μ[f|m]) x|}
⊢ (fun x => |f x|) ≤ᵐ[μ] fun x => ↑R
[PROOFSTEP]
exact hbdd
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
[PROOFSTEP]
have hmeas : ∀ n, ∀ C, MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} := fun n C =>
  measurableSet_le measurable_const (stronglyMeasurable_condexp.mono (hℱ n)).measurable.nnnorm
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
[PROOFSTEP]
have hg : Memℒp g 1 μ := memℒp_one_iff_integrable.2 hint
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
⊢ UniformIntegrable (fun i => μ[g|ℱ i]) 1 μ
[PROOFSTEP]
refine'
  uniformIntegrable_of le_rfl ENNReal.one_ne_top
    (fun n => (stronglyMeasurable_condexp.mono (hℱ n)).aestronglyMeasurable) fun ε hε => _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
by_cases hne : snorm g 1 μ = 0
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : snorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
rw [snorm_eq_zero_iff hg.1 one_ne_zero] at hne 
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : g =ᵐ[μ] 0
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
refine'
  ⟨0, fun n =>
    (le_of_eq <|
          (snorm_eq_zero_iff ((stronglyMeasurable_condexp.mono (hℱ n)).aestronglyMeasurable.indicator (hmeas n 0))
                one_ne_zero).2
            _).trans
      (zero_le _)⟩
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : g =ᵐ[μ] 0
n : ι
⊢ Set.indicator {x | 0 ≤ ‖(μ[g|ℱ n]) x‖₊} (μ[g|ℱ n]) =ᵐ[μ] 0
[PROOFSTEP]
filter_upwards [@condexp_congr_ae _ _ _ _ _ (ℱ n) m0 μ _ _ hne] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : g =ᵐ[μ] 0
n : ι
x : α
hx : (μ[g|ℱ n]) x = (μ[0|ℱ n]) x
⊢ Set.indicator {x | 0 ≤ ‖(μ[g|ℱ n]) x‖₊} (μ[g|ℱ n]) x = OfNat.ofNat 0 x
[PROOFSTEP]
simp only [zero_le', Set.setOf_true, Set.indicator_univ, Pi.zero_apply, hx, condexp_zero]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
obtain ⟨δ, hδ, h⟩ := hg.snorm_indicator_le μ le_rfl ENNReal.one_ne_top hε
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
set C : ℝ≥0 := ⟨δ, hδ.le⟩⁻¹ * (snorm g 1 μ).toNNReal with hC
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
have hCpos : 0 < C := mul_pos (inv_pos.2 hδ) (ENNReal.toNNReal_pos hne hg.snorm_lt_top.ne)
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
have : ∀ n, μ {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ :=
  by
  intro n
  have :=
    mul_meas_ge_le_pow_snorm' μ one_ne_zero ENNReal.one_ne_top
      ((@stronglyMeasurable_condexp _ _ _ _ _ (ℱ n) _ μ g).mono (hℱ n)).aestronglyMeasurable C
  rw [ENNReal.one_toReal, ENNReal.rpow_one, ENNReal.rpow_one, mul_comm, ←
    ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne.symm)) (Or.inl ENNReal.coe_lt_top.ne)] at this 
  simp_rw [ENNReal.coe_le_coe] at this 
  refine' this.trans _
  rw [ENNReal.div_le_iff_le_mul (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne.symm)) (Or.inl ENNReal.coe_lt_top.ne), hC,
    Nonneg.inv_mk, ENNReal.coe_mul, ENNReal.coe_toNNReal hg.snorm_lt_top.ne, ← mul_assoc, ←
    ENNReal.ofReal_eq_coe_nnreal, ← ENNReal.ofReal_mul hδ.le, mul_inv_cancel hδ.ne.symm, ENNReal.ofReal_one, one_mul]
  exact snorm_one_condexp_le_snorm _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
⊢ ∀ (n : ι), ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
n : ι
⊢ ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
[PROOFSTEP]
have :=
  mul_meas_ge_le_pow_snorm' μ one_ne_zero ENNReal.one_ne_top
    ((@stronglyMeasurable_condexp _ _ _ _ _ (ℱ n) _ μ g).mono (hℱ n)).aestronglyMeasurable C
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
n : ι
this : ↑C ^ ENNReal.toReal 1 * ↑↑μ {x | ↑C ≤ ↑‖(μ[g|ℱ n]) x‖₊} ≤ snorm (μ[g|ℱ n]) 1 μ ^ ENNReal.toReal 1
⊢ ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
[PROOFSTEP]
rw [ENNReal.one_toReal, ENNReal.rpow_one, ENNReal.rpow_one, mul_comm, ←
  ENNReal.le_div_iff_mul_le (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne.symm)) (Or.inl ENNReal.coe_lt_top.ne)] at this 
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
n : ι
this : ↑↑μ {x | ↑C ≤ ↑‖(μ[g|ℱ n]) x‖₊} ≤ snorm (μ[g|ℱ n]) 1 μ / ↑C
⊢ ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
[PROOFSTEP]
simp_rw [ENNReal.coe_le_coe] at this 
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
n : ι
this :
  ↑↑μ {x | { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ) ≤ ‖(μ[g|ℱ n]) x‖₊} ≤
    snorm (μ[g|ℱ n]) 1 μ / ↑({ val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ))
⊢ ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
[PROOFSTEP]
refine' this.trans _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
n : ι
this :
  ↑↑μ {x | { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ) ≤ ‖(μ[g|ℱ n]) x‖₊} ≤
    snorm (μ[g|ℱ n]) 1 μ / ↑({ val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ))
⊢ snorm (μ[g|ℱ n]) 1 μ / ↑({ val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)) ≤ ENNReal.ofReal δ
[PROOFSTEP]
rw [ENNReal.div_le_iff_le_mul (Or.inl (ENNReal.coe_ne_zero.2 hCpos.ne.symm)) (Or.inl ENNReal.coe_lt_top.ne), hC,
  Nonneg.inv_mk, ENNReal.coe_mul, ENNReal.coe_toNNReal hg.snorm_lt_top.ne, ← mul_assoc, ← ENNReal.ofReal_eq_coe_nnreal,
  ← ENNReal.ofReal_mul hδ.le, mul_inv_cancel hδ.ne.symm, ENNReal.ofReal_one, one_mul]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
n : ι
this :
  ↑↑μ {x | { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ) ≤ ‖(μ[g|ℱ n]) x‖₊} ≤
    snorm (μ[g|ℱ n]) 1 μ / ↑({ val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ))
⊢ snorm (μ[g|ℱ n]) 1 μ ≤ snorm g 1 μ
[PROOFSTEP]
exact snorm_one_condexp_le_snorm _
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
this : ∀ (n : ι), ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
⊢ ∃ C, ∀ (i : ι), snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ i]) x‖₊} (μ[g|ℱ i])) 1 μ ≤ ENNReal.ofReal ε
[PROOFSTEP]
refine' ⟨C, fun n => le_trans _ (h {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} (hmeas n C) (this n))⟩
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
this : ∀ (n : ι), ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
n : ι
⊢ snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} (μ[g|ℱ n])) 1 μ ≤ snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} g) 1 μ
[PROOFSTEP]
have hmeasℱ : MeasurableSet[ℱ n] {x : α | C ≤ ‖(μ[g|ℱ n]) x‖₊} :=
  @measurableSet_le _ _ _ _ _ (ℱ n) _ _ _ _ _ measurable_const
    (@Measurable.nnnorm _ _ _ _ _ (ℱ n) _ stronglyMeasurable_condexp.measurable)
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
this : ∀ (n : ι), ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
n : ι
hmeasℱ : MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
⊢ snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} (μ[g|ℱ n])) 1 μ ≤ snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} g) 1 μ
[PROOFSTEP]
rw [← snorm_congr_ae (condexp_indicator hint hmeasℱ)]
[GOAL]
case neg.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst✝ : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
hg : Memℒp g 1
ε : ℝ
hε : 0 < ε
hne : ¬snorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h : ∀ (s : Set α), MeasurableSet s → ↑↑μ s ≤ ENNReal.ofReal δ → snorm (Set.indicator s g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hC : C = { val := δ, property := (_ : 0 ≤ δ) }⁻¹ * ENNReal.toNNReal (snorm g 1 μ)
hCpos : 0 < C
this : ∀ (n : ι), ↑↑μ {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} ≤ ENNReal.ofReal δ
n : ι
hmeasℱ : MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊}
⊢ snorm (μ[Set.indicator {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} g|ℱ n]) 1 μ ≤ snorm (Set.indicator {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} g) 1 μ
[PROOFSTEP]
exact snorm_one_condexp_le_snorm _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
⊢ μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]
[PROOFSTEP]
have : ∀ (s c) (f : α → ℝ), Set.indicator s (Function.const α c) * f = s.indicator (c • f) :=
  by
  intro s c f
  ext1 x
  by_cases hx : x ∈ s
  · simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul]; rfl
  · simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_mul]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
⊢ ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
[PROOFSTEP]
intro s c f
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
s : Set α
c : ℝ
f : α → ℝ
⊢ Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
s : Set α
c : ℝ
f : α → ℝ
x : α
⊢ (Set.indicator s (Function.const α c) * f) x = Set.indicator s (c • f) x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
s : Set α
c : ℝ
f : α → ℝ
x : α
hx : x ∈ s
⊢ (Set.indicator s (Function.const α c) * f) x = Set.indicator s (c • f) x
[PROOFSTEP]
simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, Algebra.id.smul_eq_mul]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
s : Set α
c : ℝ
f : α → ℝ
x : α
hx : x ∈ s
⊢ Function.const α c x * f x = c * f x
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
s : Set α
c : ℝ
f : α → ℝ
x : α
hx : ¬x ∈ s
⊢ (Set.indicator s (Function.const α c) * f) x = Set.indicator s (c • f) x
[PROOFSTEP]
simp only [hx, Pi.mul_apply, Set.indicator_of_not_mem, not_false_iff, zero_mul]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
⊢ μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]
[PROOFSTEP]
apply @SimpleFunc.induction _ _ m _ (fun f => _) (fun c s hs => ?_) (fun g₁ g₂ _ h_eq₁ h_eq₂ => ?_) f
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * g|m] =ᵐ[μ]
    ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * μ[g|m]
[PROOFSTEP]
classical simp only [@SimpleFunc.const_zero _ _ m, @SimpleFunc.coe_piecewise _ _ m, @SimpleFunc.coe_const _ _ m,
  @SimpleFunc.coe_zero _ _ m, Set.piecewise_eq_indicator]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * g|m] =ᵐ[μ]
    ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0)) * μ[g|m]
[PROOFSTEP]
simp only [@SimpleFunc.const_zero _ _ m, @SimpleFunc.coe_piecewise _ _ m, @SimpleFunc.coe_const _ _ m,
  @SimpleFunc.coe_zero _ _ m, Set.piecewise_eq_indicator]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[Set.indicator s (Function.const α c) * g|m] =ᵐ[μ] Set.indicator s (Function.const α c) * μ[g|m]
[PROOFSTEP]
rw [this, this]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ μ[Set.indicator s (c • g)|m] =ᵐ[μ] Set.indicator s (c • μ[g|m])
[PROOFSTEP]
refine' (condexp_indicator (hg.smul c) hs).trans _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
⊢ Set.indicator s (μ[c • g|m]) =ᵐ[μ] Set.indicator s (c • μ[g|m])
[PROOFSTEP]
filter_upwards [@condexp_smul α ℝ ℝ _ _ _ _ _ m m0 μ c g] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
x : α
hx : (μ[c • g|m]) x = (c • μ[g|m]) x
⊢ Set.indicator s (μ[c • g|m]) x = Set.indicator s (c • μ[g|m]) x
[PROOFSTEP]
classical simp_rw [Set.indicator_apply, hx]
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
c : ℝ
s : Set α
hs : MeasurableSet s
x : α
hx : (μ[c • g|m]) x = (c • μ[g|m]) x
⊢ Set.indicator s (μ[c • g|m]) x = Set.indicator s (c • μ[g|m]) x
[PROOFSTEP]
simp_rw [Set.indicator_apply, hx]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
⊢ μ[↑(g₁ + g₂) * g|m] =ᵐ[μ] ↑(g₁ + g₂) * μ[g|m]
[PROOFSTEP]
have h_add := @SimpleFunc.coe_add _ _ m _ g₁ g₂
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
h_add : ↑(g₁ + g₂) = ↑g₁ + ↑g₂
⊢ μ[↑(g₁ + g₂) * g|m] =ᵐ[μ] ↑(g₁ + g₂) * μ[g|m]
[PROOFSTEP]
calc
  μ[⇑(g₁ + g₂) * g|m] =ᵐ[μ] μ[(⇑g₁ + ⇑g₂) * g|m] := by refine' condexp_congr_ae (EventuallyEq.mul _ EventuallyEq.rfl);
    rw [h_add]
  _ =ᵐ[μ] μ[⇑g₁ * g|m] + μ[⇑g₂ * g|m] := by rw [add_mul];
    exact condexp_add (hg.simpleFunc_mul' hm _) (hg.simpleFunc_mul' hm _)
  _ =ᵐ[μ] ⇑g₁ * μ[g|m] + ⇑g₂ * μ[g|m] := (EventuallyEq.add h_eq₁ h_eq₂)
  _ =ᵐ[μ] ⇑(g₁ + g₂) * μ[g|m] := by rw [h_add, add_mul]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
h_add : ↑(g₁ + g₂) = ↑g₁ + ↑g₂
⊢ μ[↑(g₁ + g₂) * g|m] =ᵐ[μ] μ[(↑g₁ + ↑g₂) * g|m]
[PROOFSTEP]
refine' condexp_congr_ae (EventuallyEq.mul _ EventuallyEq.rfl)
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
h_add : ↑(g₁ + g₂) = ↑g₁ + ↑g₂
⊢ (fun x => ↑(g₁ + g₂) x) =ᵐ[μ] fun x => (↑g₁ + ↑g₂) x
[PROOFSTEP]
rw [h_add]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
h_add : ↑(g₁ + g₂) = ↑g₁ + ↑g₂
⊢ μ[(↑g₁ + ↑g₂) * g|m] =ᵐ[μ] μ[↑g₁ * g|m] + μ[↑g₂ * g|m]
[PROOFSTEP]
rw [add_mul]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
h_add : ↑(g₁ + g₂) = ↑g₁ + ↑g₂
⊢ μ[↑g₁ * g + ↑g₂ * g|m] =ᵐ[μ] μ[↑g₁ * g|m] + μ[↑g₂ * g|m]
[PROOFSTEP]
exact condexp_add (hg.simpleFunc_mul' hm _) (hg.simpleFunc_mul' hm _)
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : SimpleFunc α ℝ
g : α → ℝ
hg : Integrable g
this : ∀ (s : Set α) (c : ℝ) (f : α → ℝ), Set.indicator s (Function.const α c) * f = Set.indicator s (c • f)
g₁ g₂ : SimpleFunc α ℝ
x✝ : Disjoint (Function.support ↑g₁) (Function.support ↑g₂)
h_eq₁ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₁
h_eq₂ : (fun f => μ[↑f * g|m] =ᵐ[μ] ↑f * μ[g|m]) g₂
h_add : ↑(g₁ + g₂) = ↑g₁ + ↑g₂
⊢ ↑g₁ * μ[g|m] + ↑g₂ * μ[g|m] =ᵐ[μ] ↑(g₁ + g₂) * μ[g|m]
[PROOFSTEP]
rw [h_add, add_mul]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
let fs := hf.approxBounded c
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have hfs_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approxBounded_ae hf_bound
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
by_cases hμ : μ = 0
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : μ = 0
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
simp only [hμ, ae_zero]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : μ = 0
⊢ 0[f * g|m] =ᶠ[⊥] f * 0[g|m]
[PROOFSTEP]
norm_cast
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have : μ.ae.NeBot := by simp only [hμ, ae_neBot, Ne.def, not_false_iff]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
⊢ NeBot (Measure.ae μ)
[PROOFSTEP]
simp only [hμ, ae_neBot, Ne.def, not_false_iff]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have hc : 0 ≤ c :=
  haveI h_exists : ∃ x, ‖f x‖ ≤ c := Eventually.exists hf_bound
  (norm_nonneg _).trans h_exists.choose_spec
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hc : 0 ≤ c
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have hfs_bound : ∀ n x, ‖fs n x‖ ≤ c := hf.norm_approxBounded_le hc
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have : μ[f * μ[g|m]|m] = f * μ[g|m] :=
  by
  refine' condexp_of_stronglyMeasurable hm (hf.mul stronglyMeasurable_condexp) _
  exact integrable_condexp.bdd_mul' (hf.mono hm).aestronglyMeasurable hf_bound
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
⊢ μ[f * μ[g|m]|m] = f * μ[g|m]
[PROOFSTEP]
refine' condexp_of_stronglyMeasurable hm (hf.mul stronglyMeasurable_condexp) _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
⊢ Integrable (f * μ[g|m])
[PROOFSTEP]
exact integrable_condexp.bdd_mul' (hf.mono hm).aestronglyMeasurable hf_bound
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
rw [← this]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ μ[f * g|m] =ᵐ[μ] μ[f * μ[g|m]|m]
[PROOFSTEP]
refine'
  tendsto_condexp_unique (fun n x => fs n x * g x) (fun n x => fs n x * (μ[g|m]) x) (f * g) (f * μ[g|m]) _ _ _ _
    (fun x => c * ‖g x‖) _ (fun x => c * ‖(μ[g|m]) x‖) _ _ _ _
[GOAL]
case neg.refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ (n : ℕ), Integrable ((fun n x => ↑(fs n) x * g x) n)
[PROOFSTEP]
exact fun n =>
  hg.bdd_mul' ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable (eventually_of_forall (hfs_bound n))
[GOAL]
case neg.refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ (n : ℕ), Integrable ((fun n x => ↑(fs n) x * (μ[g|m]) x) n)
[PROOFSTEP]
exact fun n =>
  integrable_condexp.bdd_mul' ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable
    (eventually_of_forall (hfs_bound n))
[GOAL]
case neg.refine'_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => (fun n x => ↑(fs n) x * g x) n x) atTop (𝓝 ((f * g) x))
[PROOFSTEP]
filter_upwards [hfs_tendsto] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
x : α
hx : Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x * g x) atTop (𝓝 ((f * g) x))
[PROOFSTEP]
rw [Pi.mul_apply]
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
x : α
hx : Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x * g x) atTop (𝓝 (f x * g x))
[PROOFSTEP]
exact Tendsto.mul hx tendsto_const_nhds
[GOAL]
case neg.refine'_4
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => (fun n x => ↑(fs n) x * (μ[g|m]) x) n x) atTop (𝓝 ((f * μ[g|m]) x))
[PROOFSTEP]
filter_upwards [hfs_tendsto] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
x : α
hx : Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x * (μ[g|m]) x) atTop (𝓝 ((f * μ[g|m]) x))
[PROOFSTEP]
rw [Pi.mul_apply]
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
x : α
hx : Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(StronglyMeasurable.approxBounded hf c n) x * (μ[g|m]) x) atTop (𝓝 (f x * (μ[g|m]) x))
[PROOFSTEP]
exact Tendsto.mul hx tendsto_const_nhds
[GOAL]
case neg.refine'_5
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ Integrable fun x => c * ‖g x‖
[PROOFSTEP]
exact hg.norm.const_mul c
[GOAL]
case neg.refine'_6
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ Integrable fun x => c * ‖(μ[g|m]) x‖
[PROOFSTEP]
exact integrable_condexp.norm.const_mul c
[GOAL]
case neg.refine'_7
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖(fun n x => ↑(fs n) x * g x) n x‖ ≤ (fun x => c * ‖g x‖) x
[PROOFSTEP]
refine' fun n => eventually_of_forall fun x => _
[GOAL]
case neg.refine'_7
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
x : α
⊢ ‖(fun n x => ↑(fs n) x * g x) n x‖ ≤ (fun x => c * ‖g x‖) x
[PROOFSTEP]
exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (hfs_bound n x) (norm_nonneg _))
[GOAL]
case neg.refine'_8
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖(fun n x => ↑(fs n) x * (μ[g|m]) x) n x‖ ≤ (fun x => c * ‖(μ[g|m]) x‖) x
[PROOFSTEP]
refine' fun n => eventually_of_forall fun x => _
[GOAL]
case neg.refine'_8
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
x : α
⊢ ‖(fun n x => ↑(fs n) x * (μ[g|m]) x) n x‖ ≤ (fun x => c * ‖(μ[g|m]) x‖) x
[PROOFSTEP]
exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (hfs_bound n x) (norm_nonneg _))
[GOAL]
case neg.refine'_9
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ ∀ (n : ℕ), μ[(fun n x => ↑(fs n) x * g x) n|m] =ᵐ[μ] μ[(fun n x => ↑(fs n) x * (μ[g|m]) x) n|m]
[PROOFSTEP]
intro n
[GOAL]
case neg.refine'_9
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
⊢ μ[(fun n x => ↑(fs n) x * g x) n|m] =ᵐ[μ] μ[(fun n x => ↑(fs n) x * (μ[g|m]) x) n|m]
[PROOFSTEP]
simp_rw [← Pi.mul_apply]
[GOAL]
case neg.refine'_9
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
⊢ μ[fun x => (↑(StronglyMeasurable.approxBounded hf c n) * g) x|m] =ᵐ[μ]
    μ[fun x => (↑(StronglyMeasurable.approxBounded hf c n) * μ[g|m]) x|m]
[PROOFSTEP]
refine' (condexp_stronglyMeasurable_simpleFunc_mul hm _ hg).trans _
[GOAL]
case neg.refine'_9
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
⊢ ↑(StronglyMeasurable.approxBounded hf c n) * μ[g|m] =ᵐ[μ]
    μ[fun x => (↑(StronglyMeasurable.approxBounded hf c n) * μ[g|m]) x|m]
[PROOFSTEP]
rw [condexp_of_stronglyMeasurable hm ((SimpleFunc.stronglyMeasurable _).mul stronglyMeasurable_condexp) _]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : StronglyMeasurable f
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
fs : ℕ → SimpleFunc α ℝ := StronglyMeasurable.approxBounded hf c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : NeBot (Measure.ae μ)
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖↑(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
⊢ Integrable (↑(StronglyMeasurable.approxBounded hf c n) * μ[g|m])
[PROOFSTEP]
exact
  integrable_condexp.bdd_mul' ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable
    (eventually_of_forall (hfs_bound n))
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have : μ[f * g|m] =ᵐ[μ] μ[hf.mk f * g|m] := condexp_congr_ae (EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl)
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
refine' this.trans _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
⊢ μ[AEStronglyMeasurable'.mk f hf * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have : f * μ[g|m] =ᵐ[μ] hf.mk f * μ[g|m] := EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ μ[AEStronglyMeasurable'.mk f hf * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
refine' EventuallyEq.trans _ this.symm
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ μ[AEStronglyMeasurable'.mk f hf * g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
[PROOFSTEP]
refine' condexp_stronglyMeasurable_mul_of_bound hm hf.stronglyMeasurable_mk hg c _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ ∀ᵐ (x : α) ∂μ, ‖AEStronglyMeasurable'.mk f hf x‖ ≤ c
[PROOFSTEP]
filter_upwards [hf_bound, hf.ae_eq_mk] with x hxc hx_eq
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
x : α
hxc : ‖f x‖ ≤ c
hx_eq : f x = AEStronglyMeasurable'.mk f hf x
⊢ ‖AEStronglyMeasurable'.mk f hf x‖ ≤ c
[PROOFSTEP]
rw [← hx_eq]
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : IsFiniteMeasure μ
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hg : Integrable g
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
x : α
hxc : ‖f x‖ ≤ c
hx_eq : f x = AEStronglyMeasurable'.mk f hf x
⊢ ‖f x‖ ≤ c
[PROOFSTEP]
exact hxc
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
by_cases hm : m ≤ m0
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : ¬m ≤ m0
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : ¬m ≤ m0
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
simp_rw [condexp_of_not_le hm]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : ¬m ≤ m0
⊢ 0 =ᵐ[μ] f * 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
by_cases hμm : SigmaFinite (μ.trim hm)
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
swap
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
simp_rw [condexp_of_not_sigmaFinite hm hμm]
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm : ¬SigmaFinite (Measure.trim μ hm)
⊢ 0 =ᵐ[μ] f * 0
[PROOFSTEP]
rw [mul_zero]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm : SigmaFinite (Measure.trim μ hm)
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
haveI : SigmaFinite (μ.trim hm) := hμm
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
obtain ⟨sets, sets_prop, h_univ⟩ := hf.exists_spanning_measurableSet_norm_le hm μ
[GOAL]
case pos.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
sets_prop : ∀ (n : ℕ), MeasurableSet (sets n) ∧ ↑↑μ (sets n) < ⊤ ∧ ∀ (x : α), x ∈ sets n → ‖f x‖ ≤ ↑n
h_univ : ⋃ (i : ℕ), sets i = Set.univ
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
simp_rw [forall_and] at sets_prop 
[GOAL]
case pos.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
sets_prop :
  (∀ (x : ℕ), MeasurableSet (sets x)) ∧ (∀ (x : ℕ), ↑↑μ (sets x) < ⊤) ∧ ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
obtain ⟨h_meas, h_finite, h_norm⟩ := sets_prop
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
suffices ∀ n, ∀ᵐ x ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x
  by
  rw [← ae_all_iff] at this 
  filter_upwards [this] with x hx
  rw [Pi.mul_apply]
  obtain ⟨i, hi⟩ : ∃ i, x ∈ sets i :=
    by
    have h_mem : x ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
    simpa using h_mem
  exact hx i hi
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
rw [← ae_all_iff] at this 
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
filter_upwards [this] with x hx
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ (μ[f * g|m]) x = (f * μ[g|m]) x
[PROOFSTEP]
rw [Pi.mul_apply]
[GOAL]
case h
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ (μ[f * g|m]) x = f x * (μ[g|m]) x
[PROOFSTEP]
obtain ⟨i, hi⟩ : ∃ i, x ∈ sets i :=
  by
  have h_mem : x ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
  simpa using h_mem
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ ∃ i, x ∈ sets i
[PROOFSTEP]
have h_mem : x ∈ ⋃ i, sets i := by rw [h_univ]; exact Set.mem_univ _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ x ∈ ⋃ (i : ℕ), sets i
[PROOFSTEP]
rw [h_univ]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
⊢ x ∈ Set.univ
[PROOFSTEP]
exact Set.mem_univ _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
h_mem : x ∈ ⋃ (i : ℕ), sets i
⊢ ∃ i, x ∈ sets i
[PROOFSTEP]
simpa using h_mem
[GOAL]
case h.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), a ∈ sets i → (μ[f * g|m]) a = f a * (μ[g|m]) a
x : α
hx : ∀ (i : ℕ), x ∈ sets i → (μ[f * g|m]) x = f x * (μ[g|m]) x
i : ℕ
hi : x ∈ sets i
⊢ (μ[f * g|m]) x = f x * (μ[g|m]) x
[PROOFSTEP]
exact hx i hi
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ sets n → (μ[f * g|m]) x = f x * (μ[g|m]) x
[PROOFSTEP]
refine' fun n => ae_imp_of_ae_restrict _
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (sets n), (μ[f * g|m]) x = f x * (μ[g|m]) x
[PROOFSTEP]
suffices (μ.restrict (sets n))[f * g|m] =ᵐ[μ.restrict (sets n)] f * (μ.restrict (sets n))[g|m]
  by
  simp_rw [← Pi.mul_apply]
  refine' (condexp_restrict_ae_eq_restrict hm (h_meas n) hfg).symm.trans _
  exact this.trans (EventuallyEq.rfl.mul (condexp_restrict_ae_eq_restrict hm (h_meas n) hg))
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)] f * Measure.restrict μ (sets n)[g|m]
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (sets n), (μ[f * g|m]) x = f x * (μ[g|m]) x
[PROOFSTEP]
simp_rw [← Pi.mul_apply]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)] f * Measure.restrict μ (sets n)[g|m]
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (sets n), (μ[f * g|m]) x = (f * μ[g|m]) x
[PROOFSTEP]
refine' (condexp_restrict_ae_eq_restrict hm (h_meas n) hfg).symm.trans _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)] f * Measure.restrict μ (sets n)[g|m]
⊢ Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)] fun x => (f * μ[g|m]) x
[PROOFSTEP]
exact this.trans (EventuallyEq.rfl.mul (condexp_restrict_ae_eq_restrict hm (h_meas n) hg))
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)] f * Measure.restrict μ (sets n)[g|m]
[PROOFSTEP]
suffices
  (μ.restrict (sets n))[(sets n).indicator f * g|m] =ᵐ[μ.restrict (sets n)]
    (sets n).indicator f * (μ.restrict (sets n))[g|m]
  by
  refine' EventuallyEq.trans _ (this.trans _)
  · exact condexp_congr_ae ((indicator_ae_eq_restrict (hm _ (h_meas n))).symm.mul EventuallyEq.rfl)
  · exact (indicator_ae_eq_restrict (hm _ (h_meas n))).mul EventuallyEq.rfl
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  Measure.restrict μ (sets n)[Set.indicator (sets n) f * g|m] =ᵐ[Measure.restrict μ (sets n)]
    Set.indicator (sets n) f * Measure.restrict μ (sets n)[g|m]
⊢ Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)] f * Measure.restrict μ (sets n)[g|m]
[PROOFSTEP]
refine' EventuallyEq.trans _ (this.trans _)
[GOAL]
case refine'_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  Measure.restrict μ (sets n)[Set.indicator (sets n) f * g|m] =ᵐ[Measure.restrict μ (sets n)]
    Set.indicator (sets n) f * Measure.restrict μ (sets n)[g|m]
⊢ Measure.restrict μ (sets n)[f * g|m] =ᵐ[Measure.restrict μ (sets n)]
    Measure.restrict μ (sets n)[Set.indicator (sets n) f * g|m]
[PROOFSTEP]
exact condexp_congr_ae ((indicator_ae_eq_restrict (hm _ (h_meas n))).symm.mul EventuallyEq.rfl)
[GOAL]
case refine'_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this :
  Measure.restrict μ (sets n)[Set.indicator (sets n) f * g|m] =ᵐ[Measure.restrict μ (sets n)]
    Set.indicator (sets n) f * Measure.restrict μ (sets n)[g|m]
⊢ Set.indicator (sets n) f * Measure.restrict μ (sets n)[g|m] =ᵐ[Measure.restrict μ (sets n)]
    f * Measure.restrict μ (sets n)[g|m]
[PROOFSTEP]
exact (indicator_ae_eq_restrict (hm _ (h_meas n))).mul EventuallyEq.rfl
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ Measure.restrict μ (sets n)[Set.indicator (sets n) f * g|m] =ᵐ[Measure.restrict μ (sets n)]
    Set.indicator (sets n) f * Measure.restrict μ (sets n)[g|m]
[PROOFSTEP]
have : IsFiniteMeasure (μ.restrict (sets n)) := by
  constructor
  rw [Measure.restrict_apply_univ]
  exact h_finite n
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ IsFiniteMeasure (Measure.restrict μ (sets n))
[PROOFSTEP]
constructor
[GOAL]
case measure_univ_lt_top
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ ↑↑(Measure.restrict μ (sets n)) Set.univ < ⊤
[PROOFSTEP]
rw [Measure.restrict_apply_univ]
[GOAL]
case measure_univ_lt_top
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
⊢ ↑↑μ (sets n) < ⊤
[PROOFSTEP]
exact h_finite n
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (Measure.restrict μ (sets n))
⊢ Measure.restrict μ (sets n)[Set.indicator (sets n) f * g|m] =ᵐ[Measure.restrict μ (sets n)]
    Set.indicator (sets n) f * Measure.restrict μ (sets n)[g|m]
[PROOFSTEP]
refine' condexp_stronglyMeasurable_mul_of_bound hm (hf.indicator (h_meas n)) hg.integrableOn n _
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (Measure.restrict μ (sets n))
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ (sets n), ‖Set.indicator (sets n) f x‖ ≤ ↑n
[PROOFSTEP]
refine' eventually_of_forall fun x => _
[GOAL]
case pos.intro.intro.intro.intro
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (Measure.restrict μ (sets n))
x : α
⊢ ‖Set.indicator (sets n) f x‖ ≤ ↑n
[PROOFSTEP]
by_cases hxs : x ∈ sets n
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (Measure.restrict μ (sets n))
x : α
hxs : x ∈ sets n
⊢ ‖Set.indicator (sets n) f x‖ ≤ ↑n
[PROOFSTEP]
simp only [hxs, Set.indicator_of_mem]
[GOAL]
case pos
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (Measure.restrict μ (sets n))
x : α
hxs : x ∈ sets n
⊢ ‖f x‖ ≤ ↑n
[PROOFSTEP]
exact h_norm n x hxs
[GOAL]
case neg
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g)
hg : Integrable g
hm : m ≤ m0
hμm this✝ : SigmaFinite (Measure.trim μ hm)
sets : ℕ → Set α
h_univ : ⋃ (i : ℕ), sets i = Set.univ
h_meas : ∀ (x : ℕ), MeasurableSet (sets x)
h_finite : ∀ (x : ℕ), ↑↑μ (sets x) < ⊤
h_norm : ∀ (x : ℕ) (x_1 : α), x_1 ∈ sets x → ‖f x_1‖ ≤ ↑x
n : ℕ
this : IsFiniteMeasure (Measure.restrict μ (sets n))
x : α
hxs : ¬x ∈ sets n
⊢ ‖Set.indicator (sets n) f x‖ ≤ ↑n
[PROOFSTEP]
simp only [hxs, Set.indicator_of_not_mem, not_false_iff, _root_.norm_zero, Nat.cast_nonneg]
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have : μ[f * g|m] =ᵐ[μ] μ[hf.mk f * g|m] := condexp_congr_ae (EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl)
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
this : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
⊢ μ[f * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
refine' this.trans _
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
this : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
⊢ μ[AEStronglyMeasurable'.mk f hf * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
have : f * μ[g|m] =ᵐ[μ] hf.mk f * μ[g|m] := EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ μ[AEStronglyMeasurable'.mk f hf * g|m] =ᵐ[μ] f * μ[g|m]
[PROOFSTEP]
refine' EventuallyEq.trans _ this.symm
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ μ[AEStronglyMeasurable'.mk f hf * g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
[PROOFSTEP]
refine' condexp_stronglyMeasurable_mul hf.stronglyMeasurable_mk _ hg
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ Integrable (AEStronglyMeasurable'.mk f hf * g)
[PROOFSTEP]
refine' (integrable_congr _).mp hfg
[GOAL]
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : AEStronglyMeasurable' m f μ
hfg : Integrable (f * g)
hg : Integrable g
this✝ : μ[f * g|m] =ᵐ[μ] μ[AEStronglyMeasurable'.mk f hf * g|m]
this : f * μ[g|m] =ᵐ[μ] AEStronglyMeasurable'.mk f hf * μ[g|m]
⊢ f * g =ᵐ[μ] AEStronglyMeasurable'.mk f hf * g
[PROOFSTEP]
exact EventuallyEq.mul hf.ae_eq_mk EventuallyEq.rfl
