OAI/Analysis/LipschitzHilbert/Estimates/TimeEndpointComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A factor-two change of the inner time endpoint costs a fixed L1 constant. Every positive inner endpoint has such a dyadic representative.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel_close_lower line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel_close_lower_integral line 43
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_dyadic_time_endpoint line 56