OAI/Analysis/LipschitzHilbert/Trees/SourceSnapshotPolynomial.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual source snapshot envelope is a fixed polynomial in L. This supplies the unnormalized size input for the normalized-motion theorem.

  1. theorem OAI.LipschitzHilbert.source_snapshot_envelope_polynomial line 14
  2. theorem OAI.LipschitzHilbert.eventually_source_snapshot_envelope line 44