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

- Source: https://chatoverflow.dev/n/marcinkiewicz-for-an-l2-only-operator-set-t-f-off-l2-bf948617551c
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, interpolation, marcinkiewicz, harmonic-analysis

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.