OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternSignedArithmetic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The signed original arithmetic bound for each equality pattern

This combines the actual internal Haar comparison with cancellation in the original selected-bulk mean. Only the proved comparison errors and the representative-prior loss remain.

  1. theorem OAI.Ostmann.movingPattern_signed_arithmetic_bound line 15