Commit 2023-08-13 09:51 640038f3

View on Github →

chore(LpSpace): golf, generalize (#6553)

  • drop mostly unused section variables;
  • generalize MeasureTheory.lintegral_indicator_const and MeasureTheory.snorm_indicator_const to a NullMeasurableSet;
  • golf a proof.

Estimated changes