awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) atTop
    (𝓝 (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)))
have simp : Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - charFun (μ n) (t • z)) atTop
  (𝓝 (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)))
Tactic: simp only [neg_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
⊢ -(2 * r⁻¹) ≤ 2 * r⁻¹
have rw : 0 ≤ 2 * r⁻¹
Tactic: rw [neg_le_self_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - charFun (μ n) (t • z)) atTop
    (𝓝 (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)))
have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
Tactic: have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹ := by rw [neg_le_self_iff]; positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - charFun (μ n) (t • z)) atTop
    (𝓝 (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)))
have simp_rw : Tendsto (β := ℂ)
  (fun (n : ℕ) ↦
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
      1 - charFun (μ n) (t • z))
  atTop
  (𝓝
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
      1 - f (t • z)))
Tactic: simp_rw [intervalIntegral.integral_of_le hr']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ 2) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
have funProp : enorm (E := ℝ) 2 ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
⊢ Tendsto (β := ℂ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
        1 - charFun (μ n) (t • z))
    atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
        1 - f (t • z)))
have refine_1 : ∀ (n : ℕ),
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ 1 - charFun (μ n) (t • z))
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
Tactic: refine tendsto_integral_of_dominated_convergence (fun _ ↦ 2) ?_ (by fun_prop) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
refine_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ 1 - charFun (μ n) (t • z))
      (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
⊢ Tendsto (β := ℂ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
        1 - charFun (μ n) (t • z))
    atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
        1 - f (t • z)))
have refine_2 : ∀ (n : ℕ),
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)),
    ‖1 - charFun (μ n) (a • z)‖ ≤ (fun (x : ℝ) ↦ (2 : ℝ)) a
Tactic: refine tendsto_integral_of_dominated_convergence (fun _ ↦ 2) ?_ (by fun_prop) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
refine_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ 1 - charFun (μ n) (t • z))
      (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
refine_2 :
  ∀ (n : ℕ),
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)),
      ‖1 - charFun (μ n) (a • z)‖ ≤ (fun (x : ℝ) ↦ (2 : ℝ)) a
⊢ Tendsto (β := ℂ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
        1 - charFun (μ n) (t • z))
    atTop
    (𝓝
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (t : ℝ) ↦
        1 - f (t • z)))
have refine_3 : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)),
  Tendsto (fun (n : ℕ) ↦ 1 - charFun (μ n) (a • z)) atTop (𝓝 (1 - f (a • z)))
Tactic: refine tendsto_integral_of_dominated_convergence (fun _ ↦ 2) ?_ (by fun_prop) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
⊢ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
have calc : LE.le (α := ℝ) (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop)
  (limsup (fun (n : ℕ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)))
    atTop)
Tactic: calc limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop
    _ ≤ limsup (fun n ↦ 2⁻¹ * r
        * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖) atTop := by
      refine limsup_le_limsup (.of_forall fun n ↦ h_le n r hr) ?_ ?_
      · exact IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ ENNReal.toReal_nonneg
      · refine ⟨4, ?_⟩
        simp only [eventually_map, eventually_atTop, ge_iff_le]
        exact ⟨0, fun n _ ↦ h_le_4 n r hr⟩
    _ = 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖ := by
      refine ((Tendsto.norm ?_).const_mul _).limsup_eq
      simp only [neg_mul]
      have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹ := by rw [neg_le_self_iff]; positivity
      simp_rw [intervalIntegral.integral_of_le hr']
      refine tendsto_integral_of_dominated_convergence (fun _ ↦ 2) ?_ (by fun_prop) ?_ ?_
      · exact fun _ ↦ Measurable.aestronglyMeasurable <| by fun_prop
      · exact fun _ ↦ ae_of_all _ fun _ ↦ norm_one_sub_charFun_le_two
      · exact ae_of_all _ fun _ ↦ tendsto_const_nhds.sub (h _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
r : ℝ
hr : 0 < r
calc :
  LE.le (α := ℝ) (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop)
    (limsup (fun (n : ℕ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)))
      atTop)
⊢ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
have calc₁ : limsup (fun (n : ℕ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))) atTop =
  2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
Tactic: calc limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop
    _ ≤ limsup (fun n ↦ 2⁻¹ * r
        * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖) atTop := by
      refine limsup_le_limsup (.of_forall fun n ↦ h_le n r hr) ?_ ?_
      · exact IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ ENNReal.toReal_nonneg
      · refine ⟨4, ?_⟩
        simp only [eventually_map, eventually_atTop, ge_iff_le]
        exact ⟨0, fun n _ ↦ h_le_4 n r hr⟩
    _ = 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖ := by
      refine ((Tendsto.norm ?_).const_mul _).limsup_eq
      simp only [neg_mul]
      have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹ := by rw [neg_le_self_iff]; positivity
      simp_rw [intervalIntegral.integral_of_le hr']
      refine tendsto_integral_of_dominated_convergence (fun _ ↦ 2) ?_ (by fun_prop) ?_ ?_
      · exact fun _ ↦ Measurable.aestronglyMeasurable <| by fun_prop
      · exact fun _ ↦ ae_of_all _ fun _ ↦ norm_one_sub_charFun_le_two
      · exact ae_of_all _ fun _ ↦ tendsto_const_nhds.sub (h _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
⊢ Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
have h_limsup_le : ∀ (r : ℝ) (hr : 0 < r),
  limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
Tactic: have h_limsup_le r (hr : 0 < r) :
      limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop
        ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖ := by
    calc limsup (fun n ↦ (μ n).real {x | r < |⟪z, x⟫|}) atTop
    _ ≤ limsup (fun n ↦ 2⁻¹ * r
        * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)‖) atTop := by
      refine limsup_le_limsup (.of_forall fun n ↦ h_le n r hr) ?_ ?_
      · exact IsCoboundedUnder.of_frequently_ge <| .of_forall fun _ ↦ ENNReal.toReal_nonneg
      · refine ⟨4, ?_⟩
        simp only [eventually_map, eventually_atTop, ge_iff_le]
        exact ⟨0, fun n _ ↦ h_le_4 n r hr⟩
    _ = 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖ := by
      refine ((Tendsto.norm ?_).const_mul _).limsup_eq
      simp only [neg_mul]
      have hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹ := by rw [neg_le_self_iff]; positivity
      simp_rw [intervalIntegral.integral_of_le hr']
      refine tendsto_integral_of_dominated_convergence (fun _ ↦ 2) ?_ (by fun_prop) ?_ ?_
      · exact fun _ ↦ Measurable.aestronglyMeasurable <| by fun_prop
      · exact fun _ ↦ ae_of_all _ fun _ ↦ norm_one_sub_charFun_le_two
      · exact ae_of_all _ fun _ ↦ tendsto_const_nhds.sub (h _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
⊢ Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
have refine_1 : Tendsto (β := ℝ) (fun (r : ℝ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))) atTop
  (𝓝 0)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (h := fun r ↦ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
refine_1 :
  Tendsto (β := ℝ) (fun (r : ℝ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))) atTop
    (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
have refine_2 : ∀ᶠ (b : ℝ) in atTop, LE.le (α := ℝ) 0 (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | b < ‖⟪z, x⟫‖}) atTop)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (h := fun r ↦ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
refine_1 :
  Tendsto (β := ℝ) (fun (r : ℝ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))) atTop
    (𝓝 0)
refine_2 : ∀ᶠ (b : ℝ) in atTop, LE.le (α := ℝ) 0 (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | b < ‖⟪z, x⟫‖}) atTop)
⊢ Tendsto (β := ℝ) (fun (r : ℝ) ↦ limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop) atTop (𝓝 0)
have refine_3 : ∀ᶠ (b : ℝ) in atTop,
  LE.le (α := ℝ) (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | b < ‖⟪z, x⟫‖}) atTop)
    ((fun (r : ℝ) ↦ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))) b)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (h := fun r ↦ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z)‖) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
⊢ ∀ᶠ (b : ℝ) in atTop, LE.le (α := ℝ) 0 (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | b < ‖⟪z, x⟫‖}) atTop)
have h₁ : ∀ (r : ℝ) (hr : 0 < r), LE.le (α := ℝ) 0 (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop)
Tactic: filter_upwards [eventually_gt_atTop 0] with r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : ℕ → Measure E
inst_5 : ∀ (i : ℕ), IsProbabilityMeasure (μ i)
f : E → ℂ
hf : ContinuousAt f 0
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (μ n) t) atTop (𝓝 (f t))
z : E
hz : ‖z‖ = 1
h_le_4 :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z)) ≤ 4
h_le :
  ∀ (n : ℕ) (r : ℝ) (hr : 0 < r),
    (μ n).real {x : E | r < |⟪z, x⟫|} ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun (μ n) (t • z))
h_limsup_le :
  ∀ (r : ℝ) (hr : 0 < r),
    limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < |⟪z, x⟫|}) atTop ≤
      2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - f (t • z))
r : ℝ
hr : 0 < r
⊢ LE.le (α := ℝ) 0 (limsup (fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}) atTop)
have h₁ : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ (μ n).real {x : E | r < ‖⟪z, x⟫‖}
Tactic: refine le_limsup_of_le ?_ fun u hu ↦ ?_