-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem condExp_stronglyMeasurable_mul_of_bound (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ}
    (hf : StronglyMeasurable[m] f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
    μ[f * g|m] =ᵐ[μ] f * μ[g|m]

Proof state:
case intro
α : 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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : (ae μ).NeBot
_x : α
hx : ‖f _x‖ ≤ c
⊢ 0 ≤ c

Tactic:
exact (norm_nonneg _).trans hx

Result:
no goals

Proof state:
α : 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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
⊢ Integrable (⇑(fs n) * μ[g|m]) μ

Tactic:
exact integrable_condExp.bdd_mul'
  ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable
  (Eventually.of_forall (hfs_bound n))

Result:
no goals

Proof state:
α : 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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : (ae μ).NeBot
⊢ 0 ≤ c

Tactic:
rcases hf_bound.exists with ⟨_x, hx⟩

Result:
case intro
α : 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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this : (ae μ).NeBot
_x : α
hx : ‖f _x‖ ≤ c
⊢ 0 ≤ c

Proof state:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
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] =ᶠ[ae μ] μ[(fun n x => (fs n) x * (μ[g|m]) x) n|m]

Tactic:
simp_rw [← Pi.mul_apply]

Result:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
n : ℕ
⊢ μ[fun x => (⇑(fs n) * g) x|m] =ᶠ[ae μ] μ[fun x => (⇑(fs n) * μ[g|m]) x|m]

Proof state:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
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

Tactic:
refine fun n => Eventually.of_forall fun x => ?_

Result:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
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

Proof state:
α : 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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
by_cases hμ : μ = 0

Result:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : μ = 0
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Proof state:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
x : α
hx : Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => (fs n) x * g x) atTop (𝓝 ((f * g) x))

Tactic:
exact hx.mul tendsto_const_nhds

Result:
no goals

Proof state:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
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‖) μ

Tactic:
exact hg.norm.const_mul c

Result:
no goals

Proof state:
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 α ℝ := hf.approxBounded c
hfs_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun x_1 => (fs x_1) x) atTop (𝓝 (f x))
hμ : ¬μ = 0
this✝ : (ae μ).NeBot
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

Tactic:
exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (hfs_bound n x) (norm_nonneg _))

Result:
no goals