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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
I₁ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
          fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ n - i ≤ n

Tactic:
lia
-- 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
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
I₁ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
          fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
i : ℕ
hi : i ∈ Finset.range (k + 1)
⊢ ‖v‖ ^ (n - i) *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin (k - i)) ↦ V) E)
        (iteratedFDeriv ℝ (k - i) f v) ≤
    C

Tactic:
exact hv _ (by lia) _ (by lia)
-- 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
hf : AEStronglyMeasurable f μ
n : ℕ
simp_rw :
  AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E) ((-(2 * (↑π : ℂ) * I)) ^ n)
        (((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
                  (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                    E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                      (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                    (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
                  fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
            (f v) :
          ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E))
    μ
⊢ AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ VectorFourier.fourierPowSMulRight L f v n) μ

Tactic:
simp_rw [fourierPowSMulRight_eq_comp]

Premises used: VectorFourier.fourierPowSMulRight_eq_comp
-- 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
hf : AEStronglyMeasurable f μ
n : ℕ
hf₁ :
  AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (x : V) ↦
      ((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
              (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
            ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
              fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x) :
          (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
        (f x))
    μ
⊢ AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E) ((-(2 * (↑π : ℂ) * I)) ^ n)
        (((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
                  (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                    E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                      (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                    (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
                  fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) :
              (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
            (f v) :
          ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E))
    μ

Tactic:
apply AEStronglyMeasurable.const_smul'

Premises used: MeasureTheory.AEStronglyMeasurable.const_smul'
-- 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
hf : AEStronglyMeasurable f μ
n : ℕ
apply :
  AEStronglyMeasurable.{u_2, u_3} (β := ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
    (fun (x : V) ↦
      (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
            (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
          (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
        fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x)
    μ
⊢ AEStronglyMeasurable (β := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (x : V) ↦
      ((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
              (a : ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ) →
                E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
            ((compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
                  (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
                (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
              fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x) :
          (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
        (f x))
    μ

Tactic:
apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp_aestronglyMeasurable₂ _ hf

Premises used: ContinuousLinearMap.continuous₂, Real, ContinuousMultilinearMap.smulRightL, Continuous.comp_aestronglyMeasurable₂
-- 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
hf : AEStronglyMeasurable f μ
n : ℕ
hf₁ :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : V) ↦
    (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
      fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x
⊢ AEStronglyMeasurable.{u_2, u_3} (β := ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
    (fun (x : V) ↦
      (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
            (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
          (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
        fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x)
    μ

Tactic:
apply Continuous.aestronglyMeasurable

Premises used: Continuous.aestronglyMeasurable
-- 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
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : V) ↦
    (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
      fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x

Tactic:
Continuous.comp (map_continuous _) (continuous_pi (fun _ ↦ L.continuous))

Premises used: Continuous.comp, continuous_pi, ContinuousLinearMap.continuous, ContinuousMapClass.map_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
hf : AEStronglyMeasurable f μ
n : ℕ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : V) ↦
    (compContinuousLinearMapLRight (E := fun (x : Fin n) ↦ W) (E₁ := fun (x : Fin n) ↦ ℝ)
          (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ) :
        (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ)
      fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x

Tactic:
exact Continuous.comp (map_continuous _) (continuous_pi (fun _ ↦ L.continuous))

Premises used: Continuous.comp, continuous_pi, ContinuousLinearMap.continuous, ContinuousMapClass.map_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 : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
⊢ Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ

Tactic:
(hf.const_mul ((2 * π * ‖L‖) ^ n)).mono' (h'f.fourierPowSMulRight L n) ?_

Premises used: Norm.norm, Real.pi, HMul.hMul, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight, HPow.hPow, OfNat.ofNat
-- 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 : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
refine :
  ∀ᵐ (a : V) ∂μ,
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f a n) ≤
      (2 * π * ‖L‖) ^ n * (‖a‖ ^ n * ‖f a‖)
⊢ Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ

Tactic:
refine (hf.const_mul ((2 * π * ‖L‖) ^ n)).mono' (h'f.fourierPowSMulRight L n) ?_

Premises used: Norm.norm, Real.pi, HMul.hMul, MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.mono', MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight, HPow.hPow, OfNat.ofNat
-- 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 : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
h :
  ∀ (v : V),
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
      (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖f v‖)
⊢ ∀ᵐ (a : V) ∂μ,
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f a n) ≤
      (2 * π * ‖L‖) ^ n * (‖a‖ ^ n * ‖f a‖)

Tactic:
filter_upwards 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 : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
v : V
⊢ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ = (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖f v‖)

Tactic:
ring
-- 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 : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
v : V
⊢ Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) (fourierPowSMulRight L f v n) ≤
    (2 * π * ‖L‖) ^ n * (‖v‖ ^ n * ‖f v‖)

Tactic:
exact (norm_fourierPowSMulRight_le L f v n).trans (le_of_eq (by ring))

Premises used: VectorFourier.norm_fourierPowSMulRight_le, LE.le.trans, le_of_eq
-- 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 μ
zero_eq :
  ∀ (x : W),
    curry0.{0, u_3, u_1} (𝕜 := ℝ) (G := W)
        (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v 0) x) =
      fourierIntegral 𝐞 μ L.toLinearMap₁₂ f x
fderiv :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) < N →
      ∀ (x : W),
        HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin m) ↦ W) E)
          (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m) y)
          (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin m.succ) ↦ W) (G := E)
            (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m.succ) x))
          x
cont :
  ∀ (m : ℕ),
    (↑m : ℕ∞ω) ≤ N →
      Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : W) ↦
        fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v m) x
⊢ HasFTaylorSeriesUpTo (𝕜 := ℝ) N (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) fun (w : W) (n : ℕ) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w

Tactic:
constructor
-- 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 μ
w : W
zero_eq :
  fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (x : V) ↦ (fourierPowSMulRight L f x 0 : (a : (i : Fin 0) → W) → E) ![]) w =
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w
⊢ curry0.{0, u_3, u_1} (𝕜 := ℝ) (G := W)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v 0) w) =
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w

Tactic:
rw [curry0_apply, Matrix.zero_empty, fourierIntegral_continuousMultilinearMap_apply'
      (integrable_fourierPowSMulRight L (hf 0 bot_le) h'f)]

Premises used: ContinuousMultilinearMap.curry0_apply, OfNat.ofNat, VectorFourier.integrable_fourierPowSMulRight, bot_le, Matrix.zero_empty, Real.fourierIntegral_continuousMultilinearMap_apply'
-- 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 μ
w : W
⊢ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (x : V) ↦ (fourierPowSMulRight L f x 0 : (a : (i : Fin 0) → W) → E) ![]) w =
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w

Tactic:
simp only [fourierPowSMulRight_apply, pow_zero, Finset.univ_eq_empty, Finset.prod_empty,
      one_smul]

Premises used: Finset.prod_empty, Finset.univ_eq_empty, pow_zero, one_smul, VectorFourier.fourierPowSMulRight_apply