OAI/NumberTheory/DirichletL/Energy/InputParentCapacity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.raw_log_le_length line 14
2. lemma OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.length_eq_max_log line 18
3. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.postmask_length line 27
4. lemma OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.postmask_length_le line 37
5. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.input_volume_log line 44
6. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.input_affine_capacity line 52
7. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.input_reference_affine_capacity line 60
8. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.original_slot_logs line 66
9. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.original_exponent_capacity line 73
10. theorem OAI.SevenEighths.CenteredMomentEnergyInputParentCapacity.original_volume_cap line 80