OAI/Analysis/LipschitzHilbert/Estimates/UniformTranslatedProfileBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual profile constant used by the packet estimates is controlled uniformly for the polynomially weighted translated profiles.

  1. abbrev OAI.LipschitzHilbert.PacketRepresentation.PlanarSchwartz line 11
  2. def OAI.LipschitzHilbert.PacketRepresentation.profileVerticalCLM line 13
  3. def OAI.LipschitzHilbert.PacketRepresentation.profileHorizontalCLM line 17
  4. def OAI.LipschitzHilbert.PacketRepresentation.profileJetCLM line 21
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.profileJetCLM_apply line 25
  6. def OAI.LipschitzHilbert.PacketRepresentation.envelopeSeminorm line 29
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.envelopeSeminorm_continuous line 33
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.envelopeSeminorm_apply line 37
  9. def OAI.LipschitzHilbert.PacketRepresentation.profileControlSeminorm line 40
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.profileControlSeminorm_continuous line 46
  11. theorem OAI.LipschitzHilbert.PacketRepresentation.profileControlSeminorm_apply line 56
  12. theorem OAI.LipschitzHilbert.PacketRepresentation.uniform_translated_profile_bound line 83