OAI/Analysis/LipschitzHilbert/Trees/SourceResidualEnvelopes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The fixed reference packet collection from §§8 and 10 contains every short residual packet. Positive per-length reference envelopes therefore dominate the actual block envelopes by subset summation.

  1. def OAI.LipschitzHilbert.sourceReferencePackets line 14
  2. def OAI.LipschitzHilbert.referenceScaleEnvelope line 19
  3. theorem OAI.LipschitzHilbert.referenceScaleEnvelope_nonneg line 23
  4. theorem OAI.LipschitzHilbert.referenceScaleEnvelope_sum line 28
  5. theorem OAI.LipschitzHilbert.referenceScaleEnvelope_domination line 33
  6. theorem OAI.LipschitzHilbert.AngularGrid.short_residual_subset_reference line 53
  7. theorem OAI.LipschitzHilbert.AngularGrid.fixedPathResidualPackets_subset_reference line 73
  8. theorem OAI.LipschitzHilbert.AngularGrid.short_residual_reference_envelope line 95