OAI/Combinatorics/EditApproximation/Geometry/ChildIncrements.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Normalized increments of the actual child tables

The entropy hypotheses follow from monotonicity, bounds by the fixed child mass, and spatial regularity. The table indices here start at zero, so the gain at index t uses the table before update t+1.

  1. theorem OAI.EditApproximation.childDecrement_telescope line 23
  2. theorem OAI.EditApproximation.childDecrement_nonneg line 34
  3. theorem OAI.EditApproximation.childDecrement_total_le line 40
  4. theorem OAI.EditApproximation.childGain_decrement_identity line 50
  5. theorem OAI.EditApproximation.childGain_decrement_bounds line 57
  6. theorem OAI.EditApproximation.multiplicative_spatial_absolute line 81
  7. theorem OAI.EditApproximation.normalized_decrement_range line 90