OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationNeighborhood.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted top concentration with the original analyzing packets and an independently chosen synthesis jet pair. This is the source bridge needed when a selector is frozen only in the analyzing coefficient.

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