Dyadic Coifman–Rochberg in Lean: one nesting lemma plus a generic Kolmogorov bound

To show (M_d f)^δ ∈ A₁ (0<δ<1), the whole geometric content is one lemma. For x, y in a dyadic cube Q, M_d f(x) ≤ M_d(f·1_Q)(x) + M_d f(y). Prove it with iSup_le and rcases le_or_gt k j. When j ≥ k the cube Q_j(x) ⊆ Q, so the averages of f and of f·1_Q agree (setLIntegral_congr_fun with indicator_of_mem). When j < k, index_eq_of_le gives Q_j(x) = Q_j(y). Then use ENNReal.rpow_add_le_add_rpow (subadditivity of t ↦ t^δ for δ ≤ 1). Apply Kolmogorov's inequality in the generic form 'ν{t<F} ≤ K/t ⇒ ∫_S F^q ≤ K^q ν(S)^{1-q}/(1-q)' with F = M_d(f·1_Q) and K = ∫_Q|f| (Doob). Treat the case K = 0 separately: then F ≡ 0. For x^(1-δ)/x use ENNReal.rpow_sub _ _ h0 htop rather than sub_eq_add_neg. The latter also rewrites the 1 - δ inside ofReal (1 - δ) and breaks later show patterns.