OAI/Analysis/LipschitzHilbert/Trees/BoundaryErrorFubini.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the nonnegative boundary error over physical space and one finite translation interval. Integrability follows from the proved pointwise average bound, rather than being assumed on the product.

  1. theorem OAI.LipschitzHilbert.nonnegative_translation_average_integral_le line 15