awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
⊢ (↑μ' : Measure E) = (↑μ₀ : Measure E)

Tactic:
ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable hA
    fun g hg ↦ tendsto_nhds_unique ?_ ((hμ g hg).comp hU)

Premises used: MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable, Filter.Tendsto.comp, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
inr :
  ∀ (g : E →ᵇ 𝕜) (hg : g ∈ A),
    Tendsto.{u_4, u_2} (α := ι) (β := 𝕜)
      ((fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ∘ fun (x : ι) ↦ x) U.1
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ' : Measure E)))
⊢ (↑μ' : Measure E) = (↑μ₀ : Measure E)

Tactic:
refine ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable hA
    fun g hg ↦ tendsto_nhds_unique ?_ ((hμ g hg).comp hU)

Premises used: MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable, Filter.Tendsto.comp, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
g : E →ᵇ 𝕜
hg : g ∈ A
inr :
  ∀
    (hμ' :
      ∀ (f : E →ᵇ 𝕜),
        Tendsto.{u_4, u_2} (β := 𝕜) (fun (i : ι) ↦ ∫ (ω : E), (f : (a : E) → 𝕜) ω ∂(↑(μ i) : Measure E)) (↑U : Filter ι)
          (𝓝 (∫ (ω : E), (f : (a : E) → 𝕜) ω ∂(↑μ' : Measure E))))
    (g : E →ᵇ 𝕜) (hg : g ∈ A),
    Tendsto.{u_4, u_2} (α := ι) (β := 𝕜)
      ((fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ∘ fun (x : ι) ↦ x) U.1
      (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ' : Measure E)))
⊢ Tendsto.{u_4, u_2} (α := ι) (β := 𝕜)
    ((fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ∘ fun (x : ι) ↦ x) U.1
    (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ' : Measure E)))

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto 𝕜] at hμ'

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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})
μ' : ProbabilityMeasure E
hμ' :
  ∀ (f : E →ᵇ 𝕜),
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (i : ι) ↦ ∫ (ω : E), (f : (a : E) → 𝕜) ω ∂(↑(μ i) : Measure E)) (↑U : Filter ι)
      (𝓝 (∫ (ω : E), (f : (a : E) → 𝕜) ω ∂(↑μ' : Measure E)))
g : E →ᵇ 𝕜
hg : g ∈ A
⊢ Tendsto.{u_4, u_2} (α := ι) (β := 𝕜)
    ((fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ∘ fun (x : ι) ↦ x) U.1
    (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ' : Measure E)))

Tactic:
hμ' g
-- Module: Mathlib.MeasureTheory.Measure.LevyConvergence
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})
μ' : ProbabilityMeasure E
hμ' :
  ∀ (f : E →ᵇ 𝕜),
    Tendsto.{u_4, u_2} (β := 𝕜) (fun (i : ι) ↦ ∫ (ω : E), (f : (a : E) → 𝕜) ω ∂(↑(μ i) : Measure E)) (↑U : Filter ι)
      (𝓝 (∫ (ω : E), (f : (a : E) → 𝕜) ω ∂(↑μ' : Measure E)))
g : E →ᵇ 𝕜
hg : g ∈ A
⊢ Tendsto.{u_4, u_2} (α := ι) (β := 𝕜)
    ((fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑(μ n) : Measure E)) ∘ fun (x : ι) ↦ x) U.1
    (𝓝 (∫ (x : E), (g : (a : E) → 𝕜) x ∂(↑μ' : Measure E)))

Tactic:
exact hμ' g
-- 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 →ᵇ ℂ
hg : Membership.mem (γ := StarSubalgebra ℂ (E →ᵇ ℂ)) (charPoly (W := E) (L := innerₗ E) continuous_probChar ⋯) g
⊢ ∃ (w : AddMonoidAlgebra ℂ E),
    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)) :
              ℂ) :
            ℂ)

Tactic:
rw [mem_charPoly] at hg

Premises used: BoundedContinuousFunction.mem_charPoly
-- 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 →ᵇ ℂ
hg :
  ∃ (w : AddMonoidAlgebra ℂ E),
    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)) :
              ℂ) :
            ℂ)
obtain :
  ∀ (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)) :
                ℂ) :
              ℂ)),
    Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
      (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
⊢ Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
    (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))

Tactic:
obtain ⟨w, hw⟩ := hg
-- 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
simp_rw :
  Eq (α := ℂ)
    (∫ (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)) :
              ℂ) :
            ℂ) ∂μ)
    (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        (∫ (x : E),
            (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
              ℂ) ∂μ :
          ℂ))
⊢ 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:
simp_rw [hw]
-- 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
rw :
  Eq (α := ℂ)
    (∑ i ∈ w.support,
      ∫ (a : E),
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) i : ℂ)
          ((↑((probChar : (a : ℝ) → Circle)
                  (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) i)) :
              ℂ) :
            ℂ) ∂μ)
    (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) a : ℂ)
        (∫ (x : E),
            (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a)) :
              ℂ) ∂μ :
          ℂ))
hf :
  ∀ i ∈ w.support,
    Integrable (ε := ℂ)
      (fun (x : E) ↦
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) i : ℂ)
          ((↑((probChar : (a : ℝ) → Circle)
                  (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) i)) :
              ℂ) :
            ℂ))
      μ
⊢ Eq (α := ℂ)
    (∫ (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)) :
              ℂ) :
            ℂ) ∂μ)
    (∑ 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:
rw [integral_finsetSum]

Premises used: MeasureTheory.integral_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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
e_f :
  ∀ (y : E),
    ∫ (a : E),
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) y : ℂ)
          ((↑((probChar : (a : ℝ) → Circle)
                  (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
              ℂ) :
            ℂ) ∂μ =
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) y : ℂ)
        (∫ (x : E),
            (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
              ℂ) ∂μ :
          ℂ)
⊢ Eq (α := ℂ)
    (∑ i ∈ w.support,
      ∫ (a : E),
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) i : ℂ)
          ((↑((probChar : (a : ℝ) → Circle)
                  (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) i)) :
              ℂ) :
            ℂ) ∂μ)
    (∑ 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:
congr with y
-- 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
y : E
e_f e_f₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) y : ℂ)
      (∫ (a : E),
          (↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
            ℂ) ∂μ :
        ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) y : ℂ)
      (∫ (x : E),
          (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
            ℂ) ∂μ :
        ℂ)
⊢ ∫ (a : E),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) y : ℂ)
        ((↑((probChar : (a : ℝ) → Circle)
                (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
            ℂ) :
          ℂ) ∂μ =
    HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) y : ℂ)
      (∫ (x : E),
          (↑((probChar : (a : ℝ) → Circle) ((((innerₗ E : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y)) :
            ℂ) ∂μ :
        ℂ)

Tactic:
rw [integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
⊢ ∀ i ∈ w.support,
    Integrable (ε := ℂ)
      (fun (x : E) ↦
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) i : ℂ)
          ((↑((probChar : (a : ℝ) → Circle)
                  (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) i)) :
              ℂ) :
            ℂ))
      μ

Tactic:
fun i hi ↦ Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul, 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
hf :
  ∀ (i : E) (hi : i ∈ w.support),
    Integrable (ε := ℂ)
      (fun (x : E) ↦
        (↑((probChar : (a : ℝ) → Circle)
              (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) i)) :
          ℂ))
      μ
⊢ ∀ i ∈ w.support,
    Integrable (ε := ℂ)
      (fun (x : E) ↦
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : E) → ℂ) i : ℂ)
          ((↑((probChar : (a : ℝ) → Circle)
                  (((((innerₗ E : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) i)) :
              ℂ) :
            ℂ))
      μ

Tactic:
refine fun i hi ↦ Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
i : E
hi : i ∈ w.support
⊢ Integrable (ε := ℂ) (⇑(innerProbChar i) : (a : E) → ℂ) μ

Tactic:
BoundedContinuousFunction.integrable μ _

Premises used: 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
μ_1 : ι → ProbabilityMeasure E
h : ∀ (t : E), Tendsto (fun (n : ι) ↦ charFun (↑(μ_1 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 μ
i : E
hi : i ∈ w.support
⊢ Integrable (ε := ℂ) (⇑(innerProbChar i) : (a : E) → ℂ) μ

Tactic:
exact BoundedContinuousFunction.integrable μ _

Premises used: BoundedContinuousFunction.integrable