awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
simp_rw :
  (iteratedFDeriv ℝ n (fun (x : E) ↦ fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)) t :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
⊢ (iteratedFDeriv ℝ n (charFun μ) t : (a : (i : Fin n) → E) → ℂ) x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
simp_rw [funext charFun_eq_fourierIntegral']

Premises used: MeasureTheory.charFun_eq_fourierIntegral', funext
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
rw :
  ((fun (x : E) ↦
            HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ) ((-(2 * Real.pi)⁻¹) ^ n)
              (iteratedFDeriv ℝ n (fourierIntegral Real.fourierChar μ (innerₗ E) 1) (-(2 * Real.pi)⁻¹ • x)))
          t :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
hf : ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) (fourierIntegral Real.fourierChar μ (innerₗ E) 1)
⊢ (iteratedFDeriv ℝ n (fun (x : E) ↦ fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)) t :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
rw [iteratedFDeriv_comp_const_smul]

Premises used: iteratedFDeriv_comp_const_smul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞)
    (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 1)

Tactic:
contDiff_fourierIntegral _ hint'

Premises used: MonoidHomClass.toMonoidHom, VectorFourier.contDiff_fourierIntegral, RingHomClass.toRingHom, starRingEnd
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞)
    (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) 1)

Tactic:
exact contDiff_fourierIntegral _ hint'

Premises used: VectorFourier.contDiff_fourierIntegral
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
simp :
  (HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ) ((-(Real.pi⁻¹ * 2⁻¹)) ^ n)
          (iteratedFDeriv ℝ n (fourierIntegral Real.fourierChar μ (innerₗ E) 1) (-((Real.pi⁻¹ * 2⁻¹) • t))) :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
⊢ ((fun (x : E) ↦
            HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ) ((-(2 * Real.pi)⁻¹) ^ n)
              (iteratedFDeriv ℝ n (fourierIntegral Real.fourierChar μ (innerₗ E) 1) (-(2 * Real.pi)⁻¹ • x)))
          t :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
simp only [mul_inv_rev, neg_smul]

Premises used: neg_smul, mul_inv_rev
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ AEStronglyMeasurable (β := ℂ) 1 μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
rw :
  (HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ) ((-(Real.pi⁻¹ * 2⁻¹)) ^ n)
          (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
            (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) (-((Real.pi⁻¹ * 2⁻¹) • t))) :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
⊢ (HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ) ((-(Real.pi⁻¹ * 2⁻¹)) ^ n)
          (iteratedFDeriv ℝ n (fourierIntegral Real.fourierChar μ (innerₗ E) 1) (-((Real.pi⁻¹ * 2⁻¹) • t))) :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
rw [h, iteratedFDeriv_fourierIntegral _ hint' (by fun_prop) le_rfl]

Premises used: le_rfl, VectorFourier.iteratedFDeriv_fourierIntegral
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
simp :
  HMul.hMul (β := ℂ) ((-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n)
      ((fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
              (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) (-((Real.pi⁻¹ * 2⁻¹) • t)) :
            (a : (i : Fin n) → E) → ℂ)
          x :
        ℂ) =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
⊢ (HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ) ((-(Real.pi⁻¹ * 2⁻¹)) ^ n)
          (fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
            (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) (-((Real.pi⁻¹ * 2⁻¹) • t))) :
        (a : (i : Fin n) → E) → ℂ)
      x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
simp only [ContinuousMultilinearMap.smul_apply, real_smul, ofReal_pow, ofReal_neg, ofReal_mul,
    ofReal_inv, ofReal_ofNat, ofReal_prod]

Premises used: Complex.real_smul, Complex.ofReal_neg, Complex.ofReal_prod, ContinuousMultilinearMap.smul_apply, Complex.ofReal_ofNat, Complex.ofReal_pow, Complex.ofReal_inv, Complex.ofReal_mul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
rw :
  (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n *
      fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
        (fun (x_1 : E) ↦ (fourierPowSMulRight (innerSL ℝ) 1 x_1 n : (a : (i : Fin n) → E) → ℂ) x)
        (-((Real.pi⁻¹ * 2⁻¹) • t)) =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
rw₁ :
  Integrable (ε := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ)
    (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) μ
⊢ HMul.hMul (β := ℂ) ((-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n)
      ((fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
              (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) (-((Real.pi⁻¹ * 2⁻¹) • t)) :
            (a : (i : Fin n) → E) → ℂ)
          x :
        ℂ) =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]

Premises used: Real.continuous_fourierChar, VectorFourier.fourierIntegral_continuousMultilinearMap_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ n * norm (E := ℂ) (1 v)) μ

Tactic:
simpa using hint.integrable_norm_pow'

Premises used: MeasureTheory.MemLp.integrable_norm_pow'
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
⊢ Integrable (ε := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ)
    (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) μ

Tactic:
exact integrable_fourierPowSMulRight _ (by simpa using hint.integrable_norm_pow') (by fun_prop)

Premises used: VectorFourier.integrable_fourierPowSMulRight
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
simp :
  (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n *
      ∫ (v : E),
        cexp (2 * (↑Real.pi : ℂ) * ((↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) *
          ((-(2 * (↑Real.pi : ℂ) * I)) ^ n * ∏ i : Fin n, (↑⟪v, x i⟫ : ℂ)) ∂μ =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
⊢ (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n *
      fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
        (fun (x_1 : E) ↦ (fourierPowSMulRight (innerSL ℝ) 1 x_1 n : (a : (i : Fin n) → E) → ℂ) x)
        (-((Real.pi⁻¹ * 2⁻¹) • t)) =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
simp only [fourierIntegral, Real.fourierChar, Circle.exp, ContinuousMap.coe_mk, ofReal_mul,
    ofReal_ofNat, innerSL, map_neg, map_smul, ContinuousLinearMap.toLinearMap₁₂_apply,
    LinearMap.mkContinuous₂_apply, innerₛₗ_apply_apply, smul_eq_mul, neg_neg, AddChar.coe_mk,
    ofReal_inv, fourierPowSMulRight_apply, Pi.ofNat_apply, real_smul, ofReal_prod, mul_one,
    Circle.smul_def]

Premises used: LinearMap.mkContinuous₂_apply, Complex.real_smul, innerₛₗ_apply_apply, ContinuousLinearMap.toLinearMap₁₂_apply, innerSL, Real.fourierChar, Circle.smul_def, VectorFourier.fourierIntegral, neg_neg, Complex.ofReal_prod, Pi.ofNat_apply, map_neg, Circle.exp, ContinuousMap.coe_mk, VectorFourier.fourierPowSMulRight_apply, smul_eq_mul, mul_one, Complex.ofReal_ofNat, Complex.ofReal_inv, Complex.ofReal_mul, AddChar.coe_mk, map_smul
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
simp_rw :
  (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹) * -(2 * (↑Real.pi : ℂ) * I)) ^ n *
      ∫ (a : E),
        cexp (2 * (↑Real.pi : ℂ) * (↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪a, t⟫ : ℂ) * I) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
⊢ (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹)) ^ n *
      ∫ (v : E),
        cexp (2 * (↑Real.pi : ℂ) * ((↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪v, t⟫ : ℂ)) * I) *
          ((-(2 * (↑Real.pi : ℂ) * I)) ^ n * ∏ i : Fin n, (↑⟪v, x i⟫ : ℂ)) ∂μ =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
simp_rw [mul_left_comm (exp _), integral_const_mul, ← mul_assoc, ← mul_pow]

Premises used: MeasureTheory.integral_const_mul, mul_assoc, mul_left_comm, Complex.exp, mul_pow
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
field_simp :
  Eq (α := ℂ) (∫ (a : E), cexp (I * (↑⟪a, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ)
    (∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp (I * (↑⟪y, t⟫ : ℂ)) ∂μ)
⊢ (-((↑Real.pi : ℂ)⁻¹ * 2⁻¹) * -(2 * (↑Real.pi : ℂ) * I)) ^ n *
      ∫ (a : E),
        cexp (2 * (↑Real.pi : ℂ) * (↑Real.pi : ℂ)⁻¹ * 2⁻¹ * (↑⟪a, t⟫ : ℂ) * I) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ =
    I ^ n * ∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ

Tactic:
field_simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
e_f :
  ∀ (x_1 : E),
    cexp (I * (↑⟪x_1, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪x_1, x i⟫ : ℂ) =
      (∏ i : Fin n, (↑⟪x_1, x i⟫ : ℂ)) * cexp (I * (↑⟪x_1, t⟫ : ℂ))
⊢ Eq (α := ℂ) (∫ (a : E), cexp (I * (↑⟪a, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪a, x i⟫ : ℂ) ∂μ)
    (∫ (y : E), (∏ i : Fin n, (↑⟪y, x i⟫ : ℂ)) * cexp (I * (↑⟪y, t⟫ : ℂ)) ∂μ)

Tactic:
congr with
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : SecondCountableTopology E
μ : Measure E
inst_5 : IsFiniteMeasure μ
n : ℕ
t : E
hint : MemLp id (↑n : ENNReal) μ
x : Fin n → E
h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
hint' :
  ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
    Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
x_1 : E
⊢ cexp (I * (↑⟪x_1, t⟫ : ℂ)) * ∏ i : Fin n, (↑⟪x_1, x i⟫ : ℂ) =
    (∏ i : Fin n, (↑⟪x_1, x i⟫ : ℂ)) * cexp (I * (↑⟪x_1, t⟫ : ℂ))

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
t : ℝ
hint : MemLp id (↑n : ENNReal) μ
rw :
  I ^ n * ∫ (y : ℝ), (↑(∏ i : Fin n, ⟪y, 1⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ =
    I ^ n * ∫ (x : ℝ), (↑x : ℂ) ^ n * cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ
⊢ iteratedDeriv n (charFun μ) t = I ^ n * ∫ (x : ℝ), (↑x : ℂ) ^ n * cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ

Tactic:
rw [iteratedDeriv, iteratedFDeriv_charFun hint]

Premises used: MeasureTheory.iteratedFDeriv_charFun, iteratedDeriv
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
t : ℝ
hint : MemLp id (↑n : ENNReal) μ
⊢ I ^ n * ∫ (y : ℝ), (↑(∏ i : Fin n, ⟪y, 1⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ =
    I ^ n * ∫ (x : ℝ), (↑x : ℂ) ^ n * cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
simp : ∫ (x : ℝ), (↑x : ℂ) ^ n ∂μ = (↑(∫ (x : ℝ), x ^ n ∂μ) : ℂ)
⊢ iteratedDeriv n (charFun μ) 0 = I ^ n * (↑(∫ (x : ℝ), x ^ n ∂μ) : ℂ)

Tactic:
simp [iteratedDeriv_charFun hint]

Premises used: MeasureTheory.iteratedDeriv_charFun
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℝ) (∫ (x : ℝ), x ^ n ∂μ) (∫ (x : ℝ), x ^ n ∂μ)
⊢ ∫ (x : ℝ), (↑x : ℂ) ^ n ∂μ = (↑(∫ (x : ℝ), x ^ n ∂μ) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
simp_rw :
  Eq (α := ℂ) (∑ x ∈ Finset.range (n + 1), (↑((↑x ! : ℝ)⁻¹ * t ^ x) : ℂ) * iteratedDerivWithin x (charFun μ) univ 0)
    (∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ))
⊢ taylorWithinEval (charFun μ) n univ 0 t =
    ∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)

Tactic:
simp_rw [taylor_within_apply, sub_zero, RCLike.real_smul_eq_coe_mul]

Premises used: sub_zero, RCLike.real_smul_eq_coe_mul, taylor_within_apply
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
⊢ Eq (α := ℂ) (∑ x ∈ Finset.range (n + 1), (↑((↑x ! : ℝ)⁻¹ * t ^ x) : ℂ) * iteratedDerivWithin x (charFun μ) univ 0)
    (∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ))

Tactic:
Finset.sum_congr rfl fun k hkn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
refine :
  ∀ (k : ℕ) (hkn : k ∈ Finset.range (n + 1)),
    (↑((↑k ! : ℝ)⁻¹ * t ^ k) : ℂ) * iteratedDerivWithin k (charFun μ) univ 0 =
      (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
⊢ Eq (α := ℂ) (∑ x ∈ Finset.range (n + 1), (↑((↑x ! : ℝ)⁻¹ * t ^ x) : ℂ) * iteratedDerivWithin x (charFun μ) univ 0)
    (∑ k ∈ Finset.range (n + 1), (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ))

Tactic:
refine Finset.sum_congr rfl fun k hkn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
push_cast :
  (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (↑t : ℂ) k * iteratedDerivWithin k (charFun μ) univ 0 =
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)
⊢ (↑((↑k ! : ℝ)⁻¹ * t ^ k) : ℂ) * iteratedDerivWithin k (charFun μ) univ 0 =
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)

Tactic:
push_cast
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
⊢ LE.le (α := ENNReal) (↑k : ENNReal) (↑n : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
⊢ MemLp id (↑k : ENNReal) μ

Tactic:
have hint' : MemLp id k μ := hint.mono_exponent (by simp_all)
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
μ : Measure ℝ
inst : IsFiniteMeasure μ
n : ℕ
hint : MemLp id (↑n : ENNReal) μ
t : ℝ
k : ℕ
hkn : k ∈ Finset.range (n + 1)
hint' : MemLp id (↑k : ENNReal) μ
⊢ (↑k ! : ℂ)⁻¹ * HPow.hPow (α := ℂ) (↑t : ℂ) k * iteratedDerivWithin k (charFun μ) univ 0 =
    (↑k ! : ℂ)⁻¹ * ((↑t : ℂ) * I) ^ k * (↑(∫ (x : ℝ), x ^ k ∂μ) : ℂ)

Tactic:
simp [iteratedDeriv_charFun_zero hint', mul_pow, mul_comm, mul_assoc, mul_left_comm]

Premises used: MeasureTheory.iteratedDeriv_charFun_zero, mul_assoc, mul_left_comm, mul_comm, mul_pow
-- Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
hint : MemLp (m0 := Real.measurableSpace) id 2 (Measure.map X P)
t : ℝ
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (Measure.map X P)

Tactic:
have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX