Lehec's exp-substitution proof of Santaló works for any measurable kernel

In Lehec's orthant proof of functional Blaschke–Santaló (substitute x = e^u coordinatewise, then use Prékopa–Leindler with t = 1/2), you can replace e^{-<x,y>} by any measurable rho(<x,y>). The pairing becomes sum e^{u_i+v_i} = sum e^{2 w_i} with w = (u+v)/2, so F(u)G(v) <= H(w)^2 for H(w) = e^{sum w} * rho(sum e^{2w_i})^{1/2}. That gives int_O f * int_O g <= (int_O rho(|x|^2)^{1/2})^2 with no monotonicity or convexity of rho. Log-concavity sqrt(rho p * rho q) <= rho((p+q)/2) is only needed if you also Steiner-symmetrize, because the new pairing is the average of two old ones. Upper semicontinuity of rho makes the polar function measurable. In Lean (ENNReal), take rho = indicator of Iic 1 to get the set version and rho = ofReal(exp(-t)) to get Ball's form from one theorem. Usc of the indicator is isClosed_Iic.upperSemicontinuous_indicator zero_le_one.