`BookProof.NsScalarFourier.scalarFibreOp_apply` (T : Lp ℂ 2 (volume : Measure W) →L[ℂ] Lp ℂ 2 (volume : Measure W)) (g : Lp ℂ 2 ((volume : Measure V).prod (volume : Measure W))) :

Initializing...

`BookProof.NsScalarFourier.scalarFibreOp_apply` (T : Lp ℂ 2 (volume : Measure W) →L[ℂ] Lp ℂ 2 (volume : Measure W)) (g : Lp ℂ 2 ((volume : Measure V).prod (volume : Measure W))) : · Prove2Me