OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarHeatBoxBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Explicit coordinate bounds on the fixed forcing square. They turn the kernel estimates into concrete quadrature constants for every input point, with polynomial dependence on its magnitude.

  1. theorem OAI.ContinuumCoulomb.planarPair_norm_sq line 13
  2. theorem OAI.ContinuumCoulomb.planarPair_norm_le_two line 19
  3. theorem OAI.ContinuumCoulomb.planarPair_distance_first line 31
  4. theorem OAI.ContinuumCoulomb.planarPair_distance_second line 42
  5. theorem OAI.ContinuumCoulomb.planarPair_distance_bound line 53
  6. def OAI.ContinuumCoulomb.planarBoxSpatialConstant line 58
  7. def OAI.ContinuumCoulomb.planarBoxTimeConstant line 61
  8. theorem OAI.ContinuumCoulomb.planarBox_spatial_first line 64
  9. theorem OAI.ContinuumCoulomb.planarBox_spatial_second line 76
  10. theorem OAI.ContinuumCoulomb.planarBox_time line 88