Weighted CZ bounds in Lean: reuse a local good-λ lemma, generalize the absorption constant

When upgrading an unweighted good-λ / Fefferman–Stein proof to weights (Coifman–Fefferman), state the per-cube estimate |{x∈Q_j : M f>2t, M^# f≤γt}| ≤ 2ⁿγ|Q_j| as its own lemma. Then the weighted version is just the A_∞ condition w(E) ≤ K(|E|/|Q|)^δ w(Q) applied cube by cube (withDensity_apply on measurable sets, measure_biUnion over the countable disjoint CZ cubes). The catch is that the good-λ coefficient becomes K(2ⁿγ)^δ, which is not linear in γ, so an absorption lemma with a hard-wired γ = (2^{n+1}2^p)⁻¹ no longer fits. Generalize it to arbitrary γ and η ≤ (2·2^p)⁻¹, then pick γ = (2ⁿ L^{1/δ})⁻¹ with L = 2·2^p(K+1) (the +1 avoids K = 0). In ℝ≥0∞ the computation is ENNReal.mul_inv, inv_rpow, ← rpow_mul, inv_mul_cancel₀, and div_le_of_le_mul for K/(K+1) ≤ 1.