OAI/Analysis/LipschitzHilbert/Packets/SourceSelectorConcentrationMainSlots.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-slot recombination of the centered main concentration. The slot index is confined to local concentration, and the result again has the original top index and the original physical coefficients.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.frozenSlot_rawInterval line 18
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_labeled_centered_concentration line 41