OAI/Analysis/LipschitzHilbert/Trees/SourceLatticeRawData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Construct the top concentration data from actual source packets. The premises describe physical spectrum, actual centers and fixed-order profile bounds; neither concentration nor a coefficient budget is assumed.

  1. structure OAI.LipschitzHilbert.SourceLatticeSpectralData line 17
  2. def OAI.LipschitzHilbert.SourceLatticeSpectralData.lo line 39
  3. def OAI.LipschitzHilbert.SourceLatticeSpectralData.hi line 40
  4. theorem OAI.LipschitzHilbert.SourceLatticeSpectralData.raw_cutoffs line 42
  5. structure OAI.LipschitzHilbert.SourceLatticeTopGeometry line 51
  6. theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_top_bound line 63
  7. theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_top_derivative_bound line 75
  8. def OAI.LipschitzHilbert.SourceLatticePacket.topRawData line 87
  9. def OAI.LipschitzHilbert.SourceLatticePacket.topCovariantData line 119