Commit 2026-07-02 09:24 40b45a06

feat: generalize some lemmas by using conditional Jensen (#36888) This PR includes two possible ways of generalizing integral_abs_condExp_le:

1. Replace absolute values with norms.
2. Consider absolute values defined on a lattice with a solid norm. We also prove that if a function is in Lp then its conditional expectation is also in Lp. In order to prove these results, some of the lemmas about essSup are generalized to conditionally complete lattices. Created with the help of Codex.