awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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)
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')
⊢ 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 [hsum P, hsum P']
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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)
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')
⊢ 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:
apply Finset.sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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
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 : ℂ)
⊢ 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:
simp only [MeasureTheory.integral_const_mul, mul_eq_mul_left_iff]

Premises used: MeasureTheory.integral_const_mul, mul_eq_mul_left_iff
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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 (α := ℂ)
      (∫ (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:
Or.inl (h i)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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 (α := ℂ)
      (∫ (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:
exact Or.inl (h i)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : Inner ℝ E
t : E
⊢ charFun μ t = ∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ

Tactic:
rfl

Premises used: MeasureTheory.charFun, rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
μ : Measure ℝ
t : ℝ
⊢ charFun μ t = ∫ (x : ℝ), cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ

Tactic:
simp [charFun_apply]

Premises used: MeasureTheory.charFun_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
μ : Measure E
⊢ charFun μ 0 = (↑(μ.real Set.univ) : ℂ)

Tactic:
simp [charFun_apply]

Premises used: MeasureTheory.charFun_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
t : E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ charFun (mE := mE) 0 t = 0

Tactic:
simp [charFun_apply]

Premises used: MeasureTheory.charFun_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ charFun μ (-t) = (starRingEnd ℂ : (a : ℂ) → ℂ) (charFun μ t)

Tactic:
simp [charFun_apply, ← integral_conj, ← exp_conj]

Premises used: MeasureTheory.charFun_apply, integral_conj, Complex.exp_conj
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
t : E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
⊢ charFun μ t = ∫ (v : E), (innerProbChar t : (a : E) → ℂ) v ∂μ

Tactic:
simp [charFun_apply, innerProbChar_apply]

Premises used: MeasureTheory.charFun_apply, BoundedContinuousFunction.innerProbChar_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ charFun μ t = ∫ (x : E), (↑((probChar : (a : ℝ) → Circle) ⟪x, t⟫) : ℂ) ∂μ

Tactic:
simp [charFun_apply, probChar_apply]

Premises used: MeasureTheory.charFun_apply, Real.probChar_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ charFun μ t = VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t)

Tactic:
simp [charFun_apply, VectorFourier.fourierIntegral_probChar]

Premises used: MeasureTheory.charFun_apply, VectorFourier.fourierIntegral_probChar
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
simp :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ)
    (∫ (v : E), cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) ∂μ)
⊢ charFun μ t = VectorFourier.fourierIntegral fourierChar μ (innerₗ E) 1 (-(2 * π)⁻¹ • t)

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]

Premises used: neg_smul, MeasureTheory.charFun_apply, Circle.smul_def, VectorFourier.fourierIntegral, inner_neg_right, neg_neg, Pi.ofNat_apply, inner_smul_right, innerₗ_apply_apply, Real.fourierChar_apply', smul_eq_mul, mul_one, Circle.coe_exp, Complex.ofReal_ofNat, Complex.ofReal_inv, Complex.ofReal_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
e_f : ∀ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ)) * I)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪x, t⟫ : ℂ) * I) ∂μ)
    (∫ (v : E), cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) ∂μ)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t x : E
⊢ 2 * (↑π : ℂ) ≠ 0

Tactic:
simp [pi_ne_zero]

Premises used: Real.pi_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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)
e_f₂ e_f₃ : cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp ((↑⟪x, t⟫ : ℂ) * I)
⊢ cexp ((↑⟪x, t⟫ : ℂ) * I) = cexp (2 * (↑π : ℂ) * ((2 * (↑π : ℂ))⁻¹ * (↑⟪x, t⟫ : ℂ)) * I)

Tactic:
rw [← mul_assoc, mul_inv_cancel₀ (by simp [pi_ne_zero]), one_mul]

Premises used: mul_inv_cancel₀, mul_assoc, one_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
rw : Norm.norm (E := ℂ) (VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t)) ≤ μ.real Set.univ
⊢ ‖charFun μ t‖ ≤ μ.real Set.univ

Tactic:
rw [charFun_eq_fourierIntegral]

Premises used: MeasureTheory.charFun_eq_fourierIntegral
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ ∫ (v : E), Norm.norm (E := ℂ) (1 v) ∂μ = μ.real Set.univ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
t : E
⊢ Norm.norm (E := ℂ) (VectorFourier.fourierIntegral probChar μ (innerₗ E) 1 (-t)) ≤ μ.real Set.univ

Tactic:
exact (VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ _ _).trans_eq (by simp)

Premises used: LE.le.trans_eq, VectorFourier.norm_fourierIntegral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : IsProbabilityMeasure μ
t : E
⊢ μ.real Set.univ = 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
t : E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : IsProbabilityMeasure μ
⊢ Norm.norm (E := ℂ) 1 + ‖charFun μ t‖ ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
simp [norm_charFun_le_one]

Premises used: MeasureTheory.norm_charFun_le_one
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
t : E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : IsProbabilityMeasure μ
⊢ HAdd.hAdd (α := ℝ) 1 1 = 2

Tactic:
norm_num
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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
funProp₁ : MeasurableEmbedding (β := ℝ) fun (x : E × E) ↦ ⟪x.1, x.2⟫
⊢ Measurable.{u_2, 0} (α := E × E) (β := ℂ) (Function.uncurry fun (x y : E) ↦ cexp ((↑⟪x, y⟫ : ℂ) * I))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
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 (charFun μ)

Tactic:
stronglyMeasurable_charFun.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.stronglyMeasurable_charFun
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
a b : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ μ.real Set.univ) volume a b

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : BorelSpace E
r : ℝ
t : E
⊢ AEMeasurable (β := E) (fun (x : E) ↦ r • x) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : BorelSpace E
r : ℝ
t : E
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := mE) (fun (x : E) ↦ cexp ((↑⟪x, t⟫ : ℂ) * I))
    (Measure.map (fun (x : E) ↦ r • x) μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : BorelSpace E
r : ℝ
t : E
rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪r • x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, r • t⟫ : ℂ) * I) ∂μ)
⊢ charFun (mE := mE) (Measure.map (fun (x : E) ↦ r • x) μ) t = charFun μ (r • t)

Tactic:
rw [charFun_apply, charFun_apply,
    integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.charFun_apply, MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
μ : Measure E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : BorelSpace E
r : ℝ
t : E
simp_rw : Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪r • x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑(r * ⟪x, t⟫) : ℂ) * I) ∂μ)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑⟪r • x, t⟫ : ℂ) * I) ∂μ) (∫ (x : E), cexp ((↑⟪x, r • t⟫ : ℂ) * I) ∂μ)

Tactic:
simp_rw [inner_smul_right, ← real_inner_smul_left]

Premises used: inner_smul_right, real_inner_smul_left
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst_2 : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
hg : AEMeasurable (β := E) (_m := mE) (fun (x : E) ↦ r • x) (Measure.map f μ)
hf₁ : AEMeasurable f μ
⊢ charFun (mE := mE) (Measure.map (fun (x : X) ↦ r • f x) μ) t = charFun (mE := mE) (Measure.map f μ) (r • t)

Tactic:
rw [show (fun x ↦ r • (f x)) = (r • ·) ∘ f from rfl, ← AEMeasurable.map_map_of_aemeasurable,
    charFun_map_smul]

Premises used: AEMeasurable.map_map_of_aemeasurable, MeasureTheory.charFun_map_smul, rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst_2 : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
⊢ AEMeasurable (β := E) (_m := mE) (fun (x : E) ↦ r • x) (Measure.map f μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
mE : MeasurableSpace E
inst : SeminormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
X : Type u_3
mX : MeasurableSpace X
μ : Measure X
inst_2 : BorelSpace E
f : X → E
hf : AEMeasurable f μ
r : ℝ
t : E
⊢ AEMeasurable f μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
μ : Measure ℝ
r t : ℝ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (fun (x : ℝ) ↦ r * x) μ) t = charFun μ (r * t)

Tactic:
charFun_map_smul r t

Premises used: MeasureTheory.charFun_map_smul