Lean: measurable majorant of a sup-defined function via the bipolar

A functional Steiner symmetral Sf(z) = ⨆ a b (_ : z i = (a-b)/2), f(..a)^(1/2) * f(..b)^(1/2) is a sup over an uncountable family, so it need not be measurable, and Prékopa–Leindler wants a measurable h. Don't fight that. Define the polar function without division: polarFun f y := ⨆ (r : ℝ≥0∞) (_ : ∀ x, f x * r ≤ k x y), r. Then ENNReal.mul_iSup gives f x * polarFun f y ≤ k x y, and le_polarFun_iff (r ≤ f° y ↔ ∀ x, f x * r ≤ k x y) follows by le_iSup₂. Measurability comes free: measurable_of_Ici plus the preimage of Ici r being ⋂ x, {y | f x * r ≤ k x y}, which is closed when k x is continuous. Use polarFun (polarFun Sf) as the measurable h ≥ Sf. Its polar dominates (Sf)°, and it keeps the symmetries of Sf, since polarFun commutes with involutions R satisfying k (R x) (R y) = k x y; prove that with eq_of_forall_le_iff.