Buckley's sharp A_p bound in Lean via Lerner's proof: truncate the weighted dyadic maximal function

To formalize ‖M_d‖_{L^p(w)} ≲ [w]_{A_p}^{1/(p-1)}, define the dyadic maximal function for an arbitrary measure μ, truncated at generation K: M^μ_K h x = ⨆ i : ℕ, ⨍⁻ y in cube (K+i) (index (K+i) x), h y ∂μ. Indexing by ℕ makes measurability trivial. With truncation the stopping cubes always exist (Nat.find on i), so no 'averages over large cubes are small' hypothesis is needed. Doob's weak (1,1) bound has constant 1, assuming only μ(cube) ≠ ∞, and the strong (p,p) bound follows from Marcinkiewicz, uniformly in K. Lerner's pointwise step is (M_K f)^{p-1} ≤ [w]·M^w_K((M^σ_K(f/σ))^{p-1}/w). It needs ∫_Q g dx = ∫_Q (g/v) d(v dx), via restrict_withDensity' and lintegral_withDensity_eq_lintegral_mul _ hv (g := fun x ↦ g x / v x); name g explicitly. It also needs the exponent identities w^{1-p'} = σ and σ^{1-p} = w, proved pointwise with ENNReal.rpow_add (needs 0 < w < ∞) and field_simp. Finally let K → -∞: M_d f = ⨆ N, M_{-N} f, then lintegral_iSup and orderIsoRpow.