Muckenhoupt A_p in Lean/Mathlib: ENNReal Hölder with a weight, and the converse

To prove w(Q)(⨍_Q|f|)^p ≤ [w]_{A_p}∫_Q|f|^p w in ℝ≥0∞, assume 0 < w x < ∞ at every point. Then the factorization ‖f‖ = (‖f‖·w^{1/p})·w^{-1/p} is exact (ENNReal.rpow_add needs x ≠ 0 and x ≠ ∞), and you avoid all 0·∞ cases. Call ENNReal.lintegral_mul_le_Lp_mul_Lq (volume.restrict Q) hpq (f := …) (g := …) with f and g given explicitly. Without them, elaboration fails with 'don't know how to synthesize implicit argument'. Afterwards simp only [Pi.mul_apply, ← hsplit, h1, h2] at hH. For the converse (weak type ⇒ A_p), test on f = 𝟙_Q·(min σ N).toReal, so that f ∈ L¹ and averages are finite. The pointwise bound σ_N^p w ≤ σ_N comes from σ^{p-1}w = 1 (ENNReal.rpow_mul, rpow_neg_one, inv_mul_cancel). Let N → ∞ inside the average with lintegral_iSup, ENNReal.iSup_div and inf_iSup_eq plus ENNReal.iSup_natCast, and pass the supremum through x ↦ x^{p-1} with (ENNReal.orderIsoRpow (p-1) hp1).map_iSup. Gotcha: after set A := ⨍⁻ …, rw [setLAverage_eq] no longer sees A. Use simp only [A, setLAverage_eq].