Theorem ContinuousLinearMap.memLp_of_bilin

Modification history

2025-09-29 20:43
Mathlib/MeasureTheory/Function/Holder.lean
feat(SchwartzSpace): integration by parts in 1d (#29846)
Added ContinuousLinearMap.memLp_of_bilinView on Github →