OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalWarmup.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The literal warmup can be calculated by direct bounded endpoint loops. Equality with the complete tables is only asserted on good seeds; the local rules themselves remain finite and bounded on every seed.

  1. def OAI.EditApproximation.physicalLocalWarmup line 13
  2. theorem OAI.EditApproximation.physicalLocalWarmup_bounds line 31
  3. theorem OAI.EditApproximation.physicalLocalWarmup_eq line 54
  4. def OAI.EditApproximation.physicalLocalWarmupMass line 79
  5. theorem OAI.EditApproximation.physicalLocalWarmupMass_eq line 84