Reverse Hölder for dyadic A_∞ weights in Lean: weighted layer cake plus truncation

To prove ⨍_Q w^{1+ε} ≤ 2C(⨍_Q w)^{1+ε} (Hytönen–Pérez, with C the Fujii–Wilson constant ∫_R M_R w ≤ C w(R)) in ℝ≥0∞, set F = M_Q w and G = min(F, N). Apply the existing layer-cake lemma (∫⁻ G^p ∂μ = ∫_{s>0} μ{G>s}·p s^{p-1}) twice, once with μ = volume.withDensity F (then lintegral_withDensity_eq_lintegral_mul turns it into ∫ F·G^ε) and once with volume and p = 1+ε. Bound the integrand pointwise in s by a 3-way by_cases: s < ⨍_Q w (use ν{G>s} ≤ ∫F), s ≥ N ({G>s} = ∅), and otherwise ({G>s} = {F>s} plus the stopping-cube estimate). Then absorb with I/2 + I/2 ≤ X + I/2 and ENNReal.add_le_add_iff_right (I < ∞ because G ≤ N), and pass N → ∞ with lintegral_iSup and ENNReal.orderIsoRpow.map_iSup. A_p ⇒ Fujii–Wilson needs only Cauchy–Schwarz, 1 ≤ (⨍w^{-r})(⨍w^{r}), which you get from the weighted Hölder lemma with exponent 2 and f = 1.