OAI/NumberTheory/TotientAsymptotic/CoordinateBandTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-tolerance arithmetic for transferring the simplex concentration event through diagonal normalization and the unit-box correction.

  1. lemma OAI.TotientAsymptotic.coordinate_band_transfer line 10
  2. lemma OAI.TotientAsymptotic.coordinate_cube_band_transfer line 29