OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/HoppingBox.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual contact numerator is an integral over the fixed forcing square. Its translated sample point is represented exactly by rational subtraction, so the concrete resolvent evaluator applies directly.

  1. def OAI.ContinuumCoulomb.planarHoppingNumerator line 15
  2. theorem OAI.ContinuumCoulomb.planarHopping_eq_numerator line 17
  3. theorem OAI.ContinuumCoulomb.planarHoppingNumerator_box line 20
  4. theorem OAI.ContinuumCoulomb.rationalPosition_shift_first line 41
  5. theorem OAI.ContinuumCoulomb.rationalShift_norm_bound line 47