OAI/Combinatorics/EditApproximation/Refinement/PhysicalBinaryMass.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The child mass is built from the actual gathered warmup words. The mean and construction of its finite input list both contribute to work.

  1. def OAI.EditApproximation.physicalWarmupMassWithWork line 11
  2. theorem OAI.EditApproximation.physicalWarmupMassWithWork_value line 17
  3. theorem OAI.EditApproximation.physicalWarmupMassWithWork_bounds line 34
  4. theorem OAI.EditApproximation.warmupAverageWordBudget_le_power line 47