awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have refine : ∀ (x : ℕ),
  LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) x) : ℝ≥0∞)
    (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: refine le_of_tendsto_of_tendsto' h_tendsto h_tendsto' fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
m : AddContent ℝ≥0∞ C
hC : IsSetRing C
m_iUnion :
  ∀ (f : ℕ → Set α),
    (∀ (i : ℕ), f i ∈ C) →
      ⋃ (i : ℕ), f i ∈ C →
        ∀ (_hf_disj : Pairwise (Disjoint on f)),
          Eq (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
            (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
f : ℕ → Set α
hf : ∀ (i : ℕ), f i ∈ C
hf_Union : ⋃ (i : ℕ), f i ∈ C
h_tendsto :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) n) : ℝ≥0∞)) atTop
    (𝓝 ((m : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i)) : Filter ℝ≥0∞)
h_tendsto' :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), (m : (a : Set α) → ℝ≥0∞) (f i)) atTop
    (𝓝 (∑' (i : ℕ), (m : (a : Set α) → ℝ≥0∞) (f i)))
x : ℕ
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) ((partialSups f : (a : ℕ) → Set α) x) : ℝ≥0∞)
    (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) (⋃ i ∈ Finset.range (x + 1), f i) : ℝ≥0∞)
  (∑ i ∈ Finset.range (x + 1), (m : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: rw [partialSups_eq_biUnion_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
⊢ P = P'
have apply : ∀ g ∈ charPoly he hL, Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
Tactic: apply ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
      (separatesPoints_charPoly he he' hL hL')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (hypothesis)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
hg : g ∈ charPoly he hL
⊢ Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
have hg₁ : ∃ (w : AddMonoidAlgebra ℂ W),
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
Tactic: simp only [mem_charPoly] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
hg :
  ∃ (w : AddMonoidAlgebra ℂ W),
    Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
⊢ Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
have obtain : ∀ (w : AddMonoidAlgebra ℂ W)
  (hw :
    Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)),
  Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
Tactic: obtain ⟨w, hw⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
⊢ Eq (α := ℂ) (∫ (x : V), (g : (a : V) → ℂ) x ∂P) (∫ (x : V), (g : (a : V) → ℂ) x ∂P')
have rw : Eq (α := ℂ)
  (∫ (x : V),
    (fun (x : V) ↦
        (∑ a ∈ w.support,
            HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
              ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
          ℂ))
      x ∂P)
  (∫ (x : V),
    (fun (x : V) ↦
        (∑ a ∈ w.support,
            HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
              ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
          ℂ))
      x ∂P')
Tactic: rw [hw]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (hypothesis)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
⊢ Eq (α := ℂ)
    (∫ (x : V),
      (fun (x : V) ↦
          (∑ a ∈ w.support,
              HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
                ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
            ℂ))
        x ∂P)
    (∫ (x : V),
      (fun (x : V) ↦
          (∑ a ∈ w.support,
              HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
                ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
            ℂ))
        x ∂P')
have hsum : ∀ (P : Measure V) [IsFiniteMeasure P],
  Eq (α := ℂ)
    (∫ (v : V),
      ∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
    (∑ a ∈ w.support,
      ∫ (v : V),
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
Tactic: have hsum (P : Measure V) [IsFiniteMeasure P] :
      ∫ v, ∑ a ∈ w.support, w a * e (L v a) ∂P = ∑ a ∈ w.support, ∫ v, w a * e (L v a) ∂P :=
    integral_finsetSum w.support
      fun a ha => Integrable.const_mul (integrable P (char he hL a)) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
hsum :
  ∀ (P : Measure V) [IsFiniteMeasure P],
    Eq (α := ℂ)
      (∫ (v : V),
        ∑ a ∈ w.support,
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
      (∑ a ∈ w.support,
        ∫ (v : V),
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
⊢ Eq (α := ℂ)
    (∫ (x : V),
      (fun (x : V) ↦
          (∑ a ∈ w.support,
              HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
                ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
            ℂ))
        x ∂P)
    (∫ (x : V),
      (fun (x : V) ↦
          (∑ a ∈ w.support,
              HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
                ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
            ℂ))
        x ∂P')
have rw : Eq (α := ℂ)
  (∑ a ∈ w.support,
    ∫ (v : V),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
  (∑ a ∈ w.support,
    ∫ (v : V),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P')
Tactic: rw [hsum P, hsum P']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
hsum :
  ∀ (P : Measure V) [IsFiniteMeasure P],
    Eq (α := ℂ)
      (∫ (v : V),
        ∑ a ∈ w.support,
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
      (∑ a ∈ w.support,
        ∫ (v : V),
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
⊢ Eq (α := ℂ)
    (∑ a ∈ w.support,
      ∫ (v : V),
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
    (∑ a ∈ w.support,
      ∫ (v : V),
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P')
have apply : ∀ i ∈ w.support,
  Eq (α := ℂ)
    (∫ (v : V),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) i : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) i)) : ℂ) : ℂ) ∂P)
    (∫ (v : V),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) i : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) i)) : ℂ) : ℂ) ∂P')
Tactic: apply Finset.sum_congr rfl fun i _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
W : Type u_1
inst : AddCommGroup W
inst_1 : Module ℝ W
inst_2 : TopologicalSpace W
e : AddChar ℝ Circle
V : Type u_2
inst_3 : AddCommGroup V
inst_4 : Module ℝ V
inst_5 : PseudoEMetricSpace V
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
inst_8 : CompleteSpace V
inst_9 : SecondCountableTopology V
L : LinearMap.{0, 0, u_2, u_1} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_1 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
P P' : Measure V
inst_10 : IsFiniteMeasure P
inst_11 : IsFiniteMeasure P'
h :
  ∀ (w : W), Eq (α := ℂ) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P) (∫ (v : V), (char he hL w : (a : V) → ℂ) v ∂P')
g : V →ᵇ ℂ
w : AddMonoidAlgebra ℂ W
hw :
  Eq (α := (a : V) → ℂ) (⇑g : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
hsum :
  ∀ (P : Measure V) [IsFiniteMeasure P],
    Eq (α := ℂ)
      (∫ (v : V),
        ∑ a ∈ w.support,
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
      (∑ a ∈ w.support,
        ∫ (v : V),
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) ∂P)
i : W
h_1 : i ∈ w.support
⊢ Eq (α := ℂ)
    (∫ (v : V),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) i : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) i)) : ℂ) : ℂ) ∂P)
    (∫ (v : V),
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) i : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) i)) : ℂ) : ℂ) ∂P')
have simp : Eq (α := ℂ)
    (∫ (a : V), (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) a : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) i)) : ℂ) ∂P)
    (∫ (a : V), (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) a : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) i)) : ℂ) ∂P') ∨
  Eq (α := ℂ) ((w : (a : W) → ℂ) i : ℂ) (0 : ℂ)
Tactic: simp only [MeasureTheory.integral_const_mul, mul_eq_mul_left_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ charFun μ t = VectorFourier.fourierIntegral fourierChar μ (innerₗ E) 1 (-(2 * π)⁻¹ • t)
have simp : Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ)
  (∫ (v : E), cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) ∂μ)
Tactic: simp only [charFun_apply, VectorFourier.fourierIntegral, neg_smul,
    innerₗ_apply_apply, inner_neg_right, inner_smul_right, neg_neg,
    fourierChar_apply', Pi.ofNat_apply, Circle.smul_def, Circle.coe_exp, ofReal_mul, ofReal_ofNat,
    ofReal_inv, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ)
    (∫ (v : E), cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) ∂μ)
have e_f : ∀ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ)) * I)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t x : E
⊢ cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ)) * I)
have e_f : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * (2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ) * I)
Tactic: rw [← mul_assoc, mul_inv_cancel₀ (by simp [pi_ne_zero]), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t x : E
e_f : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * (2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ) * I)
⊢ cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ)) * I)
have e_f₁ : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (1 * (↑⟪x, t⟫ : ℂ) * I)
Tactic: rw [← mul_assoc, mul_inv_cancel₀ (by simp [pi_ne_zero]), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t x : E
e_f : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * (2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ) * I)
e_f₁ : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (1 * (↑⟪x, t⟫ : ℂ) * I)
⊢ cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ)) * I)
have e_f₂ : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp ((↑⟪x, t⟫ : ℂ) * I)
Tactic: rw [← mul_assoc, mul_inv_cancel₀ (by simp [pi_ne_zero]), one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ ‖charFun μ t‖ ≤ μ.real Set.univ
have rw : Norm.norm (E := ℂ) (VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t)) ≤ μ.real Set.univ
Tactic: rw [charFun_eq_fourierIntegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : OpensMeasurableSpace E
inst_3 : SecondCountableTopology E
inst_4 : SFinite μ
⊢ Measurable.{u_2, 0} (α := E × E) (β := ℂ) (Function.uncurry fun (x y : E) ↦ cexp ((↑⟪x, y⟫ : ℂ) * I))
have funProp : LE.le.{u_2} (α := MeasurableSpace (E × E)) Prod.instMeasurableSpace Prod.instMeasurableSpace
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : OpensMeasurableSpace E
inst_3 : SecondCountableTopology E
inst_4 : SFinite μ
funProp : LE.le.{u_2} (α := MeasurableSpace (E × E)) Prod.instMeasurableSpace Prod.instMeasurableSpace
⊢ Measurable.{u_2, 0} (α := E × E) (β := ℂ) (Function.uncurry fun (x y : E) ↦ cexp ((↑⟪x, y⟫ : ℂ) * I))
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (x : E × E) ↦ ⟪x.1, x.2⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : BorelSpace E
r : ℝ
t : E
⊢ charFun (mE := mE) (Measure.map (fun (x : E) ↦ r • x) μ) t = charFun μ (r • t)
have rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪r • x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, r • t⟫ : ℂ) * I) ∂μ)
Tactic: rw [charFun_apply, charFun_apply,
    integral_map (by fun_prop) (by fun_prop)]