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 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
⊢ ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))

Tactic:
have h_eq (μ : Measure E) (hμ : IsProbabilityMeasure μ) :
      ∫ x, g x ∂μ = ∑ a ∈ w.support, w a * ∫ x, (probChar (innerₗ E x a) : ℂ) ∂μ := by
    simp_rw [hw]
    rw [integral_finsetSum]
    · congr with y
      rw [integral_const_mul]
    · refine fun i hi ↦ Integrable.const_mul ?_ _
      change Integrable (innerProbChar i) μ
      exact BoundedContinuousFunction.integrable μ _
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
h_eq :
  ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))
simp_rw :
  Tendsto (β := ℂ)
    (fun (n : ι) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑(μ n) : Measure E) :
            ℂ))
    𝓕
    (𝓝
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑μ₀ : Measure E) :
            ℂ)))
⊢ Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
    (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))

Tactic:
simp_rw [h_eq (μ _), h_eq μ₀]

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
h_eq :
  ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))
⊢ Tendsto (β := ℂ)
    (fun (n : ι) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑(μ n) : Measure E) :
            ℂ))
    𝓕
    (𝓝
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑μ₀ : Measure E) :
            ℂ)))

Tactic:
tendsto_finsetSum _ fun y hy ↦ Tendsto.const_mul _ ?_

Premises used: Filter.Tendsto.const_mul, tendsto_finsetSum, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
h_eq :
  ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))
refine :
  ∀ (y : E) (hy : y ∈ w.support),
    Tendsto (β := ℂ)
      (fun (n : ι) ↦
        ∫ (x : E),
          (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
            ℂ) ∂(↑(μ n) : Measure E))
      𝓕
      (𝓝
        (∫ (x : E),
          (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
            ℂ) ∂(↑μ₀ : Measure E)))
⊢ Tendsto (β := ℂ)
    (fun (n : ι) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑(μ n) : Measure E) :
            ℂ))
    𝓕
    (𝓝
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂(↑μ₀ : Measure E) :
            ℂ)))

Tactic:
refine tendsto_finsetSum _ fun y hy ↦ Tendsto.const_mul _ ?_

Premises used: Filter.Tendsto.const_mul, tendsto_finsetSum
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
ι : Type u_2
𝓕 : Filter ι
μ₀ : ProbabilityMeasure E
μ : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ n) : Measure E) t) 𝓕 (𝓝 (charFun (↑μ₀ : Measure E) t))
g : E →ᵇ ℂ
w : AddMonoidAlgebra ℂ E
hw :
  Eq (α := (a : E) → ℂ) (⇑g : (a : E) → ℂ) fun (x : E) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
            ℂ) :
          ℂ)
h_eq :
  ∀ (μ : Measure E) (hμ : IsProbabilityMeasure μ),
    Eq (α := ℂ) (∫ (x : E), (g : (a : E) → ℂ) x ∂μ)
      (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
          (∫ (x : E),
              (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
                ℂ) ∂μ :
            ℂ))
y : E
hy : y ∈ w.support
⊢ Tendsto (β := ℂ)
    (fun (n : ι) ↦
      ∫ (x : E),
        (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
          ℂ) ∂(↑(μ n) : Measure E))
    𝓕
    (𝓝
      (∫ (x : E),
        (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
          ℂ) ∂(↑μ₀ : Measure E)))

Tactic:
simpa [← charFun_eq_integral_probChar] using h y

Premises used: MeasureTheory.charFun_eq_integral_probChar
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
⊢ ContinuousAt (charFun (↑μ₀ : Measure E)) 0

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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
⊢ IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}

Tactic:
have h_tight : IsTightMeasureSet (𝓧 := E) {μ n | n} :=
    isTightMeasureSet_of_tendsto_charFun (by fun_prop) h
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ Tendsto μ atTop (𝓝 μ₀)

Tactic:
tendsto_of_tight_of_separatesPoints h_tight (𝕜 := ℂ)
    (A := charPoly continuous_probChar (L := innerₗ E) continuous_inner) ?_ ?_

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints, Complex
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
refine_1 :
  Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E) (A := ℂ)
    (StarSubalgebra.toSubalgebra
      (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯)))
refine_2 :
  ∀ (g : E →ᵇ ℂ),
    Membership.mem (γ := StarSubalgebra ℂ (E →ᵇ ℂ)) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯) g →
      Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) atTop
        (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
⊢ Tendsto μ atTop (𝓝 μ₀)

Tactic:
refine tendsto_of_tight_of_separatesPoints h_tight (𝕜 := ℂ)
    (A := charPoly continuous_probChar (L := innerₗ E) continuous_inner) ?_ ?_

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints, Complex
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E) (A := ℂ)
    (StarSubalgebra.toSubalgebra
      (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯)))

Tactic:
separatesPoints_charPoly continuous_probChar probChar_ne_one _ ?_

Premises used: Real.continuous_probChar, Real.probChar_ne_one, BoundedContinuousFunction.separatesPoints_charPoly
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
refine_1 :
  ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)
⊢ Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E) (A := ℂ)
    (StarSubalgebra.toSubalgebra
      (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯)))

Tactic:
refine separatesPoints_charPoly continuous_probChar probChar_ne_one _ ?_

Premises used: Real.continuous_probChar, Real.probChar_ne_one, BoundedContinuousFunction.separatesPoints_charPoly
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)

Tactic:
fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩

Premises used: Iff.mpr, inner_self_ne_zero, DFunLike.ne_iff, Exists.intro
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ ∀ (v : E),
    v ≠ 0 → Ne (α := E →ₗ[ℝ] ℝ) (((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) v : E →ₗ[ℝ] ℝ) (0 : E →ₗ[ℝ] ℝ)

Tactic:
exact fun v hv ↦ DFunLike.ne_iff.mpr ⟨v, inner_self_ne_zero.mpr hv⟩

Premises used: Iff.mpr, DFunLike.ne_iff, Exists.intro
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ ∀ (g : E →ᵇ ℂ),
    Membership.mem (γ := StarSubalgebra ℂ (E →ᵇ ℂ)) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯) g →
      Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) atTop
        (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))

Tactic:
fun g ↦ tendsto_charPoly_of_tendsto_charFun h

Premises used: Set.Mem, MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
h_tight : IsTightMeasureSet.{u_1} (𝓧 := E) (m𝓧 := inst_3) {x : Measure E | ∃ (n : ℕ), (↑(μ n) : Measure E) = x}
⊢ ∀ (g : E →ᵇ ℂ),
    Membership.mem (γ := StarSubalgebra ℂ (E →ᵇ ℂ)) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯) g →
      Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) atTop
        (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))

Tactic:
exact fun g ↦ tendsto_charPoly_of_tendsto_charFun h

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_charPoly_of_tendsto_charFun
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
⊢ Tendsto μ atTop (𝓝 μ₀) ↔
    ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))

Tactic:
⟨fun h t ↦ ?_, tendsto_of_tendsto_charFun⟩

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun, Iff.intro
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
refine :
  ∀ (h : Tendsto μ atTop (𝓝 μ₀)) (t : E),
    Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
⊢ Tendsto μ atTop (𝓝 μ₀) ↔
    ∀ (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))

Tactic:
refine ⟨fun h t ↦ ?_, tendsto_of_tendsto_charFun⟩
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h : Tendsto μ atTop (𝓝 μ₀)
t : E
rw :
  ∀
    (h :
      ∀ (f : E →ᵇ ℂ),
        Tendsto (β := ℂ) (fun (i : ℕ) ↦ ∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑(μ i) : Measure E)) atTop
          (𝓝 (∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑μ₀ : Measure E))))
    (t : E), Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))
⊢ Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto ℂ] at h

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto, Complex
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h :
  ∀ (f : E →ᵇ ℂ),
    Tendsto (β := ℂ) (fun (i : ℕ) ↦ ∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑(μ i) : Measure E)) atTop
      (𝓝 (∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑μ₀ : Measure E)))
t : E
simp_rw :
  Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑(μ n) : Measure E)) atTop
    (𝓝 (∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑μ₀ : Measure E)))
⊢ Tendsto (fun (n : ℕ) ↦ charFun (↑(μ n) : Measure E) t) atTop (𝓝 (charFun (↑μ₀ : Measure E) t))

Tactic:
simp_rw [charFun_eq_integral_innerProbChar]

Premises used: MeasureTheory.charFun_eq_integral_innerProbChar
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h :
  ∀ (f : E →ᵇ ℂ),
    Tendsto (β := ℂ) (fun (i : ℕ) ↦ ∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑(μ i) : Measure E)) atTop
      (𝓝 (∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑μ₀ : Measure E)))
t : E
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑(μ n) : Measure E)) atTop
    (𝓝 (∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑μ₀ : Measure E)))

Tactic:
h (innerProbChar t)

Premises used: BoundedContinuousFunction.innerProbChar
-- 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
μ₀ : ProbabilityMeasure E
μ : ℕ → ProbabilityMeasure E
h :
  ∀ (f : E →ᵇ ℂ),
    Tendsto (β := ℂ) (fun (i : ℕ) ↦ ∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑(μ i) : Measure E)) atTop
      (𝓝 (∫ (ω : E), (f : (a : E) → ℂ) ω ∂(↑μ₀ : Measure E)))
t : E
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ ∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑(μ n) : Measure E)) atTop
    (𝓝 (∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂(↑μ₀ : Measure E)))

Tactic:
exact h (innerProbChar t)

Premises used: BoundedContinuousFunction.innerProbChar
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
pos :
  ∀ (ε_top : ε₂ = ∞),
    (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
neg :
  ∀ (ε_top : ¬ε₂ = ∞),
    (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂

Tactic:
by_cases ε_top : ε₂ = ∞
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
ε_top : ε₂ = ∞
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂

Tactic:
simp only [ε_top, toReal_top,
                add_top, le_top]

Premises used: add_top, le_top, ENNReal.toReal_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
ε₁ ε₂ : ℝ≥0∞
μ ν : Measure Ω
h_le : ε₁ ≤ ε₂
B : Set Ω
hε₁ : (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞) ε₁
ε_top : ¬ε₂ = ∞
apply :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₁.toReal B) : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) B ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε₂.toReal B) : ℝ≥0∞) ε₂

Tactic:
apply hε₁.trans (add_le_add ?_ h_le)

Premises used: add_le_add, LE.le.trans