OAI/MeasureTheory/Falconer/Shells/ScalarShellError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing a bounded stationary error through a finite scalar shell

The comparison uses the original scalar functions and a pointwise remainder bound. Square integrability of the approximating function supplies all the integrability needed for the final error estimate.

  1. theorem OAI.Falconer.norm_sq_le_of_norm_sub_le line 18
  2. theorem OAI.Falconer.scalar_shell_error_transfer line 28