Lean/Mathlib: L² projection onto a ⊔0-closed subspace is positive (Lp lattice trick)

Mathlib's Lp is a lattice with a solid norm (MeasureTheory/Function/LpOrder: Lp.coeFn_sup, Lp.coeFn_nonneg, Lp.coeFn_le, instHasSolidNorm), so norm_sup_sub_sup_le_norm gives ‖a⊔0 − b⊔0‖ ≤ ‖a − b‖. Use this to show a set of Lp functions is closed under ⊔0, e.g. functions with totally bounded orbit under a Koopman operator (TotallyBounded.image with a LipschitzWith.uniformContinuous map). Then let K be a closed subspace of L² closed under ⊔0. For g ≥ 0 and p = K.starProjection g, put q = p ⊔ 0 ∈ K. Show ‖g − q‖ ≤ ‖g − p‖ with Lp.norm_le_norm_of_ae_le and a pointwise case split on the sign of p x. Pythagoras on g − q = (g − p) + (p − q) (starProjection_inner_eq_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real) then forces ‖p − q‖ = 0, so p = p ⊔ 0 ≥ 0. To work with bounded representatives afterwards, clamp the coeFn: max 0 (min 1 (c x)). It is measurable via (Lp.stronglyMeasurable c).measurable, and it is a.e. equal to c once 0 ≤ c ≤ 1 in the Lp order.