-- 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 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]

Tactic:
refine (condExp_stronglyMeasurable_simpleFunc_mul hm _ hg).trans ?_

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 : ℕ
⊢ ⇑(fs n) * μ[g|m] =ᶠ[ae μ] μ[fun x => (⇑(fs n) * μ[g|m]) x|m]

Proof state:
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 α ℝ := 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 ((fun n x => (fs n) x * (μ[g|m]) x) n) μ

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

Result:
no goals

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:
intro n

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 n x => (fs n) x * g x) n|m] =ᶠ[ae μ] μ[(fun n x => (fs n) x * (μ[g|m]) x) n|m]

Proof state:
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 α ℝ := 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 : α) ∂μ, Tendsto (fun n => (fun n x => (fs n) x * (μ[g|m]) x) n x) atTop (𝓝 ((f * μ[g|m]) x))

Tactic:
filter_upwards [hfs_tendsto] with x hx

Result:
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|m]) x) atTop (𝓝 ((f * μ[g|m]) x))

Proof state:
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 α ℝ := 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|m]) x) n x‖ ≤ (fun x => c * ‖(μ[g|m]) x‖) x

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

Result:
no goals

Proof state:
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
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ μ[f * g|m] =ᶠ[ae μ] f * μ[g|m]

Tactic:
rw [← this]

Result:
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
this✝ : (ae μ).NeBot
hc : 0 ≤ c
hfs_bound : ∀ (n : ℕ) (x : α), ‖(fs n) x‖ ≤ c
this : μ[f * μ[g|m]|m] = f * μ[g|m]
⊢ μ[f * g|m] =ᶠ[ae μ] μ[f * μ[g|m]|m]

Proof state:
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 α ℝ := 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 : α) ∂μ, Tendsto (fun n => (fun n x => (fs n) x * g x) n x) atTop (𝓝 ((f * g) x))

Tactic:
filter_upwards [hfs_tendsto] with x hx

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

Proof state:
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
⊢ 0[f * g|m] =ᶠ[⊥] f * 0[g|m]

Tactic:
norm_cast

Result:
no goals