-- Mathlib/Probability/StrongLaw.lean
theorem tendsto_integral_truncation {f : α → ℝ} (hf : Integrable f μ) :
    Tendsto (fun A => ∫ x, truncation f A x ∂μ) atTop (𝓝 (∫ x, f x ∂μ))

Proof state:
case refine_4.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ Tendsto (fun n => truncation f n x) atTop (𝓝 (f x))

Tactic:
apply tendsto_const_nhds.congr' _

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ (fun x_1 => f x) =ᶠ[atTop] fun n => truncation f n x

Proof state:
case refine_2.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ ‖truncation f A x‖ ≤ |f x|

Tactic:
rw [Real.norm_eq_abs]

Result:
case refine_2.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Tendsto (fun A => ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun x => |f x|) a

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x => |f x|) μ

case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => truncation f n a) atTop (𝓝 (f a))

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ

Tactic:
exact Eventually.of_forall fun A ↦ hf.aestronglyMeasurable.truncation

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun x => |f x|) a

Tactic:
filter_upwards with A

Result:
case refine_2.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
⊢ ∀ᵐ (a : α) ∂μ, ‖truncation f A a‖ ≤ |f a|

Proof state:
case refine_2.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
⊢ ∀ᵐ (a : α) ∂μ, ‖truncation f A a‖ ≤ |f a|

Tactic:
filter_upwards with x

Result:
case refine_2.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ ‖truncation f A x‖ ≤ |f x|

Proof state:
case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => truncation f n a) atTop (𝓝 (f a))

Tactic:
filter_upwards with x

Result:
case refine_4.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ Tendsto (fun n => truncation f n x) atTop (𝓝 (f x))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ (fun x_1 => f x) =ᶠ[atTop] fun n => truncation f n x

Tactic:
filter_upwards [Ioi_mem_atTop (abs (f x))] with A hA

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
A : ℝ
hA : A ∈ Set.Ioi |f x|
⊢ f x = truncation f A x

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Integrable (fun x => |f x|) μ

Tactic:
exact hf.abs

Result:
no goals

Proof state:
case refine_2.h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
exact abs_truncation_le_abs_self _ _ _

Result:
no goals

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
A : ℝ
hA : A ∈ Set.Ioi |f x|
⊢ f x = truncation f A x

Tactic:
exact (truncation_eq_self hA).symm

Result:
no goals