OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingEnergyDischarge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The whole-plane main result with its localized energy input discharged. Only the published scalar existence input remains explicit.

  1. theorem OAI.ForcedComputation.ExpandingDetector.whole_plane_velocity_detection_energy_discharged line 14