awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
t : PiLp 2 E
⊢ Eq (α := ℂ)
    (∫ (x : (i : ι) → E i),
      cexp
        ((↑(∑ i : ι,
                ⟪ofLp (p := 2)
                    ((MeasurableEquiv.toLp 2 ((i : ι) → E i) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) x) i,
                  t.ofLp i⟫) :
            ℂ) *
          I) ∂Measure.pi (α := E) μ)
    (∫ (x : (i : ι) → E i), ∏ i : ι, cexp ((↑⟪x i, t.ofLp i⟫ : ℂ) * I) ∂Measure.pi (α := E) μ)

Tactic:
simp [ofReal_sum, Finset.sum_mul, Complex.exp_sum]

Premises used: Complex.ofReal_sum, Complex.exp_sum, Finset.sum_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
⊢ ν = Measure.pi (α := E) μ

Tactic:
(MeasurableEquiv.toLp 2 (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFun, MeasurableEquiv.map_measurableEquiv_injective, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
refine :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
        (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) ν) t =
      charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
        (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i))
          (Measure.pi (α := E) μ))
        t
⊢ ν = Measure.pi (α := E) μ

Tactic:
refine (MeasurableEquiv.toLp 2 (Π i, E i)).map_measurableEquiv_injective
      <| Measure.ext_of_charFun <| funext fun t ↦ ?_

Premises used: MeasurableEquiv.toLp, funext, MeasureTheory.Measure.ext_of_charFun, MeasurableEquiv.map_measurableEquiv_injective, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
t : WithLp 2 ((i : ι) → E i)
rw :
  charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
rw₁ :
  ∏ i : ι, charFun (μ i) (t.ofLp i) =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t
rw₂ rw₃ : Eq (α := ℂ) (∏ i : ι, charFun (μ i) (t.ofLp i)) (∏ i : ι, charFun (μ i) (t.ofLp i))
⊢ charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i)) ν) t =
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i))
      (Measure.map (⇑(MeasurableEquiv.toLp 2 ((i : ι) → E i)) : (a : (i : ι) → E i) → WithLp 2 ((i : ι) → E i))
        (Measure.pi (α := E) μ))
      t

Tactic:
rw [MeasurableEquiv.coe_toLp, h, charFun_pi]

Premises used: MeasurableEquiv.coe_toLp, MeasureTheory.charFun_pi
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
rw :
  ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) ν) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)

Tactic:
charFun_pi

Premises used: MeasureTheory.charFun_pi
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
ι : Type u_6
inst : Fintype ι
E : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (E i)
inst_2 : (i : ι) → InnerProductSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_3 : ∀ (i : ι), CompleteSpace.{u_7} (E i)
inst_4 : ∀ (i : ι), SecondCountableTopology.{u_7} (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_7} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_6 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_7 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (t : WithLp 2 ((i : ι) → E i)),
    charFun (mE := WithLp.measurableSpace 2 ((i : ι) → E i)) (Measure.map (toLp 2) (Measure.pi (α := E) μ)) t =
      ∏ i : ι, charFun (μ i) (t.ofLp i)

Tactic:
exact charFun_pi

Premises used: MeasureTheory.charFun_pi
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
L : StrongDual ℝ E
⊢ charFunDual μ L = ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ

Tactic:
rfl

Premises used: MeasureTheory.charFunDual, rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
rw :
  ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1
⊢ charFunDual μ L = charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1

Tactic:
rw [charFunDual_apply]

Premises used: MeasureTheory.charFunDual_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
hfm :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
    (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ Measurable (β := ℂ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
    (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
exact Measurable.aestronglyMeasurable <| by fun_prop

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))

Tactic:
have : ∫ x, cexp (L x * I) ∂μ = ∫ x, cexp (x * I) ∂(μ.map L) := by
    rw [integral_map]
    · fun_prop
    · exact Measurable.aestronglyMeasurable <| by fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
this :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑⟪x, 1⟫ : ℂ) * I))
⊢ ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) 1

Tactic:
rw [this, charFun_apply]

Premises used: MeasureTheory.charFun_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
this :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑x : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑⟪x, 1⟫ : ℂ) * I))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
rw :
  charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    ∫ (v : E), cexp ((↑((u • L : (a : E) → ℝ) v) : ℂ) * I) ∂μ
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u = charFunDual μ (u • L)

Tactic:
rw [charFunDual_apply]

Premises used: MeasureTheory.charFunDual_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
rw :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (∫ (x : E), cexp ((↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
hφ : AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ
hfm :
  AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑u : ℂ) * (↑x : ℂ) * I))
    (Measure.map (⇑L : (a : E) → ℝ) μ)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))

Tactic:
rw [integral_map]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (∫ (x : E), cexp ((↑u : ℂ) * (↑((L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEMeasurable (β := ℝ) (⇑L : (a : E) → ℝ) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ Measurable (β := ℂ) fun (x : ℝ) ↦ cexp ((↑u : ℂ) * (↑x : ℂ) * I)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ cexp ((↑u : ℂ) * (↑x : ℂ) * I))
    (Measure.map (⇑L : (a : E) → ℝ) μ)

Tactic:
exact Measurable.aestronglyMeasurable <| by fun_prop

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))

Tactic:
have : ∫ x, cexp ((u • L) x * I) ∂μ = ∫ x, cexp (u * x * I) ∂(μ.map L) := by
    rw [integral_map]
    · simp
    · fun_prop
    · exact Measurable.aestronglyMeasurable <| by fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
this :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑⟪x, u⟫ : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
⊢ charFun (mE := Real.measurableSpace) (Measure.map (⇑L : (a : E) → ℝ) μ) u =
    ∫ (v : E), cexp ((↑((u • L : (a : E) → ℝ) v) : ℂ) * I) ∂μ

Tactic:
rw [this, charFun_apply]

Premises used: MeasureTheory.charFun_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : OpensMeasurableSpace E
L : StrongDual ℝ E
u : ℝ
this :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((u • L : (a : E) → ℝ) x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦ cexp ((↑⟪x, u⟫ : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : E) → ℝ) μ) fun (x : ℝ) ↦
      cexp ((↑u : ℂ) * (↑x : ℂ) * I))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
t : E
⊢ charFun μ t = charFunDual μ ((InnerProductSpace.toDualMap ℝ E : (a : E) → StrongDual ℝ E) t)

Tactic:
simp [charFunDual_apply, charFun_apply, real_inner_comm]

Premises used: MeasureTheory.charFunDual_apply, MeasureTheory.charFun_apply, real_inner_comm
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
L : StrongDual ℝ E
rw :
  charFunDual μ
      ((InnerProductSpace.toDual ℝ E : (a : E) → StrongDual ℝ E)
        ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L)) =
    charFunDual μ L
⊢ charFun μ ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L) = charFunDual μ L

Tactic:
rw [charFun_eq_charFunDual_toDualMap, ← InnerProductSpace.toDual_apply_eq_toDualMap_apply]

Premises used: InnerProductSpace.toDual_apply_eq_toDualMap_apply, MeasureTheory.charFun_eq_charFunDual_toDualMap
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
L : StrongDual ℝ E
⊢ charFunDual μ
      ((InnerProductSpace.toDual ℝ E : (a : E) → StrongDual ℝ E)
        ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L)) =
    charFunDual μ L

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : OpensMeasurableSpace E
inst_5 : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
⊢ Measurable (α := F) (β := ℝ) (⇑L' : (a : F) → ℝ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : OpensMeasurableSpace E
inst_5 : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
⊢ Measurable.{u_2, u_3} (α := E) (β := F) (⇑L : (a : E) → F)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : OpensMeasurableSpace E
inst_5 : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
rw :
  charFun (E := ℝ) (mE := Real.measurableSpace)
      (Measure.map (Function.comp (β := F) (⇑L' : (a : F) → ℝ) (⇑L : (a : E) → F)) μ) 1 =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑(L' ∘SL L) : (a : E) → ℝ) μ) 1
⊢ charFunDual (mE := mF) (Measure.map (⇑L : (a : E) → F) μ) L' = charFunDual μ (L' ∘SL L)

Tactic:
rw [charFunDual_eq_charFun_map_one, charFunDual_eq_charFun_map_one,
    Measure.map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.charFunDual_eq_charFun_map_one, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
mF : MeasurableSpace F
μ : Measure E
inst_4 : OpensMeasurableSpace E
inst_5 : BorelSpace F
L : E →L[ℝ] F
L' : StrongDual ℝ F
⊢ charFun (E := ℝ) (mE := Real.measurableSpace)
      (Measure.map (Function.comp (β := F) (⇑L' : (a : F) → ℝ) (⇑L : (a : E) → F)) μ) 1 =
    charFun (E := ℝ) (mE := Real.measurableSpace) (Measure.map (⇑(L' ∘SL L) : (a : E) → ℝ) μ) 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
x : E
L : StrongDual ℝ E
rw :
  (@integral _ _ _ _ mE (Measure.dirac x) fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) =
    cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
rw₁ rw₂ : cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I) = cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)
⊢ charFunDual (mE := mE) (Measure.dirac x) L = cexp ((↑((L : (a : E) → ℝ) x) : ℂ) * I)

Tactic:
rw [charFunDual_apply, integral_dirac]

Premises used: MeasureTheory.charFunDual_apply, MeasureTheory.integral_dirac
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ AEMeasurable (β := E) (fun (x : E) ↦ x + r) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := mE) (fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I))
    (Measure.map (fun (x : E) ↦ x + r) μ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
rw :
  Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) (x + r)) : ℂ) * I) ∂μ)
    (∫ (a : E), cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I) ∂μ)
⊢ charFunDual (mE := mE) (Measure.map (fun (x : E) ↦ x + r) μ) L =
    charFunDual μ L * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)

Tactic:
rw [charFunDual_apply, charFunDual_apply, integral_map (by fun_prop) (by fun_prop),
    ← integral_mul_const]

Premises used: MeasureTheory.charFunDual_apply, MeasureTheory.integral_map, MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
μ : Measure E
inst_2 : BorelSpace E
r : E
L : StrongDual ℝ E
e_f :
  ∀ (a : E),
    cexp ((↑((L : (a : E) → ℝ) (a + r)) : ℂ) * I) =
      cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I)
⊢ Eq (α := ℂ) (∫ (x : E), cexp ((↑((L : (a : E) → ℝ) (x + r)) : ℂ) * I) ∂μ)
    (∫ (a : E), cexp ((↑((L : (a : E) → ℝ) a) : ℂ) * I) * cexp ((↑((L : (a : E) → ℝ) r) : ℂ) * I) ∂μ)

Tactic:
congr with a