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
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hvf_int : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : V) ↦ ‖v‖ * ‖f v‖) volume
x : V
⊢ HasFDerivAt (𝓕 f) (𝓕 (E := (v : V) → V →L[ℝ] E) (fourierSMulRight (innerSL ℝ) f) x) x

Tactic:
VectorFourier.hasFDerivAt_fourierIntegral (innerSL ℝ) hf_int hvf_int x

Premises used: Real, innerSL, VectorFourier.hasFDerivAt_fourierIntegral, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hvf_int : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : V) ↦ ‖v‖ * ‖f v‖) volume
⊢ fderiv ℝ (𝓕 f) = 𝓕 (E := (v : V) → V →L[ℝ] E) (fourierSMulRight (innerSL ℝ) f)

Tactic:
VectorFourier.fderiv_fourierIntegral (innerSL ℝ) hf_int hvf_int

Premises used: Real, innerSL, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, VectorFourier.fderiv_fourierIntegral, innerₛₗ, RingHomClass.toRingHom, starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf_int : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hvf_int : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : V) ↦ ‖v‖ * ‖f v‖) volume
⊢ Differentiable ℝ (𝓕 f)

Tactic:
VectorFourier.differentiable_fourierIntegral (innerSL ℝ) hf_int hvf_int

Premises used: Real, innerSL, VectorFourier.differentiable_fourierIntegral, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable (V →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fderiv ℝ f) volume
rw : 𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ f) = fourierSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f)
⊢ 𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ f) = fourierSMulRight (-innerSL ℝ) (𝓕 f)

Tactic:
rw [← flip_innerSL_real V]

Premises used: flip_innerSL_real
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable (V →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fderiv ℝ f) volume
⊢ 𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ f) = fourierSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f)

Tactic:
VectorFourier.fourierIntegral_fderiv (innerSL ℝ) hf h'f hf'

Premises used: Real, innerSL, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, starRingEnd, VectorFourier.fourierIntegral_fderiv, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
h'f : Differentiable ℝ f
hf' : @Integrable (V →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fderiv ℝ f) volume
⊢ 𝓕 (E := (x : V) → V →L[ℝ] E) (fderiv ℝ f) = fourierSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f)

Tactic:
exact VectorFourier.fourierIntegral_fderiv (innerSL ℝ) hf h'f hf'

Premises used: Real, innerSL, VectorFourier.fourierIntegral_fderiv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable ℝ _ _ _ inst_5 (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) (volume : Measure V)
⊢ ContDiff ℝ (↑N : ℕ∞ω) (𝓕 f)

Tactic:
VectorFourier.contDiff_fourierIntegral (innerSL ℝ) hf

Premises used: Real, innerSL, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, VectorFourier.contDiff_fourierIntegral, RingHomClass.toRingHom, starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
N : ℕ∞
hf : ∀ (n : ℕ), (↑n : ℕ∞) ≤ N → @Integrable ℝ _ _ _ inst_5 (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) (volume : Measure V)
h'f : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f volume
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ iteratedFDeriv ℝ n (𝓕 f) =
    𝓕 (E := (v : V) → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) fun (v : V) ↦
      fourierPowSMulRight (innerSL ℝ) f v n

Tactic:
VectorFourier.iteratedFDeriv_fourierIntegral (innerSL ℝ) hf h'f hn

Premises used: Real, innerSL, VectorFourier.iteratedFDeriv_fourierIntegral, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) _ _ _ inst_5
        (iteratedFDeriv ℝ n f) (volume : Measure V)
n : ℕ
hn : (↑n : ℕ∞) ≤ N
rw :
  𝓕 (E := V → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) =
    fun (w : V) ↦ fourierPowSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f) w n
⊢ 𝓕 (E := V → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) =
    fun (w : V) ↦ fourierPowSMulRight (-innerSL ℝ) (𝓕 f) w n

Tactic:
rw [← flip_innerSL_real V]

Premises used: flip_innerSL_real
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) _ _ _ inst_5
        (iteratedFDeriv ℝ n f) (volume : Measure V)
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ 𝓕 (E := V → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) =
    fun (w : V) ↦ fourierPowSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f) w n

Tactic:
VectorFourier.fourierIntegral_iteratedFDeriv (innerSL ℝ) hf h'f hn

Premises used: Real, innerSL, VectorFourier.fourierIntegral_iteratedFDeriv, MonoidHomClass.toMonoidHom, LinearMap.mk₂'ₛₗ, innerₛₗ, RingHomClass.toRingHom, starRingEnd, innerₗ
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      @Integrable (ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) _ _ _ inst_5
        (iteratedFDeriv ℝ n f) (volume : Measure V)
n : ℕ
hn : (↑n : ℕ∞) ≤ N
⊢ 𝓕 (E := V → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) =
    fun (w : V) ↦ fourierPowSMulRight (-ContinuousLinearMap.flip (innerSL ℝ)) (𝓕 f) w n

Tactic:
exact VectorFourier.fourierIntegral_iteratedFDeriv (innerSL ℝ) hf h'f hn

Premises used: Real, innerSL, VectorFourier.fourierIntegral_iteratedFDeriv
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
⊢ HPow.hPow (α := ℝ) (|(((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) w : V →L[ℝ] ℝ) : (a : V) → ℝ) w| : ℝ) n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f)
          w) ≤
    ‖w‖ ^ n * (2 * π * Norm.norm.{u_2} (E := V →L[ℝ] V →L[ℝ] ℝ) (innerSL ℝ)) ^ k *
        (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ inst_5 (volume : Measure V) fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)

Tactic:
have := VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le (innerSL ℝ) hf h'f hk hn
      w w
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
this :
  HPow.hPow (α := ℝ) (|(((innerSL ℝ : (a : V) → V →L[ℝ] ℝ) w : V →L[ℝ] ℝ) : (a : V) → ℝ) w| : ℝ) n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f)
          w) ≤
    ‖w‖ ^ n * (2 * π * Norm.norm.{u_2} (E := V →L[ℝ] V →L[ℝ] ℝ) (innerSL ℝ)) ^ k *
        (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ inst_5 (volume : Measure V) fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)
⊢ HPow.hPow (β := ℕ) ‖w‖ 2 ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (fourierIntegral 𝐞 (volume : Measure V) (ContinuousLinearMap.toLinearMap₁₂ (innerSL ℝ)) f)
          w) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ inst_5 (volume : Measure V) fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))

Tactic:
simp only [innerSL_apply_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
      mul_assoc] at this

Premises used: innerSL_apply_apply, mul_assoc, real_inner_self_eq_norm_sq, abs_norm, abs_pow
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn : (↑n : ℕ∞) ≤ N
w : V
⊢ ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))

Tactic:
have Z : ‖w‖ ^ n * (‖w‖ ^ n * ‖iteratedFDeriv ℝ k (𝓕 f) w‖) ≤
      ‖w‖ ^ n * ((2 * (π * ‖innerSL (E := V) ℝ‖)) ^ k * ((2 * k + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂volume)) := by
    have := VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le (innerSL ℝ) hf h'f hk hn
      w w
    simp only [innerSL_apply_apply _ w w, real_inner_self_eq_norm_sq w, abs_pow, abs_norm,
      mul_assoc] at this
    rwa [pow_two, mul_pow, mul_assoc] at this
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  HPow.hPow (β := ℕ) ‖w‖ 0 *
      (HPow.hPow (β := ℕ) ‖w‖ 0 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    HPow.hPow (β := ℕ) ‖w‖ 0 *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) 0 *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
inl :
  ∀
    (Z :
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w) ≤
        (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
          ∑ x ∈ Finset.range (k + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖),
    Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
      (2 * π) ^ k *
        ∑ x ∈ Finset.range (k + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
⊢ HPow.hPow (β := ℕ) ‖w‖ 0 *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * π) ^ k * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) 0 *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (HAdd.hAdd (α := ℕ) 0 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)

Tactic:
simp only [pow_zero, one_mul, mul_one, zero_add, Finset.range_one, Finset.product_singleton,
      Finset.sum_map, Function.Embedding.coeFn_mk, norm_iteratedFDeriv_zero] at Z ⊢

Premises used: Finset.product_singleton, Finset.sum_map, zero_add, pow_zero, Function.Embedding.coeFn_mk, Finset.range_one, mul_one, norm_iteratedFDeriv_zero, one_mul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
inl :
  ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖) ≤
    (2 * π) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
⊢ Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * π) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖

Tactic:
apply Z.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
rw :
  (2 * (π * 1)) ^ k *
    ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
| (2 * π) ^ k *
    ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖

Tactic:
rw [← mul_one π]

Premises used: Real.pi, mul_one
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
inl :
  ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖) ≤
    (2 * (π * 1)) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
⊢ ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖) ≤
    (2 * π) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖

Tactic:
conv_rhs => rw [← mul_one π]

Premises used: Real.pi, mul_one
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
inl : Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ) ≤ 1
⊢ ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖) ≤
    (2 * (π * 1)) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖

Tactic:
gcongr