OAI/NumberTheory/DirichletL/RowCompletion/SupportBounds.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalRowCompletion.localRowValue_zero_of_mem line 84
  2. theorem OAI.CanonicalRowCompletion.idealRowHom_zero_of_dvd line 93
  3. theorem OAI.CanonicalRowCompletion.columnWeight_zero_of_mask line 101
  4. theorem OAI.CanonicalRowCompletion.columnWeight_zero_of_not_squarefree line 120
  5. theorem OAI.CanonicalRowCompletion.weighted_column_support line 124
  6. theorem OAI.CanonicalRowCompletion.weighted_column_tsum_eq line 146
  7. theorem OAI.CanonicalRowCompletion.localRowValue_mul line 165
  8. theorem OAI.CanonicalRowCompletion.idealRowHom_argument_mul line 173
  9. theorem OAI.CanonicalRowCompletion.rowTwist_row_factor line 190
  10. theorem OAI.CanonicalRowCompletion.cubeWeight_row_factor line 198
  11. theorem OAI.CanonicalRowCompletion.idealRowHom_prime_powers line 217
  12. theorem OAI.CanonicalRowCompletion.cubeWeight_prime_powers line 227
  13. def OAI.CanonicalRowCompletion.excludedGenerator line 243
  14. theorem OAI.CanonicalRowCompletion.excludedGenerator_mem line 245
  15. theorem OAI.CanonicalRowCompletion.excludedGenerator_not_mem_pool line 253
  16. theorem OAI.CanonicalRowCompletion.outside_pool_fixed_mask line 271
  17. theorem OAI.CanonicalRowCompletion.canonicalSourceCoefficient_fixed_mask line 283
  18. def OAI.CanonicalRowCompletion.outsideCanonicalRow line 303
  19. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_eq_global line 313
  20. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_cube_inverse line 341
  21. theorem OAI.CanonicalRowCompletion.outsideCanonicalRow_cube_split line 353
  22. def OAI.CanonicalRowCompletion.cubeIndex line 371
  23. theorem OAI.CanonicalRowCompletion.cubeIndex_apply line 374
  24. def OAI.CanonicalRowCompletion.cubeIdeal line 378
  25. theorem OAI.CanonicalRowCompletion.cubeIdeal_cubeIndex line 381
  26. theorem OAI.CanonicalRowCompletion.cubeIndex_inj line 396
  27. theorem OAI.CanonicalRowCompletion.outside_cubeIdeal_cubeIndex line 403
  28. theorem OAI.CanonicalRowCompletion.sum_outside_cubeIndex line 410
  29. theorem OAI.CanonicalRowCompletion.cubeIdeal_ne_zero line 424
  30. theorem OAI.CanonicalRowCompletion.cubeIdeal_primaryGenerator line 429
  31. theorem OAI.SecondPassIntegration.densityChildEnergy_canonical_terminal line 448
  32. def OAI.SecondPassArithmetic.globalQuantitativeSource line 495
  33. theorem OAI.SecondPassArithmetic.globalQuantitativeSource_block_mem line 502
  34. theorem OAI.SecondPassArithmetic.globalQuantitativeSource_frequency_ne_zero line 509
  35. theorem OAI.SecondPassArithmetic.globalFirstRayChildBudget_canonical_bound line 517
  36. theorem OAI.SecondPassArithmetic.globalFirstQuantitativeBudget_canonical_bound line 598