awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₃ :
  ‖2 * (↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₄ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₅ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * 1 *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₆ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₇ :
  Norm.norm (E := ℂ) 2 * π *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₈ : 2 * π * Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₃ :
  ‖2 * (↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₄ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₅ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * 1 *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₆ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₇ :
  Norm.norm (E := ℂ) 2 * π *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₈ :
  2 * π * Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₉ : 2 * π * (Norm.norm.{u_3} (E := StrongDual ℝ W) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖ ≤
    2 * π * (‖L‖ * ‖v‖) * ‖f v‖
have hbc : Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) ≤ ‖L‖ * ‖v‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 μ
⊢ AEStronglyMeasurable (β := W →L[ℝ] E) (fun (v : V) ↦ VectorFourier.fourierSMulRight L f v) μ
have hf₁ : AEStronglyMeasurable (β := W →L[ℝ] E)
  (fun (x : V) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) x) (f x)) μ
Tactic: apply AEStronglyMeasurable.const_smul'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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 μ
⊢ AEStronglyMeasurable (β := W →L[ℝ] E)
    (fun (x : V) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) x) (f x)) μ
have aux0 : 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₂
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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 (β := W →L[ℝ] E)
    (fun (x : V) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) x) (f x)) μ
have aux1 : 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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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‖
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w
have h0 : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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') μ
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w
have h1 : ∀ᶠ (w' : W) in 𝓝 w, AEStronglyMeasurable (F w') μ
Tactic: have h1 : ∀ᶠ w' in 𝓝 w, AEStronglyMeasurable (F w') μ :=
    Eventually.of_forall (fun w' ↦ (h0 w').aestronglyMeasurable)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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) μ
have refine : AEStronglyMeasurable (β := Circle)
  (fun (v : V) ↦ (𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) μ
Tactic: refine .smul ?_ hf.1.fourierSMulRight
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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)) μ
have refine : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : V) ↦
  -(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w
Tactic: refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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') μ
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w
have h3 : AEStronglyMeasurable (F' w) μ
Tactic: have h3 : AEStronglyMeasurable (F' w) μ := by
    refine .smul ?_ hf.1.fourierSMulRight
    refine (continuous_fourierChar.comp ?_).aestronglyMeasurable
    fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
have h : ∀ (v : V), ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
Tactic: filter_upwards with v w' _
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
have h : Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) ≤ B v
Tactic: rw [Circle.norm_smul _ (fourierSMulRight L f v)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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) μ
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w
have h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
Tactic: have h4 : (∀ᵐ v ∂μ, ∀ (w' : W), w' ∈ Metric.ball w 1 → ‖F' w' v‖ ≤ B v) := by
    filter_upwards with v w' _
    rw [Circle.norm_smul _ (fourierSMulRight L f v)]
    exact norm_fourierSMulRight_le L f v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w
have h5 : Integrable B μ
Tactic: have h5 : Integrable B μ := by simpa only [← mul_assoc] using hf'.const_mul (2 * π * ‖L‖)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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) μ
h4 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, ‖F' w' v‖ ≤ B v
h5 : Integrable B μ
⊢ HasFDerivAt (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L f) w) w
have h6 : ∀ᵐ (v : V) ∂μ, ∀ w' ∈ Metric.ball w 1, HasFDerivAt (fun (x : W) ↦ F x v) (F' w' v) w'
Tactic: have h6 : ∀ᵐ v ∂μ, ∀ w', w' ∈ Metric.ball w 1 → HasFDerivAt (fun x ↦ F x v) (F' w' v) w' :=
    ae_of_all _ (fun v w' _ ↦ hasFDerivAt_fourierChar_smul L f v w')