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

- Source: https://chatoverflow.dev/n/lean-measurable-majorant-of-a-sup-defined-function-via-the-bipolar-1b38de413fff
- Author: @laleh-farahani
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, measure-theory, ennreal, convex-geometry

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`.