awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
h₁ : 0 ≤ 2⁻¹ * r
grw grw₁ :
  2⁻¹ * r * ∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (x • z)‖ ≤
    2⁻¹ * r * ∫ (x : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (x • z)‖
⊢ 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:
grw [intervalIntegral.norm_integral_le_integral_norm hr']

Premises used: intervalIntegral.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
hbc : LE.le (α := ℝ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4)
⊢ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖ ≤ 2⁻¹ * r * ∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
hbc :
  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)
⊢ LE.le (α := ℝ) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ‖1 - f (t • z)‖) (∫ (t : ℝ) in -(2 * r⁻¹)..2 * r⁻¹, ε / 4)

Tactic:
rw [intervalIntegral.integral_of_le hr', intervalIntegral.integral_of_le hr']

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
⊢ ∀ (i : ℕ), Measurable.{u_1, 0} (α := E) (β := ℂ) ((fun (n : ℕ) (t : E) ↦ charFun (μ n) t) i)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
refine : Tendsto (fun (n : ℕ) (t : E) ↦ charFun (μ n) t) atTop (𝓝 f)
⊢ Measurable f

Tactic:
refine measurable_of_tendsto_metrizable (f := fun n t ↦ charFun (μ n) t) (by fun_prop) ?_

Premises used: measurable_of_tendsto_metrizable
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (x : E), Tendsto (fun (i : ℕ) ↦ charFun (μ i) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) (t : E) ↦ charFun (μ n) t) atTop (𝓝 f)

Tactic:
rwa [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
⊢ Measurable f

Tactic:
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]
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
funProp : ‖ε / 4‖ₑ ≠ ∞
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ε / 4)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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⁻¹)))
hbc₁ :
  (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ)
    (fun (x : ℝ) ↦ ‖1 - f (x • z)‖) fun (x : ℝ) ↦ ε / 4
⊢ 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)

Tactic:
refine integral_mono_ae ?_ (by fun_prop) ?_

Premises used: MeasureTheory.integral_mono_ae
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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⁻¹)))

Tactic:
Integrable.mono' (integrable_const (ε / 4)) ?_ ?_

Premises used: MeasureTheory.Integrable.mono', HDiv.hDiv, OfNat.ofNat, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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⁻¹)))
hbc₁ : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖‖1 - f (a • z)‖‖ ≤ ε / 4
⊢ @Integrable ℝ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))

Tactic:
refine Integrable.mono' (integrable_const (ε / 4)) ?_ ?_

Premises used: MeasureTheory.Integrable.mono', HDiv.hDiv, OfNat.ofNat, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ ‖1 - f (x • z)‖

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ ‖1 - f (x • z)‖)
    (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))

Tactic:
exact Measurable.aestronglyMeasurable <| by fun_prop

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)), ‖‖1 - f (a • z)‖‖ ≤ ε / 4

Tactic:
simpa using ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Set.Ioc (-(2 * r⁻¹)) (2 * r⁻¹)))).EventuallyLE (β := ℝ)
    (fun (x : ℝ) ↦ ‖1 - f (x • z)‖) fun (x : ℝ) ↦ ε / 4

Tactic:
ae_restrict_of_forall_mem measurableSet_Ioc h_le_Ioc

Premises used: MeasureTheory.ae_restrict_of_forall_mem, measurableSet_Ioc, Filter.EventuallyLE