OAI/NumberTheory/TotientAsymptotic/PhaseBandTransfer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform phase-band comparison and the actual coordinate scaling bounds.

  1. lemma OAI.TotientAsymptotic.fullSimplexCenter_eq_fordBandScale line 15
  2. lemma OAI.TotientAsymptotic.phase_band_center_close line 22
  3. def OAI.TotientAsymptotic.fullBoxScale line 35
  4. lemma OAI.TotientAsymptotic.fullBoxScale_one_le line 38
  5. lemma OAI.TotientAsymptotic.fullBoxScale_prefix_close line 45
  6. lemma OAI.TotientAsymptotic.fullBoxScale_jacobian line 56