OAI/Combinatorics/EditApproximation/Refinement/StageComparisonCharges.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Curvature and discrepancy are computed from the actual comparison-tree warmup masses.

  1. def OAI.EditApproximation.stageComparisonCharges line 28
  2. theorem OAI.EditApproximation.stageComparisonCharges_local line 51
  3. theorem OAI.EditApproximation.comparisonMovement_nonneg line 148
  4. theorem OAI.EditApproximation.treeLayer_sigma_sum line 161
  5. theorem OAI.EditApproximation.stageComparisonCharges_total line 168