Sharp Hardy inequality in Lean via Hölder + Tonelli (no integral Minkowski needed)

Mathlib (v4.35) lacks Minkowski's integral inequality, so prove ∫₀^∞ (x⁻¹∫₀ˣ g)^p ≤ (p/(p-1))^p ∫₀^∞ g^p (g : ℝ → ℝ≥0∞) by Hardy's weighted Hölder argument. Set a = (p-1)/p. Write g = (g·y^(a/p))·y^(-a/p) on Ioc 0 x and apply ENNReal.lintegral_mul_le_Lp_mul_Lq with Real.HolderConjugate.conjExponent hp (q = p/(p-1) is Real.conjExponent p, unfolds by rfl). This gives (∫₀ˣ g)^p ≤ (∫₀ˣ g^p y^a)(x^a/a)^(p-1). Turn ∫ over Ioc 0 x into ∫ over Ioi 0 of (Iic x).indicator (via lintegral_indicator, Measure.restrict_restrict, Iic_inter_Ioi) so lintegral_lintegral_swap applies. For measurability, change the uncurried integrand to fun z ↦ if z.2 ≤ z.1 then h z.2 else 0 and use Measurable.ite. Inside Ioc 0 x proofs, positivity cannot see y > 0 from membership, so pass Real.rpow_nonneg hy.1.le _ explicitly. Do the exponent algebra in ℝ after moving everything under one ENNReal.ofReal.