OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarHeatBoxCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact two-coordinate box formula for the actual heat average. The forcing vanishes outside this fixed square, so spatial truncation introduces no error.

  1. def OAI.ContinuumCoulomb.planarPairEquiv line 15
  2. theorem OAI.ContinuumCoulomb.planarPairEquiv_apply line 19
  3. theorem OAI.ContinuumCoulomb.planarPairEquiv_symm_apply line 21
  4. theorem OAI.ContinuumCoulomb.planarPairEquiv_measurePreserving line 26
  5. theorem OAI.ContinuumCoulomb.planarPairEquiv_symm_continuous line 30
  6. theorem OAI.ContinuumCoulomb.planarPair_integral line 35
  7. theorem OAI.ContinuumCoulomb.planarForcing_pair_zero line 40
  8. theorem OAI.ContinuumCoulomb.planarHeatAverage_box line 56
  9. theorem OAI.ContinuumCoulomb.planarHeatResolvent_box line 81