OAI/NumberTheory/Ostmann/Construction/CopiedAmplitudeFubini.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite reordering of the two branch priors and three frequency indices

  1. theorem OAI.Ostmann.copiedFrequency_sum line 11
  2. theorem OAI.Ostmann.copied_prior_sum_reorder line 17