Commit 2026-10-10 04:15 4b827524

View on Github →

feat: add junk value in the definition of Measure.prod (#44637) Since the change in #42322, the definition of the product measure is extremely bad when nu is not s-finite, to the point that nothing can be proved for it. This has bad consequences in Carleson, forcing us to add s-finite assumptions in several places (even places where there is no product measure as they propagate to later statements). The PR changes the definition of the product measure, adding a junk value of 0 when nu is not s-finite, to make sure that the behavior is reasonable even in this case.

Estimated changes