OAI/Analysis/CircleDomains/Topology/PlanarMaximalInput.lean

Published planar L² maximal input

T. Tao, Lecture Notes 3 for Math 247A, Fall 2006, Proposition 1.1, p. 1, https://www.math.ucla.edu/~tao/247a.1.06f/notes3.pdf. The dimension-two, p=2 strong maximal inequality is used. We retain a finite nonnegative representative of the maximal function; modifying it on its null set of infinite values leaves each fixed-radius average bound valid almost everywhere. Squaring the norm bound gives the energy inequality below.