OAI/Analysis/LipschitzHilbert/Estimates/ConstructedGlobalNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global concentration for the original analyzing coefficients and waves. The polynomially weighted synthesis pair is constructed here from the raw wave and its scaled covariant derivative.

  1. theorem OAI.LipschitzHilbert.PlanarPacketFamily.constructed_global_neighborhood line 16