Weighted good-λ without an a priori bound: truncate the weight too, min(w,R) keeps A_∞ uniformly

Problem: the absorption step in Coifman–Fefferman, ∫(M_d f)^p w ≤ C∫(M^# f)^p w, needs ∫(M_d f)^p w < ∞ beforehand. Truncating only the function, min(M_d f, N), does not help, because w{M_d f > s} may be infinite.

Fix: also truncate the weight, u = min(w,R). Lemma (paper and Lean): if w(E) ≤ K(|E|/|Q|)^δ w(Q) for E ⊆ Q, with 0 < δ ≤ 1 and w(Q) < ∞, then u satisfies the same inequality with K' = 2K + η⁻¹, where Kη^δ ≤ 1/2. K' does not depend on R. Let F = {w > R} ∩ Q. Always u(E) ≤ R|E|. If |F| ≥ η|Q|, then u(Q) ≥ Rη|Q|. Otherwise w(F) ≤ w(Q)/2, so w(Q) ≤ 2u(Q). Reduce first to δ ≤ 1 via r^δ ≤ r^{min δ 1} for r ≤ 1 (ENNReal.rpow_le_rpow_of_exponent_ge).

Then ∫ min(M_d f,N)^p u ≤ R∫ min(M_d f,N)^p < ∞ as soon as M_d f has weak type p₀ < p, e.g. weak (1,1) for f ∈ L¹, p > 1. Absorb, then use monotone convergence in R (ENNReal.mul_iSup) and then in N ((ENNReal.orderIsoRpow p hp).map_iSup). ⨆ n, min b n = b is (inf_iSup_eq b _).symm.trans (by rw [ENNReal.iSup_natCast]; exact inf_top_eq b).

Lean gotchas: (1) in lintegral_iSup, pass the measurability and monotonicity as haves typed with the lambda form fun R x ↦ .... Inline .mul yields a Pi-product (f * g) a that rw [← lintegral_iSup ...] then cannot find. (2) gcongr on ν {x | a < F x} ≤ ν {x | a < min (F x) N} descends into the set-builder and asks for F x ≤ min (F x) N. Use measure_mono fun x (hx : a < F x) ↦ show a < min (F x) N from lt_min hx h instead. (3) mul_le_mul_left' no longer exists in current Mathlib. mul_le_mul' le_rfl h works in ℝ≥0∞.