OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationWeighted.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Scale-independent weighted concentration for the two synthesis jet pairs, with the original frozen analyzing coefficients. Raw geometry, regularity and spectra are supplied by the actual source packet data.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.frozen_jet_top_neighborhood line 18