awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A
have linarith : A < -A → 2 * (0 - A) + (A - -A) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
linarith : A < -A → 2 * (0 - A) + (A - -A) = 0
⊢ -A ≤ A
have linarith₁ : A < -A → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ^ n ∂μ) (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have M : MeasurableSet (Set.Ioc 0 A)
Tactic: have M : MeasurableSet (Set.Ioc 0 A) := measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ^ n ∂μ) (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have M' : MeasurableSet (Set.Ioc A 0)
Tactic: have M' : MeasurableSet (Set.Ioc A 0) := measurableSet_Ioc
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
⊢ Eq (α := ℝ) (∫ (x : α), truncation f A x ^ n ∂μ) (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have rw : Eq (α := ℝ) (∫ (x : α), ((Set.Ioc 0 A).indicator id ∘ f) x ^ n ∂μ) (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
Tactic: rw [truncation_eq_of_nonneg h'f]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have inl : ∀ (hA : 0 ≤ A),
  Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
Tactic: rcases le_or_gt 0 A with (hA | hA)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
inl :
  ∀ (hA : 0 ≤ A),
    Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
      (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have inr : ∀ (hA : A < 0),
  Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
Tactic: rcases le_or_gt 0 A with (hA | hA)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : 0 ≤ A
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have inl : Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
    (Set.Ioc 0 A).indicator (fun (x : ℝ) ↦ x ^ n) x)
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le hA,
      ← integral_indicator M]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : 0 ≤ A
inl :
  Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc 0 A).indicator (fun (x : ℝ) ↦ x ^ n) x)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have inl₁ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
  (Measure.map f μ)
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le hA,
      ← integral_indicator M]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have inr : Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
  (-@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le,
      ← integral_indicator M']
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
inr :
  Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (-@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
        (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
⊢ Eq (α := ℝ) (∫ (x : α), (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n) (f x) ∂μ)
    (∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ)
have inr₁ : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (z : ℝ) ↦ (Set.Ioc 0 A).indicator id z ^ n)
  (Measure.map f μ)
Tactic: rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le,
      ← integral_indicator M']
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ Eq (α := ℝ) (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (y : ℝ) ↦ (Set.Ioc 0 A).indicator id y ^ n)
    (-@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
        (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
have inr : Eq (α := ℝ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
    (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
  0
Tactic: simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero,
        zero_eq_neg]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map f μ) fun (x : ℝ) ↦
      (Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x)
    0
have inr : (ae (F := Measure ℝ) (Measure.map f μ)).EventuallyEq (β := ℝ) ((Set.Ioc A 0).indicator fun (x : ℝ) ↦ x ^ n) 0
Tactic: apply integral_eq_zero_of_ae
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
⊢ (ae (F := Measure ℝ) (Measure.map f μ)).EventuallyEq (β := ℝ) ((Set.Ioc A 0).indicator fun (x : ℝ) ↦ x ^ n) 0
have this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
Tactic: have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
        (ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
⊢ (ae (F := Measure ℝ) (Measure.map f μ)).EventuallyEq (β := ℝ) ((Set.Ioc A 0).indicator fun (x : ℝ) ↦ x ^ n) 0
have h : ∀ (x : ℝ) (hx : 0 ≤ x), Eq (α := ℝ) ((Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x) (0 x)
Tactic: filter_upwards [this] with x hx
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
⊢ Eq (α := ℝ) ((Set.Ioc A 0).indicator (fun (x : ℝ) ↦ x ^ n) x) (0 x)
have h : A < x → x ≤ 0 → x ^ n = 0
Tactic: simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x
h''x : x ≤ 0
⊢ x = 0
have linarith : x < 0 → 0 - x + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x
h''x : x ≤ 0
linarith : x < 0 → 0 - x + (x - 0) = 0
⊢ x = 0
have linarith₁ : 0 < x → x - 0 + (0 - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
h : A < x
h''x : x ≤ 0
⊢ x ^ n = 0
have this₁ : x = 0
Tactic: have : x = 0 := by linarith
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
⊢ LE.le (α := ℝ) (∫ (x : α), truncation f A x ∂μ) (∫ (x : α), f x ∂μ)
have apply : ∀ (x : α), 0 x ≤ truncation f A x
Tactic: apply integral_mono_of_nonneg
    (Eventually.of_forall fun x => ?_) hf (Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
apply : ∀ (x : α), 0 x ≤ truncation f A x
⊢ LE.le (α := ℝ) (∫ (x : α), truncation f A x ∂μ) (∫ (x : α), f x ∂μ)
have apply₁ : ∀ (x : α), truncation f A x ≤ f x
Tactic: apply integral_mono_of_nonneg
    (Eventually.of_forall fun x => ?_) hf (Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Tendsto (β := ℝ) (fun (A : ℝ) ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))
have refine_1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ
Tactic: refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine_1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ
⊢ Tendsto (β := ℝ) (fun (A : ℝ) ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))
have refine_2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun (x : α) ↦ |f x|) a
Tactic: refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine_1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ
refine_2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun (x : α) ↦ |f x|) a
⊢ Tendsto (β := ℝ) (fun (A : ℝ) ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))
have refine_3 : Integrable (ε := ℝ) (fun (x : α) ↦ |f x|) μ
Tactic: refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
refine_1 : ∀ᶠ (n : ℝ) in atTop, AEStronglyMeasurable (truncation f n) μ
refine_2 : ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun (x : α) ↦ |f x|) a
refine_3 : Integrable (ε := ℝ) (fun (x : α) ↦ |f x|) μ
⊢ Tendsto (β := ℝ) (fun (A : ℝ) ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))
have refine_4 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℝ) ↦ truncation f n a) atTop (𝓝 (f a))
Tactic: refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᶠ (n : ℝ) in atTop, ∀ᵐ (a : α) ∂μ, ‖truncation f n a‖ ≤ (fun (x : α) ↦ |f x|) a
have refine_2 : ∀ (A : ℝ), ∀ᵐ (a : α) ∂μ, ‖truncation f A a‖ ≤ |f a|
Tactic: filter_upwards with A
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
A : ℝ
⊢ ∀ᵐ (a : α) ∂μ, ‖truncation f A a‖ ≤ |f a|
have refine_2 : ∀ (x : α), ‖truncation f A x‖ ≤ |f x|
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℝ) ↦ truncation f n a) atTop (𝓝 (f a))
have refine_4 : ∀ (x : α), Tendsto (fun (n : ℝ) ↦ truncation f n x) atTop (𝓝 (f x))
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ Tendsto (fun (n : ℝ) ↦ truncation f n x) atTop (𝓝 (f x))
have apply : EventuallyEq (β := ℝ) atTop (fun (x_1 : ℝ) ↦ f x) fun (n : ℝ) ↦ truncation f n x
Tactic: apply tendsto_const_nhds.congr' _
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ EventuallyEq (β := ℝ) atTop (fun (x_1 : ℝ) ↦ f x) fun (n : ℝ) ↦ truncation f n x
have h : ∀ (A : ℝ) (hA : A ∈ Set.Ioi |f x|), f x = truncation f A x
Tactic: filter_upwards [Ioi_mem_atTop (abs (f x))] with A hA
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (hypothesis)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
⊢ ∑ j ∈ range K,
      ((ℙ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {ω : Ω | Membership.mem (γ := Set ℝ) (Set.Ioc (↑j : ℝ) (↑N : ℝ)) (X ω)} ≤
    ENNReal.ofReal (HAdd.hAdd (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : Ω) ↦ X a) 1)
have this : IsProbabilityMeasure ρ
Tactic: haveI : IsProbabilityMeasure ρ := Measure.isProbabilityMeasure_map hint.aemeasurable
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ Eq (α := ℝ) (∑ j ∈ range K, ∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ)
    (∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
have apply : ∀ (j : ℕ) (hj : j ∈ range K),
  Eq (α := ℝ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ) (∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
Tactic: apply sum_congr rfl fun j hj => ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
j : ℕ
hj : j ∈ range K
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑j : ℝ)..(↑N : ℝ), 1 ∂ρ) (∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
have rw : ∀ k ∈ Set.Ico j N, IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1) ρ (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: rw [intervalIntegral.sum_integral_adjacent_intervals_Ico ((mem_range.1 hj).le.trans hKN)]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ Eq (α := ℝ) (∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
    (∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in (↑i : ℝ)..(↑(i + 1) : ℝ), 1 ∂ρ)
have simp_rw : Eq (α := ℝ)
  (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N,
    ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
  (∑ x ∈ (range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K),
    ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
Tactic: simp_rw [sum_sigma']
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N,
      ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
    (∑ x ∈ (range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K),
      ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
have refine_1 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
      ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K))
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a)
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
refine_1 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N,
      ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
    (∑ x ∈ (range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K),
      ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
have refine_2 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
      ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K)) a →
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N)
      ((fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        a)
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
inst : MeasureSpace Ω
inst_1 : IsProbabilityMeasure.{u_1} (α := Ω) (m0 := MeasureSpace.toMeasurableSpace) ℙ
X : Ω → ℝ
hint : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
refine_1 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
refine_2 :
  ∀ (a : (_ : ℕ) × ℕ),
    Membership.mem (γ := Finset ((_ : ℕ) × ℕ))
        ((range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K)) a →
      Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N)
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a)
⊢ Eq (α := ℝ)
    (∑ x ∈ (range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N,
      ∫ (x : ℝ) in (↑(x.snd (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.snd (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
    (∑ x ∈ (range N).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ range (min (a + 1) K),
      ∫ (x : ℝ) in (↑(x.fst (β := fun (i : ℕ) ↦ ℕ)) : ℝ)..(↑(x.fst (β := fun (i : ℕ) ↦ ℕ) + 1) : ℝ), 1 ∂ρ)
have refine_3 : ∀ (a : (_ : ℕ) × ℕ),
  Membership.mem (γ := Finset ((_ : ℕ) × ℕ)) ((range K).sigma (α := fun (a : ℕ) ↦ ℕ) fun (a : ℕ) ↦ Ico a N) a →
    (fun (p : (_ : ℕ) × ℕ) ↦
          (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) : (_ : ℕ) × ℕ))
        ((fun (p : (_ : ℕ) × ℕ) ↦
            (Sigma.mk (β := fun (i : ℕ) ↦ ℕ) (p.snd (β := fun (i : ℕ) ↦ ℕ)) (p.fst (β := fun (i : ℕ) ↦ ℕ)) :
              (_ : ℕ) × ℕ))
          a) =
      a
Tactic: refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_