OAI/Analysis/LipschitzHilbert/Estimates/FiniteRemovalIteration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite iteration of proved removal steps, with exact telescoping packet sums. The step is supplied by the density and size selections.

  1. def OAI.LipschitzHilbert.finitePacketSum line 12
  2. theorem OAI.LipschitzHilbert.iterate_finite_removal line 15
  3. theorem OAI.LipschitzHilbert.finite_removal_zero_remainder line 63