awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ μ₀ = μ'
have h : ∀ (s : Set E),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((↑μ' : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- 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)
s : Set E
h_1 : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((↑μ' : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) (((↑μ₀ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [this]
-- 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})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
⊢ Tendsto μ (↑U : Filter ι) (𝓝 μ₀)
have inr : (↑μ' : Measure E) = (↑μ₀ : Measure E)
Tactic: suffices (μ' : Measure E) = μ₀ by convert! hμ'; ext; rw [this]
-- 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})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
⊢ (↑μ' : Measure E) = (↑μ₀ : Measure E)
have 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)))
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)
-- 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})
μ' : ProbabilityMeasure E
hμ' : Tendsto μ (↑U : Filter ι) (𝓝 μ')
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)))
have 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)))
Tactic: rw [ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto 𝕜] at hμ'
Cleared hypotheses: hμ', g, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (hypothesis)
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
⊢ Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
    (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
have 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)) :
            ℂ) :
          ℂ)
Tactic: rw [mem_charPoly] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
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)) :
              ℂ) :
            ℂ)
⊢ Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
    (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
have 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)))
Tactic: obtain ⟨w, hw⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
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 μ
⊢ 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)) :
              ℂ) ∂μ :
          ℂ))
have 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)) :
            ℂ) ∂μ :
        ℂ))
Tactic: simp_rw [hw]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
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 μ
⊢ 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)) :
              ℂ) ∂μ :
          ℂ))
have 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)) :
            ℂ) ∂μ :
        ℂ))
Tactic: rw [integral_finsetSum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
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)) :
              ℂ) ∂μ :
          ℂ))
⊢ 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)) :
              ℂ) ∂μ :
          ℂ))
have 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)) :
            ℂ) :
          ℂ))
    μ
Tactic: rw [integral_finsetSum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
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 μ
⊢ 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)) :
              ℂ) ∂μ :
          ℂ))
have 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)) :
            ℂ) ∂μ :
        ℂ)
Tactic: congr with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
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
⊢ ∫ (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)) :
            ℂ) ∂μ :
        ℂ)
have 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)) : ℂ) ∂μ :
      ℂ)
Tactic: rw [integral_const_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : 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)) :
              ℂ) :
            ℂ))
      μ
have 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)) :
        ℂ))
    μ
Tactic: refine fun i hi ↦ Integrable.const_mul ?_ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyConvergence (hypothesis)
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)) :
            ℂ) :
          ℂ)
⊢ Tendsto (β := ℂ) (fun (n : ι) ↦ ∫ (x : E), (g : (a : E) → ℂ) x ∂(↑(μ n) : Measure E)) 𝓕
    (𝓝 (∫ (x : E), (g : (a : E) → ℂ) x ∂(↑μ₀ : Measure E)))
have 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)) :
              ℂ) ∂μ :
          ℂ))
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 μ _