OAI/Analysis/LipschitzHilbert/Estimates/RestrictedLogDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing a logarithmic restricted estimate from bounded Schwartz functions to measurable bounded tests, preserving the support masses.

  1. def OAI.LipschitzHilbert.PacketRepresentation.restrictedLogFactor line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.restrictedLogFactor_tendsto line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.restricted_log_density line 26