Commit 2026-10-06 11:24 6036e0e7

chore: extend L^p lemmas from normed spaces to enormed setting (#43834) In the refactor of eLpNorm in #42406, I adapted some lemmas in LpSemiNorm.CompareExp to the new setting by adding a continuity assumption. It turns out that this assumption is too strong for some applications in Carleson. This PR proves more general versions of the lemmas, suitable for Carleson. The lemmas are of the form eLpNorm (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm f p μ * eLpNorm g q μ when ‖b (f x) (g x)‖ ≤ c * ‖f x‖ * ‖g x‖ (where the norm could also be an nnnorm or an enorm). They were only proved in normed spaces. The PR proves versions in enormed spaces. The main new application is the inequality eLpNorm (f * g) r μ ≤ eLpNorm f p μ * eLpNorm g q μ when f and g take values in ENNReal. I tried to be coherent, with lemmas named ..._of_pos when they assume that r is positive, with of_enorm when the assumption is in terms of enorms, and of_norm when it's in terms of norms. Now, the main statements are the enorms ones, and the other statements are deduced from the enorms ones. I have not removed any statement, but I have renamed those that were not following this convention. The PR is maybe hard to review because of this, but the changes are mostly mechanical. I have tried hard to avoid measurability assumptions when they were not necessary.