OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationSpectral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted jet neighborhood is instantiated from the original physical spectral wedge and the source top geometry. No concentration, coefficient budget or replacement-wave support is assumed separately.

  1. theorem OAI.LipschitzHilbert.SourceLatticePacket.source_frozen_spectral_jet_neighborhood line 14