OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarHeatEvolution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Differentiation in time of the actual heat average. The compact forcing allows a fixed compact dominating set on every positive time neighborhood.

  1. theorem OAI.ContinuumCoulomb.planarHeatAverage_flip line 13
  2. theorem OAI.ContinuumCoulomb.planarHeatKernel_joint_continuousAt line 19
  3. theorem OAI.ContinuumCoulomb.planarHeatTimeDerivative_joint_continuousAt line 26
  4. theorem OAI.ContinuumCoulomb.planarHeatTimeDerivative_forcing_continuous line 36
  5. theorem OAI.ContinuumCoulomb.planarHeatTimeDerivative_forcing_joint_continuousAt line 43
  6. theorem OAI.ContinuumCoulomb.planarHeatTimeDerivative_local_bound line 58
  7. theorem OAI.ContinuumCoulomb.planarHeatAverage_hasDerivAt line 82