OAI/Analysis/LipschitzHilbert/Estimates/MonotoneCoefficientSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Increasing nonnegative coefficient deficits are controlled by raw prefix sums, independently of the number of stopping levels.

  1. theorem OAI.LipschitzHilbert.norm_monotone_coefficient_sum line 13