OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarProcessorUnconditional.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete planar processor theorem with the smooth-dependence input discharged for the actual compiled finite Hamiltonian.

  1. theorem OAI.ForcedComputation.Recorder.Planar.smooth_planar_processor_unconditional line 13
  2. theorem OAI.ForcedComputation.Recorder.Planar.exists_smooth_planar_processor line 21