OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/CrossTransitionEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryTwoScaleCofactor.crossTransitionEnergy line 22
2. lemma OAI.OrdinaryTwoScaleCofactor.cross_transition_amplification line 27
3. lemma OAI.OrdinaryTwoScaleCofactor.cross_transition_bound line 55
4. lemma OAI.OrdinaryTwoScaleCofactor.dyadic_inverse_mass line 71
5. lemma OAI.OrdinaryTwoScaleCofactor.dyadic_inverse_squared_mass line 87
6. lemma OAI.OrdinaryTwoScaleCofactor.dyadic_mixed_energy line 102
7. theorem OAI.OrdinaryTwoScaleCofactor.dyadic_cross_transition line 118