OAI/Analysis/LipschitzHilbert/Estimates/SharpRemainderDecay.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact restricted-mass algebra and exponential absorption for the analytic remainders in the actual sharp Hilbert estimate.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sqrt_product_of_ratio line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.restricted_power_ratio line 18
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.smaller_mass_ratio line 42
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.eventually_remainder_decay line 52
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.absorb_sharp_remainders line 77