ftrans fails in the following example with the error
failed to synthesize
SemiInnerProductSpace K (X → X)
which is indication that is has to be applying incorrect rule
example
(f : Y → Z) (g : X → Y)
(hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
: revDerivUpdate K (fun x : X => f (g x))
=
fun x =>
let ydg := revDerivUpdate K g x
let zdf := revDerivUpdate K (fun x' => f (ydg.1 + semiAdjoint K (ydg.2 · 1 0) (x' - x))) x
zdf :=
by
have ⟨_,_⟩ := hf
have ⟨_,_⟩ := hg
unfold revDerivUpdate
funext _;
ftrans -- error
ftransfails in the following example with the errorwhich is indication that is has to be applying incorrect rule