OAI/Analysis/LipschitzHilbert/Estimates/TailLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strict tail bounds pass to almost-everywhere limits.

  1. theorem OAI.LipschitzHilbert.strict_tail_bound_of_ae_tendsto line 16