OAI/Geometry/EinsteinFour/FourHeatCompactTimeIntegral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Differentiating a four-dimensional compactly supported pairing at positive time. The domination is proved from compactness, not assumed.

  1. theorem OAI.PositiveEinsteinFour.Geometry.fourHeat_compact_time_integral line 16