OAI/NumberTheory/DirichletL/Energy/LiveClippingDefect.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.rowTwistedSum_support_witness line 15
  2. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.rowTwistedSum_support_scale line 32
  3. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.positiveSlotRow_support_scales line 43
  4. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.positiveSlotRow_profiles_scales line 57
  5. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.length_le_raw_add_endpoint line 66
  6. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.total_clipping_defect line 78
  7. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.endpoint_threshold line 87
  8. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.profiles_uniform_defect line 105
  9. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.total_clipping_defect_nonneg line 118
  10. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.positiveSlotRow_zero_or_defect line 127
  11. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.energy_support_witness line 141
  12. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.energy_zero_or_defect line 160
  13. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.raw_gates_of_defect line 176
  14. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_slot_budgets line 186
  15. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_defect_le_width line 195
  16. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_balanced_long_nonneg line 199
  17. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_reflected_low line 208
  18. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_reflected_low_admissible line 234
  19. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_deleted_cases line 241
  20. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_fixed_slack line 263
  21. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_deleted_reference_cases line 274
  22. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.robust_deleted_reference_window line 321
  23. theorem OAI.SevenEighths.CenteredMomentEnergyLiveClippingDefect.live_profiles_reference_window line 348