OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/HeatSampleError.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identification and uniform error of the literal rational samples used in the box quadrature. The required Taylor magnitude follows from the input radius and the positive time cutoff.

  1. theorem OAI.ContinuumCoulomb.rationalPosition_eq_pair line 12
  2. theorem OAI.ContinuumCoulomb.RationalHeatSample.error_density line 19
  3. theorem OAI.ContinuumCoulomb.RationalHeatSample.error_density_uniform line 28
  4. theorem OAI.ContinuumCoulomb.RationalHeatSample.exponent_abs_le line 37