awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
I₂ :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f v n))
    μ
I₃ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin (n + 1)) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ :
  Integrable (ε := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) μ
w' : W
m : (i : Fin n) → W
h :
  ∀ (v : V),
    Eq.{u_1 + 1} (α := E)
      ((fourierPowSMulRight L f v (n + 1) : (a : (i : Fin (n + 1)) → W) → E)
          (Fin.cons (α := fun (i : Fin (n + 1)) ↦ W) w' m) :
        E)
      (((((fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v :
                    W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
                  (a : W) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) E)
                w' :
              ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
            (a : (i : Fin n) → W) → E)
          m :
        E)
⊢ Eq.{u_1 + 1} (α := E)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂
      (fun (x : V) ↦
        (fourierPowSMulRight L f x (n + 1) : (a : (i : Fin (n + 1)) → W) → E)
          (Fin.cons (α := fun (i : Fin (n + 1)) ↦ W) w' m))
      w)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂
      (fun (x : V) ↦
        ((((fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) x :
                    W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
                  (a : W) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) E)
                w' :
              ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
            (a : (i : Fin n) → W) → E)
          m)
      w)

Tactic:
congr with v
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
I₂ :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f v n))
    μ
I₃ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin (n + 1)) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ :
  Integrable (ε := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) μ
w' : W
m : (i : Fin n) → W
v : V
⊢ Eq.{u_1 + 1} (α := E)
    ((fourierPowSMulRight L f v (n + 1) : (a : (i : Fin (n + 1)) → W) → E)
        (Fin.cons (α := fun (i : Fin (n + 1)) ↦ W) w' m) :
      E)
    (((((fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v :
                  W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
                (a : W) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) E)
              w' :
            ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
          (a : (i : Fin n) → W) → E)
        m :
      E)

Tactic:
simp only [fourierPowSMulRight_apply, mul_comm, pow_succ, neg_mul, Fin.prod_univ_succ,
        Fin.cons_zero, Fin.cons_succ, neg_smul, fourierSMulRight_apply, neg_apply, smul_apply,
        smul_comm (M := ℝ) (N := ℂ) (α := E), smul_smul]

Premises used: neg_smul, Fin.cons_succ, pow_succ, ContinuousMultilinearMap.neg_apply, smul_smul, VectorFourier.fourierSMulRight_apply, ContinuousMultilinearMap.smul_apply, Fin.prod_univ_succ, mul_comm, VectorFourier.fourierPowSMulRight_apply, neg_mul, SMulCommClass.smul_comm, Fin.cons_zero
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
I₂ :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f v n))
    μ
I₃ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin (n + 1)) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ :
  Integrable (ε := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) μ
⊢ Eq (α := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin (n + 1)) ↦ W) (G := E)
        (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) w) :
      W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L fun (v : V) ↦ fourierPowSMulRight L f v n) w :
      W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)

Tactic:
have E : curryLeft
          (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun v ↦ fourierPowSMulRight L f v (n + 1)) w) =
        fourierIntegral 𝐞 μ L.toLinearMap₁₂
          (fourierSMulRight L fun v ↦ fourierPowSMulRight L f v n) w := by
      ext w' m
      rw [curryLeft_apply, fourierIntegral_continuousMultilinearMap_apply' I₃,
        fourierIntegral_continuousLinearMap_apply' I₄,
        fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)]
      congr with v
      simp only [fourierPowSMulRight_apply, mul_comm, pow_succ, neg_mul, Fin.prod_univ_succ,
        Fin.cons_zero, Fin.cons_succ, neg_smul, fourierSMulRight_apply, neg_apply, smul_apply,
        smul_comm (M := ℝ) (N := ℂ) (α := E), smul_smul]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℂ E_1
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E_1
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
I₂ :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
          (fourierPowSMulRight L f v n))
    μ
I₃ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin (n + 1)) ↦ W) E_1)
    (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ :
  Integrable (ε := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fun (v : V) ↦ fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) μ
E :
  Eq (α := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin (n + 1)) ↦ W) (G := E_1)
        (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) w) :
      W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L fun (v : V) ↦ fourierPowSMulRight L f v n) w :
      W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E_1)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w

Tactic:
E ▸ hasFDerivAt_fourierIntegral L I₁ I₂ w

Premises used: VectorFourier.hasFDerivAt_fourierIntegral, Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℂ E_1
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E_1
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
I₂ :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
          (fourierPowSMulRight L f v n))
    μ
I₃ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin (n + 1)) ↦ W) E_1)
    (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ :
  Integrable (ε := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fun (v : V) ↦ fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) μ
E :
  Eq (α := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin (n + 1)) ↦ W) (G := E_1)
        (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) w) :
      W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L fun (v : V) ↦ fourierPowSMulRight L f v n) w :
      W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E_1)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E_1)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w

Tactic:
exact E ▸ hasFDerivAt_fourierIntegral L I₁ I₂ w
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : V × W) ↦
    (((L.toLinearMap₁₂ : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2

Tactic:
apply L.continuous₂

Premises used: ContinuousLinearMap.continuous₂
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
cont :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : W) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) x

Tactic:
apply fourierIntegral_continuous Real.continuous_fourierChar (by apply L.continuous₂)

Premises used: VectorFourier.fourierIntegral_continuous, Real.continuous_fourierChar
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ

Tactic:
integrable_fourierPowSMulRight L (hf n hn) h'f

Premises used: VectorFourier.integrable_fourierPowSMulRight
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ

Tactic:
exact integrable_fourierPowSMulRight L (hf n hn) h'f

Premises used: VectorFourier.integrable_fourierPowSMulRight
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ HasFTaylorSeriesUpTo (𝕜 := ℝ) (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) fun (w : W) (n : ℕ) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w

Tactic:
hasFTaylorSeriesUpTo_fourierIntegral _ (fun n hn ↦ hf n (mod_cast hn)) h'f

Premises used: WithTop.coe_le_coe._simp_1, cast, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
pos : ∀ (h'f : Integrable f μ), ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
neg : ∀ (h'f : ¬Integrable f μ), ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)

Tactic:
by_cases h'f : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : Integrable f μ
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)

Tactic:
(hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f.1).contDiff

Premises used: VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', And.left, HasFTaylorSeriesUpTo.contDiff
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : Integrable f μ
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)

Tactic:
exact (hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f.1).contDiff

Premises used: VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', And.left, HasFTaylorSeriesUpTo.contDiff
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : ¬Integrable f μ
h : ∀ (w : W), fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w = 0 w
⊢ fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0

Tactic:
ext w
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : ¬Integrable f μ
w : W
⊢ fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w = 0 w

Tactic:
simp [fourierIntegral, integral, h'f]

Premises used: VectorFourier.fourierIntegral, MeasureTheory.integral
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : ¬Integrable f μ
⊢ fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0

Tactic:
have : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0 := by
      ext w; simp [fourierIntegral, integral, h'f]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : ¬Integrable f μ
this : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)

Tactic:
simpa [this] using contDiff_const

Premises used: contDiff_const
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
h :
  ∀ (w : W),
    Eq (α := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
      (iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w)
⊢ Eq (α := W → ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f))
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ fun (v : V) ↦ fourierPowSMulRight L f v n)

Tactic:
ext w : 1
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞) ≤ N
w : W
⊢ Eq (α := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w)

Tactic:
((hasFTaylorSeriesUpTo_fourierIntegral' L hf h'f).eq_iteratedFDeriv
    (mod_cast hn) w).symm

Premises used: HasFTaylorSeriesUpTo.eq_iteratedFDeriv, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', Eq.symm