OAI/Analysis/LipschitzHilbert/Packets/UniformAnalyzedLine.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform local budgets for the actual analyzing coefficients. The constant is fixed before the finite Hilbert and scale index types.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.uniform_analyzedLine_localBudget line 15
  2. theorem OAI.LipschitzHilbert.PlanarPacketFamily.uniform_analyzed_top_moment line 51