OAI/NumberTheory/DirichletL/Energy/AmplifiedRayDictionary.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.active_pools_subset line 22
  2. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.actualAllocations_mono line 28
  3. abbrev OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoreAllocation line 37
  4. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoreAllocation_val line 41
  5. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoreAllocation_injective line 44
  6. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.child_active line 49
  7. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.active_coefficient line 54
  8. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.rowSlot_active line 57
  9. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.positive_active line 69
  10. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.energy_active line 80
  11. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.positive_active_restrict line 92
  12. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.energy_active_restrict line 104
  13. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.common_energy_active line 118
  14. def OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoredError line 142
  15. lemma OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.error_source_active line 148
  16. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoredError_data line 155
  17. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.error_live_slots line 167
  18. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoredError_volume line 174
  19. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.error_normalized_source line 185
  20. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.error_normalized_sum line 194
  21. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.error_energy line 205
  22. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.matches_child line 228
  23. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.matches_twiceChild line 239
  24. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.active_common_ray_energy line 248
  25. theorem OAI.SevenEighths.CenteredMomentEnergyAmplifiedRayDictionary.restoredError_matches line 270