OAI/NumberTheory/DirichletL/Inversion/InitialClippedColumns.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialClippedColumns.clippedTest line 16
  2. theorem OAI.SevenEighths.InverseInitialClippedColumns.clippedTest_eq_source line 19
  3. theorem OAI.SevenEighths.InverseInitialClippedColumns.child_test_clipping line 24
  4. def OAI.SevenEighths.InverseInitialClippedColumns.freshColumns line 38
  5. theorem OAI.SevenEighths.InverseInitialClippedColumns.mem_freshColumns line 42
  6. theorem OAI.SevenEighths.InverseInitialClippedColumns.freshColumns_clipping_range line 48
  7. theorem OAI.SevenEighths.InverseInitialClippedColumns.freshColumns_initial_clipping_shift line 60
  8. theorem OAI.SevenEighths.InverseInitialClippedColumns.clippedTest_support_of_freshColumns line 75
  9. theorem OAI.SevenEighths.InverseInitialClippedColumns.canonical_row_zero_of_freshColumns_empty line 85
  10. theorem OAI.SevenEighths.InverseInitialClippedColumns.canonical_row_nonzero_freshColumns line 101
  11. theorem OAI.SevenEighths.InverseInitialClippedColumns.canonical_row_clipping line 111
  12. theorem OAI.SevenEighths.InverseInitialClippedColumns.canonical_row_clipping_norm line 128
  13. def OAI.SevenEighths.InverseInitialClippedColumns.columnEnergy line 139
  14. theorem OAI.SevenEighths.InverseInitialClippedColumns.columnEnergy_clipping line 147
  15. theorem OAI.SevenEighths.InverseInitialClippedColumns.canonical_pair_clipping line 159
  16. theorem OAI.SevenEighths.InverseInitialClippedColumns.canonical_pair_clipping_left_conjugate line 179
  17. def OAI.SevenEighths.InverseInitialClippedColumns.normalizedColumnEnergy line 199
  18. theorem OAI.SevenEighths.InverseInitialClippedColumns.columnEnergy_normalization line 208
  19. theorem OAI.SevenEighths.InverseInitialClippedColumns.initial_columnEnergy_clipping_normalized line 231
  20. def OAI.SevenEighths.InverseInitialClippedColumns.leftHeight line 246
  21. def OAI.SevenEighths.InverseInitialClippedColumns.rightHeight line 247
  22. theorem OAI.SevenEighths.InverseInitialClippedColumns.leftHeight_eq line 249
  23. theorem OAI.SevenEighths.InverseInitialClippedColumns.rightHeight_eq line 254
  24. def OAI.SevenEighths.InverseInitialClippedColumns.clippingPhase line 259
  25. theorem OAI.SevenEighths.InverseInitialClippedColumns.clippingPhase_norm line 262
  26. theorem OAI.SevenEighths.InverseInitialClippedColumns.clippingPhase_continuous line 265
  27. theorem OAI.SevenEighths.InverseInitialClippedColumns.fresh_pair_mode_clipping line 269
  28. theorem OAI.SevenEighths.InverseInitialClippedColumns.child_height_moment_bound line 295
  29. def OAI.SevenEighths.InverseInitialClippedColumns.outerCutoff line 304
  30. def OAI.SevenEighths.InverseInitialClippedColumns.retainedCutoffs line 307
  31. theorem OAI.SevenEighths.InverseInitialClippedColumns.retainedCutoffs_nonzero line 310
  32. theorem OAI.SevenEighths.InverseInitialClippedColumns.larger_windows_one line 326
  33. theorem OAI.SevenEighths.InverseInitialClippedColumns.retained_physical_kernel_restore line 336