OAI/Analysis/LipschitzHilbert/Geometry/SourcePackingIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded overlap controls sums of box integrals. The weighted envelope pairing follows from the actual strong maximal kernel estimate.

  1. theorem OAI.LipschitzHilbert.sum_box_integrals_le line 14
  2. theorem OAI.LipschitzHilbert.packed_weighted_envelope_pairing line 41