`BookProof.NsPartialFourier.partialFourier_norm` (v : Lp F 2 (volume : Measure V)) : ‖partialFourier V F v‖ = ‖v‖

Initializing...

`BookProof.NsPartialFourier.partialFourier_norm` (v : Lp F 2 (volume : Measure V)) : ‖partialFourier V F v‖ = ‖v‖ · Prove2Me