OAI/Analysis/LipschitzHilbert/Geometry/LaceyLiProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-family weak-(2,2) Lipschitz Kakeya estimate of Lacey--Li, Memoirs AMS 205 (2010), no.965, result 1.10 / equation (1.11). The proof uses the actual maximal-removal selection, the near/far overlap bounds, and the proved weak-L1 auxiliary operators.

  1. theorem OAI.LipschitzHilbert.laceyLiInput_proved line 15