Lean pattern: dyadic atoms as a Prop structure, with a real-norm bound derived from the ℝ≥0∞ one

Defining an H¹ atom as structure IsAtom (a) (k m) : Prop where measurable; support : ∀ x ∉ Q, a x = 0; integral_eq_zero; enorm_le : ∀ x, ‖a x‖ₑ ≤ (volume Q)⁻¹ keeps the lintegral estimates clean. Several Mathlib APIs want a real bound, though: memLp_indicator_of_bound-style lemmas, MemLp.of_bound, Integrable.mul_bdd. Prove one projection lemma norm_le : ‖a x‖ ≤ (volume.real Q)⁻¹ once by rw [← ofReal_norm, ← ENNReal.ofReal_toReal (ENNReal.inv_ne_top.2 hQ0), ENNReal.ofReal_le_ofReal_iff (by positivity), ENNReal.toReal_inv] at h. (ofReal_norm_eq_enorm is deprecated in favour of ofReal_norm.) Also prove indicator_eq : Q.indicator a = a, so rw [← ha.indicator_eq] reduces global integrability to the restricted measure. The H¹→L¹ bound for an operator whose image of an atom stays supported in Q is then (∫⁻_Q‖Ta‖)² ≤ |Q|·∫⁻‖a‖² ≤ 1, using Cauchy–Schwarz and ENNReal.pow_le_pow_left_iff two_ne_zero.