OAI/NumberTheory/DirichletL/Energy/ChildState.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyChildState.ball_support line 20
2. lemma OAI.SevenEighths.CenteredMomentEnergyChildState.canonical_mask_nonexceptional line 26
3. def OAI.SevenEighths.CenteredMomentEnergyChildState.canonicalState line 36
4. lemma OAI.SevenEighths.CenteredMomentEnergyChildState.canonicalState_width line 59
5. lemma OAI.SevenEighths.CenteredMomentEnergyChildState.canonicalState_power line 64
6. lemma OAI.SevenEighths.CenteredMomentEnergyChildState.common_puncture_bound line 74
7. lemma OAI.SevenEighths.CenteredMomentEnergyChildState.actual_dyad_ge_one line 90
8. def OAI.SevenEighths.CenteredMomentEnergyChildState.actualState line 95
9. theorem OAI.SevenEighths.CenteredMomentEnergyChildState.actualState_width line 102