Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand (ForML/SchwartzRealFourier.lean)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Tactic:
have := intervalIntegral.integral_deriv_smul_eq_sub (a := a) (b := b)
  (u := fun x ↦ Real.fourierChar[-(x * ξ)])
  (v := fun x ↦ f x)
  (u' := fun x ↦ (-ξ) • (2 * π * I * Real.fourierChar[-(x * ξ)]))
  (v' := fun x ↦ deriv f x)
  (fun x _ ↦ .comp_of_tower x (Real.hasDerivAt_fourierChar _) (hasDerivAt_mul_const ξ).neg)
  (fun x _ ↦ f.differentiableAt.hasDerivAt)
  (Continuous.continuousOn <|
    .const_smul (.mul continuous_const (continuous_mul_right ξ).neg.realFourierChar) _)
  (by simpa [derivCLM_apply ℝ] using (derivCLM ℝ f).continuous.continuousOn)
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (fun x => -ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) x • (fun x => f x) x +
        (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) x • (fun x => deriv (⇑f) x) x =
    (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) b • (fun x => f x) b -
      (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) a • (fun x => f x) a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (fun x => -ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) x • (fun x => f x) x +
        (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) x • (fun x => deriv (⇑f) x) x =
    (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) b • (fun x => f x) b -
      (fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) a • (fun x => f x) a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Tactic:
simp only at this
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
Tactic:
rw [← this]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ ∫ (x : ℝ) in a..b,
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
Tactic:
refine intervalIntegral.integral_congr ?_
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ Set.EqOn
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    (fun x =>
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
    (Set.uIcc a b)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
⊢ Set.EqOn
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    (fun x =>
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
    (Set.uIcc a b)
Tactic:
intro x _
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (fun x =>
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
      x =
    (fun x =>
        (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
      x

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (fun x =>
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
      x =
    (fun x =>
        (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
      x
Tactic:
simp only
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
      (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
      (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
Tactic:
rw [sub_eq_neg_add, add_left_inj]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ -((2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x) =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ -((2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x) =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Tactic:
simp only [neg_smul, neg_inj]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Tactic:
rw [Complex.real_smul, smul_smul]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) • f x =
    (↑ξ * (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) • f x =
    (↑ξ * (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Tactic:
exact congrArg₂ _ (by ring) rfl
State after:
no goals

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
⊢ ContinuousOn (fun x => deriv (⇑f) x) (Set.uIcc a b)
Tactic:
simpa [derivCLM_apply ℝ] using (derivCLM ℝ f).continuous.continuousOn
State after:
no goals

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ 2 * ↑π * I * ↑ξ * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) =
    ↑ξ * (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))
Tactic:
ring
State after:
no goals