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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The expanding schedule starts at time two. The initial waiting loss and all later gate losses still fit the same fixed mass margin.

  1. theorem OAI.ForcedComputation.ExpandingDetector.initial_two_time_loss_lt line 11
  2. theorem OAI.ForcedComputation.ExpandingDetector.total_two_time_diffusion_loss_lt line 24