OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/ActualResidualParameters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The counterterm size in the residual theorem is computed from the actual orbital Coulomb sums; no independent coefficient bound is assumed.

  1. theorem OAI.ContinuumCoulomb.actual_counterterm_scale_bound line 13
  2. theorem OAI.ContinuumCoulomb.exists_actual_manufactured_residual_parameters line 24