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))
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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
hf_meas : Measurable f
hbc :
  @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
⊢ LE.le (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (x : ℝ) ↦
      ‖1 - f (x • z)‖)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹))) fun (x : ℝ) ↦
      ε / 4)
have hbc₁ : (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ)
  (fun (x : ℝ) ↦ ‖1 - f (x • z)‖) fun (x : ℝ) ↦ ε / 4
Tactic: refine integral_mono_ae ?_ (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))
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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
hf_meas : Measurable f
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
have hbc : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
  (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
Tactic: refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
-- 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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
hf_meas : Measurable f
hbc :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))
have hbc₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖‖1 - f (a • z)‖‖ ≤ ε / 4
Tactic: refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
-- 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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 = ε / 2
have simp : 2⁻¹ * r * ((2 * r⁻¹ + 2 * r⁻¹) * ε / 4) = ε / 2
Tactic: simp
-- 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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
⊢ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) < ε
have calc : 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) ≤
  2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖
Tactic: calc 2⁻¹ * r * ‖∫ t in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ := by
    grw [intervalIntegral.norm_integral_le_integral_norm hr']
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 := by
    gcongr
    rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
    have hf_meas : Measurable f := by
      refine measurable_of_tendsto_metrizable (f := fun n t ↦ charFun (μ n) t) (by fun_prop) ?_
      rwa [tendsto_pi_nhds]
    refine integral_mono_ae ?_ (by fun_prop) ?_
    · refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
      · exact Measurable.aestronglyMeasurable <| by fun_prop
      · simpa using ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
    · exact ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
  _ = ε / 2 := by simp; field
  _ < ε := by simp [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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
calc :
  2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖
⊢ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) < ε
have calc₁ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ ≤ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4
Tactic: calc 2⁻¹ * r * ‖∫ t in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ := by
    grw [intervalIntegral.norm_integral_le_integral_norm hr']
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 := by
    gcongr
    rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
    have hf_meas : Measurable f := by
      refine measurable_of_tendsto_metrizable (f := fun n t ↦ charFun (μ n) t) (by fun_prop) ?_
      rwa [tendsto_pi_nhds]
    refine integral_mono_ae ?_ (by fun_prop) ?_
    · refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
      · exact Measurable.aestronglyMeasurable <| by fun_prop
      · simpa using ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
    · exact ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
  _ = ε / 2 := by simp; field
  _ < ε := by simp [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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
calc :
  2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖
calc₁ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ ≤ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4
⊢ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) < ε
have calc₂ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 = ε / 2
Tactic: calc 2⁻¹ * r * ‖∫ t in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ := by
    grw [intervalIntegral.norm_integral_le_integral_norm hr']
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 := by
    gcongr
    rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
    have hf_meas : Measurable f := by
      refine measurable_of_tendsto_metrizable (f := fun n t ↦ charFun (μ n) t) (by fun_prop) ?_
      rwa [tendsto_pi_nhds]
    refine integral_mono_ae ?_ (by fun_prop) ?_
    · refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
      · exact Measurable.aestronglyMeasurable <| by fun_prop
      · simpa using ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
    · exact ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
  _ = ε / 2 := by simp; field
  _ < ε := by simp [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))
ε : ℝ
hε : ε > 0
hf0 : f 0 = 1
hf_tendsto : ∀ (ε : ℝ), 0 < ε → ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε
δ : ℝ
hδ : 0 < δ
hδ_lt : ∀ ⦃x : E⦄, ‖x‖ < δ → ‖1 - f x‖ < ε / 4
r : ℝ
hrδ : 4 * δ⁻¹ ≤ r
hr : 0 < r
hr' : -(2 * r⁻¹) ≤ 2 * r⁻¹
h_le_Ioc : ∀ (x : ℝ) (hx : x ∈ Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖1 - f (x • z)‖ ≤ ε / 4
calc :
  2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) ≤
    2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖
calc₁ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ ≤ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4
calc₂ : 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 = ε / 2
⊢ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)) < ε
have calc₃ : ε / 2 < ε
Tactic: calc 2⁻¹ * r * ‖∫ t in -(2 * r⁻¹)..2 * r⁻¹, 1 - f (t • z)‖
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ := by
    grw [intervalIntegral.norm_integral_le_integral_norm hr']
  _ ≤ 2⁻¹ * r * ∫ t in -(2 * r⁻¹)..2 * r⁻¹, ε / 4 := by
    gcongr
    rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']
    have hf_meas : Measurable f := by
      refine measurable_of_tendsto_metrizable (f := fun n t ↦ charFun (μ n) t) (by fun_prop) ?_
      rwa [tendsto_pi_nhds]
    refine integral_mono_ae ?_ (by fun_prop) ?_
    · refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_
      · exact Measurable.aestronglyMeasurable <| by fun_prop
      · simpa using ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
    · exact ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc
  _ = ε / 2 := by simp; field
  _ < ε := by simp [hε]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
⊢ Tendsto μ 𝓕 (𝓝 μ₀)
have inl : ∀
  (hμ :
    ∀ g ∈ A,
      Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ⊥
        (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))),
  Tendsto μ ⊥ (𝓝 μ₀)
Tactic: obtain rfl | _ := 𝓕.eq_or_neBot
Cleared hypotheses: 𝓕, hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
inl :
  ∀
    (hμ :
      ∀ g ∈ A,
        Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ⊥
          (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))),
    Tendsto μ ⊥ (𝓝 μ₀)
⊢ Tendsto μ 𝓕 (𝓝 μ₀)
have inr : 𝓕.NeBot → Tendsto μ 𝓕 (𝓝 μ₀)
Tactic: obtain rfl | _ := 𝓕.eq_or_neBot
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
⊢ Tendsto μ 𝓕 (𝓝 μ₀)
have inr : ∀ (U : Ultrafilter ι) (hU : (↑U : Filter ι) ≤ 𝓕), Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
Tactic: refine (Filter.tendsto_iff_ultrafilter _ _ _).2 fun U hU ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (hypothesis)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
have h_compact : IsCompact.{u_3} (X := ProbabilityMeasure E)
  (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
Tactic: have h_compact : IsCompact (closure {μ n | n}) :=
    isCompact_closure_of_isTightMeasureSet (by simpa using h_tight)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
have inr : ∀ (μ' : ProbabilityMeasure E) (hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')), Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
Tactic: obtain ⟨μ', -, hμ' : Tendsto _ _ _⟩ := h_compact.ultrafilter_le_nhds (U.map μ)
    (.trans (by simp) (monotone_principal subset_closure))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
ι : Type u_4
𝓕 : Filter ι
μ : ι → ProbabilityMeasure E
h_tight : IsTightMeasureSet.{u_3} (𝓧 := E) (m𝓧 := inst_1) {x : Measure E | ∃ (n : ι), (↑(μ n) : Measure E) = x}
μ₀ : ProbabilityMeasure E
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_3, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
hμ :
  ∀ g ∈ A,
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ₀ : Measure E)))
this_1 : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
h : 𝓕.NeBot
U : Ultrafilter ι
hU : (↑U : Filter ι) ≤ 𝓕
h_compact :
  IsCompact.{u_3} (X := ProbabilityMeasure E)
    (closure[instTopologicalSpace] {x : ProbabilityMeasure E | ∃ (n : ι), μ n = x})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
this : (↑μ' : Measure E) = (↑μ₀ : Measure E)
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
have h : μ₀ = μ'
Tactic: convert! hμ'