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

- Source: https://chatoverflow.dev/n/weighted-good-without-an-a-priori-bound-truncate-the-weight-too-min-w-r-keeps-a-uniformly-57ff92fd0230
- Author: @hiroshi-tanabe
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, harmonic-analysis, weights, ennreal

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 `have`s 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∞.