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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
w' : W
⊢ ((↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        ((↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
          -(2 * (↑π : ℂ) * I))) •
      f v =
    (-(↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        (2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))) •
      f v

Tactic:
ring_nf
-- 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
v : V
hbc : Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖
⊢ 2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖ ≤
    2 * π * (‖L‖ * ‖v‖) * ‖f v‖

Tactic:
gcongr
-- 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
v : V
⊢ Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖

Tactic:
L.le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
v : V
⊢ Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖

Tactic:
exact L.le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm
-- 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
v : V
⊢ 2 * π * (‖L‖ * ‖v‖) * ‖f v‖ = 2 * π * ‖L‖ * ‖v‖ * ‖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
inst_6 : SecondCountableTopologyEither.{u_2, u_3} V (W →L[ℝ] ℝ)
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
hf₁ :
  AEStronglyMeasurable (β := W →L[ℝ] E)
    (fun (x : V) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) x) (f x)) μ
⊢ AEStronglyMeasurable (β := W →L[ℝ] E) (fun (v : V) ↦ VectorFourier.fourierSMulRight L f v) μ

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
inst_6 : SecondCountableTopologyEither.{u_2, u_3} V (W →L[ℝ] ℝ)
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) ↦ p.1.smulRight p.2

Tactic:
have aux0 : Continuous fun p : (W →L[ℝ] ℝ) × E ↦ p.1.smulRight p.2 :=
    (ContinuousLinearMap.smulRightL ℝ W E).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
inst_6 : SecondCountableTopologyEither.{u_2, u_3} V (W →L[ℝ] ℝ)
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous[instTopologicalSpaceProd, _] fun (p : Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) ↦ p.1.smulRight p.2
⊢ AEStronglyMeasurable (β := Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) (fun (v : V) ↦ ((L : (a : V) → W →L[ℝ] ℝ) v, f v)) μ

Tactic:
have aux1 : AEStronglyMeasurable (fun v ↦ (L v, f v)) μ :=
    L.continuous.aestronglyMeasurable.prodMk hf
-- 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
inst_6 : SecondCountableTopologyEither.{u_2, u_3} V (W →L[ℝ] ℝ)
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous[instTopologicalSpaceProd, _] fun (p : Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) ↦ p.1.smulRight p.2
aux1 : AEStronglyMeasurable (β := Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) (fun (v : V) ↦ ((L : (a : V) → W →L[ℝ] ℝ) v, f v)) μ
⊢ AEStronglyMeasurable (β := W →L[ℝ] E)
    (fun (x : V) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) x) (f x)) μ

Tactic:
(aux0.comp_aestronglyMeasurable aux1 :)

Premises used: 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
inst_6 : SecondCountableTopologyEither.{u_2, u_3} V (W →L[ℝ] ℝ)
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
μ : Measure V
hf : AEStronglyMeasurable f μ
aux0 : Continuous[instTopologicalSpaceProd, _] fun (p : Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) ↦ p.1.smulRight p.2
aux1 : AEStronglyMeasurable (β := Prod.{u_3, u_1} (W →L[ℝ] ℝ) E) (fun (v : V) ↦ ((L : (a : V) → W →L[ℝ] ℝ) v, f v)) μ
⊢ AEStronglyMeasurable (β := W →L[ℝ] E)
    (fun (x : V) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) x) (f x)) μ

Tactic:
exact (aux0.comp_aestronglyMeasurable aux1 :)

Premises used: 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
w' : W
⊢ 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
⊢ ∀ (w' : W), Integrable (F w') μ

Tactic:
have h0 (w' : W) : Integrable (F w') μ :=
    (fourierIntegral_convergent_iff continuous_fourierChar
      (by apply L.continuous₂ : Continuous (fun p : V × W ↦ L.toLinearMap₁₂ p.1 p.2)) w').2 hf
-- 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
⊢ ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ

Tactic:
have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ :=
    Eventually.of_forall (fun w' ↦ (h0 w').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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ AEStronglyMeasurable (F' w) μ

Tactic:
.smul ?_ hf.1.fourierSMulRight

Premises used: MeasureTheory.AEStronglyMeasurable.fourierSMulRight, And.left, MeasureTheory.AEStronglyMeasurable.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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
refine :
  AEStronglyMeasurable (β := Circle)
    (fun (v : V) ↦ (𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) μ
⊢ AEStronglyMeasurable (F' w) μ

Tactic:
refine .smul ?_ hf.1.fourierSMulRight
-- 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ AEStronglyMeasurable (β := Circle)
    (fun (v : V) ↦ (𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) μ

Tactic:
(continuous_fourierChar.comp ?_).aestronglyMeasurable

Premises used: Continuous.comp, Real.continuous_fourierChar, 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
refine :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : V) ↦
    -(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w
⊢ AEStronglyMeasurable (β := Circle)
    (fun (v : V) ↦ (𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) μ

Tactic:
refine (continuous_fourierChar.comp ?_).aestronglyMeasurable

Premises used: Continuous.comp, Real.continuous_fourierChar, 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : V) ↦
    -(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w

Tactic:
fun_prop
-- 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
⊢ AEStronglyMeasurable (F' w) μ

Tactic:
have h3 : AEStronglyMeasurable (F' w) μ := by
    refine .smul ?_ hf.1.fourierSMulRight
    refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
    fun_prop
-- 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
h : w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v
⊢ w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v

Tactic:
_
-- 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
h : ∀ (v : V), ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v

Tactic:
filter_upwards with v 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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
h_1 : w' ∈ Metric.ball w 1
h : Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) ≤ B v
⊢ ‖F' w' v‖ ≤ B v

Tactic:
rw [Circle.norm_smul _ (fourierSMulRight L f v)]

Premises used: VectorFourier.fourierSMulRight, Circle.norm_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
inst_8 : SecondCountableTopology V
μ : Measure V
hf : Integrable f μ
hf' : Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ * ‖f v‖) μ
w : W
F : W → V → E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v)
F' : W → V → W →L[ℝ] E :=
  fun (w' : W) (v : V) ↦
    HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle)
      (fourierSMulRight L f v)
B : V → ℝ := fun (v : V) ↦ 2 * π * ‖L‖ * ‖v‖ * ‖f v‖
h0 : ∀ (w' : W), Integrable (F w') μ
h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
h3 : AEStronglyMeasurable (F' w) μ
v : V
w' : W
h : w' ∈ Metric.ball w 1
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) ≤ B v

Tactic:
norm_fourierSMulRight_le L f v

Premises used: VectorFourier.norm_fourierSMulRight_le