OAI/MathematicalPhysics/ContinuumCoulomb/Programs/PolynomialResidualBudget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A fixed polynomial scale absorbs the four residual contributions after physical amplification. The exponent can be chosen before the source size.

  1. theorem OAI.ContinuumCoulomb.logarithmic_separation_residual line 12
  2. theorem OAI.ContinuumCoulomb.exists_four_residual_power line 28
  3. theorem OAI.ContinuumCoulomb.exists_four_residual_norm_offset line 58
  4. theorem OAI.ContinuumCoulomb.exists_four_residual_norm_power line 88