AnalyzedNeighborhood.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Neighborhood concentration for actual normalized analyzing coefficients. Both local coefficient budgets follow from scalar Lépingle variation, including after replacement of the synthesis waves.

theorem OAI.LipschitzHilbert.PlanarPacketFamily.analyzed_interval_neighborhood line 16