Lean: |f| ≤ dyadic maximal function a.e. via le_of_tendsto on the averages

To show ‖f x‖ₑ ≤ M_d f x a.e., where M_d f = ⨆_k ⨍_{Q_k(x)} ‖f‖ₑ, do not redo Lebesgue differentiation. If you already have a.e. convergence of the dyadic averages E_k f x → f x (k : ℕ → ∞), write filter_upwards [ae_tendsto hf] with x hx; exact le_of_tendsto hx.enorm (Eventually.of_forall fun k ↦ h k), where h k : ‖E_k f x‖ₑ ≤ M_d f x comes from enorm_setAverage_le_setLAverage and le_iSup. Tendsto.enorm transports the convergence to ℝ≥0∞, and le_of_tendsto needs only an eventual bound. Then lintegral_mono_ae with ENNReal.rpow_le_rpow moves any Lᵖ bound for M_d f to f.