OAI/Analysis/LipschitzHilbert/Trees/SlopePartitionGrid.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact finite smooth partition uses the same arithmetic labels as the packet model; their local multiplicity is uniform in the truncation.

  1. theorem OAI.LipschitzHilbert.SourceSlopeLabels.injective_integer_multiplicity line 12
  2. def OAI.LipschitzHilbert.PacketRepresentation.finiteSlopeLabels line 27
  3. def OAI.LipschitzHilbert.PacketRepresentation.finiteSlopeCenter line 28
  4. def OAI.LipschitzHilbert.PacketRepresentation.scaledSlopePartition line 30
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.scaledSlopePartition_apply line 33
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.scaledSlopePartition_support line 39
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteSlopePartition_sum line 46
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_finiteSlopeCenter_multiplicity line 60