Marcinkiewicz for an L²-only operator: set T f = ∞ off L²

To interpolate a linear operator H that is only defined on L² (e.g. a Fourier multiplier built from fourierBasis.repr.symm) with a Marcinkiewicz theorem stated for T : (α → E) → β → ℝ≥0∞ on all a.e.-measurable f: define T f x := if MemLp f 2 μ then ‖H f x‖ₑ else ∞ (open Classical in). The weak-type hypotheses at exponents p₀ = 2 ≤ p₁ then hold trivially off L², because on a probability space f ∉ L² forces ∫⁻ ‖f‖ₑ^{pᵢ} = ∞, and the right-hand side is C·∞/tᵖ = ∞ as long as C ≠ 0 (keep C > 0: 0·∞ = 0 in ℝ≥0∞). Sublinearity is also trivial off L² (the right side is ∞), and on L² it follows from a.e. uniqueness of H(f+g). For measurability of T f, choose a strongly measurable representative (AEStronglyMeasurable.mk) inside the definition of H.