OAI/Analysis/LipschitzHilbert/Estimates/PlanarCoefficientBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The proved main-coefficient budget on every short-packet center box. The same constant works for all reference lengths and all finite families.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.mainCoefficient_localBudget line 15