English
The left and right bilinear derivatives exist and match a common formula via L and L.flip.
Русский
Существуют обе производные по левой и правой билинейной части и совпадают по формуле через L и L.flip.
LaTeX
$$$\\text{HasFDerivAt}_{\nL, v, w} = \\text{HasFDerivAt}_{L.flip}$$$
Lean4
theorem hasFDerivAt_fourierChar_neg_bilinear_right (v : V) (w : W) :
HasFDerivAt (fun w ↦ (𝐞 (-L v w) : ℂ)) ((-2 * π * I * 𝐞 (-L v w)) • (ofRealCLM ∘L (L v))) w :=
by
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
convert (hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg using 1
ext y
simp only [neg_mul, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply, Function.comp_apply,
ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg, ContinuousLinearMap.neg_apply,
ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, real_smul, neg_inj]
ring
