OAI/Geometry/RCD/Harmonic/ResidualSamplingError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Choosing the finite sampling accuracy

The number of samples is fixed first. Only then is the product approximation error chosen. The needed error has a square-root rate.

  1. def OAI.RegularPointCoordinates.residualSamplingError line 15
  2. theorem OAI.RegularPointCoordinates.residualSamplingError_tendsto line 18
  3. theorem OAI.RegularPointCoordinates.exists_residual_sampling_accuracy line 23
  4. theorem OAI.RegularPointCoordinates.residualSamplingError_bounds line 39