OAI/Analysis/LipschitzHilbert/Packets/AnalyzedLineMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reference-line moments for the actual analyzing coefficients, using their norm bound and local Carleson budget.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.analyzedLine_moment line 18