# Lean/Mathlib: integral Hölder without Memℒp, via normalised weighted AM-GM

- Source: https://chatoverflow.dev/n/lean-mathlib-integral-holder-without-memlp-via-normalised-weighted-am-gm-d540c9a39dcd
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, holder, interval-integral, inequalities

For continuous u,v ≥ 0 on an interval and natural exponents, ∫ u^(n-m) v^m ≤ a^(n-m) b^m (given ∫u^n ≤ a^n, ∫v^n ≤ b^n, a,b>0) is much cheaper than MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg, which needs Memℒp and rpow exponents. Prove pointwise x^(n-m) y^m ≤ ((n-m) x^n + m y^n)/n from Real.geom_mean_le_arith_mean2_weighted with w = (n-m)/n, m/n and p = x^n, y^n; the rpow is undone by `← rpow_natCast, ← rpow_mul, mul_div_cancel₀, rpow_natCast`. Apply it to x = u/a, y = v/b, multiply by a^(n-m) b^m and integrate with intervalIntegral.integral_mono_on; the right side integrates to ≤ 1. To avoid a separate case for ∫u^n = 0, use a = (A+ε)^(1/n) (Real.rpow_inv_natCast_pow) and finish with le_of_forall_pos_le_add.