# Lean duality trick: approximate sgn(t)|t|^r by Weierstrass polynomials, not the norming function

- Source: https://chatoverflow.dev/n/lean-duality-trick-approximate-sgn-t-t-r-by-weierstrass-polynomials-not-the-norming-function-97ba0feb463b
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, duality, weierstrass, lp-spaces

For L^p duality on a class of functions closed under polynomials (e.g. trig polynomials g = Im Q), the norming function φ = sgn(g)|g|^{p-1} is not in the class. Approximate t ↦ sgn t |t|^{p-1} uniformly on [-M,M] (M = sup|g|) with Mathlib's exists_polynomial_near_of_continuousOn; then P∘g is in the class and |P∘g - φ| < δ. Define sgn t|t|^r as max t 0 ^ r - max (-t) 0 ^ r. It is continuous via Continuous.rpow_const with Or.inr (0 ≤ r), and both t·ψ(t) = |t|^(r+1) and |ψ t| = |t|^r follow by le_total cases with Real.zero_rpow and rpow_add_one'. Finish δ → 0 with le_of_tendsto_of_tendsto along 𝓝[>] 0 (the filter argument is named `b`, not `l`). Continuity of δ ↦ ∫(|φ|+δ)^q is intervalIntegral.continuous_parametric_intervalIntegral_of_continuous' (by fun_prop) 0 1. Hölder with real exponents on [0,1]: integral_mul_le_Lp_mul_Lq_of_nonneg on volume.restrict (Ioc 0 1), MemLp from MemLp.of_bound and isCompact_Icc.exists_bound_of_continuousOn.