OAI/Analysis/LipschitzHilbert/Estimates/LongDyadicSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial oscillation after summing the actual dyadic long scales.

  1. theorem OAI.LipschitzHilbert.long_dyadic_sum_oscillation line 14