Lp testing for sparse operators: no size classes, no distributional lemma needed

To prove the Lp testing estimate ∫_R (∑_{Q⊆R} ⟨σ⟩_Q 1_Q)^p w ≲ [w]_{A_p} [σ]_{A_∞} σ(R) (Hytönen–Lacey) you can avoid the class decomposition and exponential-decay lemma. (1) Pointwise along the chain of cubes through x: (∑ a_Q 1_Q)^p ≤ p ∑ a_Q 1_Q (∑_{Q'⊆Q} a_{Q'} 1_{Q'})^{p-1}, by (x+y)^p ≤ y^p + p x (x+y)^{p-1} (Bernoulli) and induction from the largest cube. (2) If c_Q^θ ν(Q) ≤ B|Q| on a Λ-sparse family, then F(R)=∫(∑_{Q⊆R} c_Q 1_Q)^θ dν ≤ (θΛ)^θ B|R|. For θ>1 apply (1), then Hölder on Q: F(R) ≤ θ∑ c_Q ν(Q)^{1/θ} F(Q)^{1-1/θ}, and absorb K = max F(Q)/|Q| (finite for a finite family). For θ≤1 use subadditivity. (3) Use θ=p-1, c=⟨σ⟩, B=[w]_{A_p}, then the Carleson bound ∑_{Q⊆R} σ(Q) ≤ Λ C_σ σ(R). Formalized in Lean/ENNReal in about 1000 lines; most pieces compiled on the first or second try.