awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
p : ℝ≥0∞
inst : Fact (1 ≤ p)
ι : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
E : ι → Type u_5
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace ℝ (E i)
mE : (i : ι) → MeasurableSpace (E i)
inst_5 : ∀ (i : ι), BorelSpace.{u_5} (E i)
inst_6 : ∀ (i : ι), SecondCountableTopology.{u_5} (E i)
inst_7 : ∀ (i : ι), CompleteSpace.{u_5} (E i)
μ : (i : ι) → Measure (E i)
ν : Measure ((i : ι) → E i)
inst_8 : ∀ (i : ι), IsFiniteMeasure (μ i)
inst_9 : IsFiniteMeasure ν
h : ν = Measure.pi (α := E) μ
⊢ ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
    charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) ν) L =
      ∏ i : ι,
        charFunDual (μ i)
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
              (ContinuousLinearMap.single ℝ E i)))
have rw : ∀ (L : StrongDual ℝ (WithLp p ((i : ι) → E i))),
  charFunDual (mE := WithLp.measurableSpace p ((i : ι) → E i)) (Measure.map (toLp p) (Measure.pi (α := E) μ)) L =
    ∏ i : ι,
      charFunDual (μ i)
        (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ) L
          (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
            (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv p ℝ E)) : ((i : ι) → E i) →L[ℝ] PiLp p E)
            (ContinuousLinearMap.single ℝ E i)))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ charFunDual (μ ∗ ν) L = charFunDual μ L * charFunDual ν L
have simp_rw : ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ ∗ ν =
  HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
    (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
Tactic: simp_rw [charFunDual_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
have rw : ∫ (x : E), ∫ (y : E), cexp ((↑((L : (a : E) → ℝ) (x + y)) : ℂ) * I) ∂ν ∂μ =
  HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
    (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
Tactic: rw [integral_conv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
mE : MeasurableSpace E
inst_2 : BorelSpace E
inst_3 : SecondCountableTopology E
μ ν : Measure E
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
L : StrongDual ℝ E
rw :
  ∫ (x : E), ∫ (y : E), cexp ((↑((L : (a : E) → ℝ) (x + y)) : ℂ) * I) ∂ν ∂μ =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
⊢ ∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ ∗ ν =
    HMul.hMul (α := ℂ) (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂μ)
      (∫ (v : E), cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I) ∂ν)
have rw₁ : Integrable (ε := ℂ) (fun (v : E) ↦ cexp ((↑((L : (a : E) → ℝ) v) : ℂ) * I)) (μ ∗ ν)
Tactic: rw [integral_conv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (charFun μ)
have simp_rw : ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
  fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
Tactic: simp_rw [funext charFun_eq_fourierIntegral']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
⊢ ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
    fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
have refine : ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
  Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ
Tactic: refine (contDiff_fourierIntegral (L := innerSL ℝ) fun k hk ↦ ?_).comp (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 : ℕ
hint : MemLp id (↑n : ENNReal) μ
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ
have simp : Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k) μ
Tactic: simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) (charFun μ)
have simp_rw : ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
  fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
Tactic: simp_rw [funext charFun_eq_fourierIntegral']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
⊢ ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) fun (x : E) ↦
    fourierIntegral Real.fourierChar μ (innerₗ E) 1 (-(2 * Real.pi)⁻¹ • x)
have refine : ∀ (k : ℕ) (hk : (↑k : ℕ∞) ≤ n), Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ
Tactic: refine (contDiff_fourierIntegral (L := innerSL ℝ) fun k hk ↦ ?_).comp (by fun_prop)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 : ℕ∞
hint : ∀ (k : ℕ), MemLp id (↑k : ENNReal) μ
k : ℕ
hk : (↑k : ℕ∞) ≤ n
⊢ Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k * norm (E := ℂ) (1 v)) μ
have simp : Integrable (ε := ℝ) (fun (v : E) ↦ ‖v‖ ^ k) μ
Tactic: simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (charFun μ)
have refine : MemLp id (↑0 : ENNReal) μ
Tactic: refine contDiff_zero.1 (contDiff_charFun ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 μ
⊢ MemLp id (↑0 : ENNReal) μ
have simpa : AEStronglyMeasurable id μ
Tactic: simpa using by fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (hypothesis)
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
⊢ (iteratedFDeriv ℝ n (charFun μ) t : (a : (i : Fin n) → E) → ℂ) x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
have h : Eq (α := E →ₗ[ℝ] E →ₗ[ℝ] ℝ) (innerₗ E) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ))
Tactic: have h : innerₗ E = (innerSL ℝ).toLinearMap₁₂ := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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 ℝ))
k : ℕ
hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
have simp : Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k) μ
Tactic: simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (hypothesis)
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 ℝ))
⊢ (iteratedFDeriv ℝ n (charFun μ) t : (a : (i : Fin n) → E) → ℂ) x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
have hint' : ∀ (k : ℕ) (hk : LE.le (α := ℕ∞) (↑k : ℕ∞) (↑n : ℕ∞)),
  Integrable (ε := ℝ) (fun (x : E) ↦ ‖x‖ ^ k * norm (E := ℂ) (1 x)) μ
Tactic: have hint' (k : ℕ) (hk : k ≤ (n : ℕ∞)) : Integrable (fun x ↦ ‖x‖ ^ k * ‖(1 : E → ℂ) x‖) μ := by
    simp only [Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary, mul_one]
    refine MemLp.integrable_norm_pow' (hint.mono_exponent (by simp_all))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ (iteratedFDeriv ℝ n (charFun μ) t : (a : (i : Fin n) → E) → ℂ) x =
    I ^ n * ∫ (y : E), (↑(∏ i : Fin n, ⟪y, x i⟫) : ℂ) * cexp ((↑⟪y, t⟫ : ℂ) * I) ∂μ
have 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) ∂μ
Tactic: simp_rw [funext charFun_eq_fourierIntegral']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ (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) ∂μ
have 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) ∂μ
Tactic: rw [iteratedFDeriv_comp_const_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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) ∂μ
⊢ (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) ∂μ
have hf : ContDiff ℝ (F := ℂ) (↑n : WithTop ℕ∞) (fourierIntegral Real.fourierChar μ (innerₗ E) 1)
Tactic: rw [iteratedFDeriv_comp_const_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ ((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) ∂μ
have 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) ∂μ
Tactic: simp only [mul_inv_rev, neg_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ (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) ∂μ
have 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) ∂μ
Tactic: rw [h, iteratedFDeriv_fourierIntegral _ hint' (by fun_prop) le_rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ (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) ∂μ
have 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) ∂μ
Tactic: simp only [ContinuousMultilinearMap.smul_apply, real_smul, ofReal_pow, ofReal_neg, ofReal_mul,
    ofReal_inv, ofReal_ofNat, ofReal_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ 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) ∂μ
have 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) ∂μ
Tactic: rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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) ∂μ
⊢ 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) ∂μ
have rw₁ : Integrable (ε := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) ℂ)
  (fun (v : E) ↦ fourierPowSMulRight (innerSL ℝ) 1 v n) μ
Tactic: rw [fourierIntegral_continuousMultilinearMap_apply Real.continuous_fourierChar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion (goal)
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)) μ
⊢ (-((↑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) ∂μ
have 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) ∂μ
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]