OAI/NumberTheory/DirichletL/RowCompletion/RowAmplitudes.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CanonicalRowCompletion.GoodMaskRowData.activeStratum line 90
  2. def OAI.CanonicalRowCompletion.GoodMaskRowData.sourceRowScalar line 93
  3. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.sourceRowScalar_norm line 103
  4. def OAI.CanonicalRowCompletion.GoodMaskRowData.sourceRowResidue line 126
  5. def OAI.CanonicalRowCompletion.GoodMaskRowData.selectedSourceRowScalar line 130
  6. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.selectedSourceRowScalar_norm line 135
  7. lemma OAI.CanonicalRowCompletion.GoodMaskRowData.sum_selectedSourceRowScalar line 145
  8. theorem OAI.CanonicalRowCompletion.GoodMaskRowData.completedT_eq_actualControlledSource line 160
  9. def OAI.CanonicalRowCompletion.residualActivePrimes line 184
  10. lemma OAI.CanonicalRowCompletion.residualActivePrimes_not_inr line 188
  11. def OAI.CanonicalRowCompletion.nonresidualComplementMap line 194
  12. lemma OAI.CanonicalRowCompletion.nonresidualComplementMap_bijective line 198
  13. def OAI.CanonicalRowCompletion.nonresidualComplementEquiv line 210
  14. lemma OAI.CanonicalRowCompletion.nonresidualComplementEquiv_val line 215
  15. lemma OAI.CanonicalRowCompletion.complementActive_image line 219
  16. lemma OAI.CanonicalRowCompletion.inactive_product_nonresidual line 225
  17. theorem OAI.CanonicalRowCompletion.inactive_weight_nonresidual_subsets line 237
  18. lemma OAI.CompletedGauss.active_product_residual_equiv line 263
  19. lemma OAI.CompletedGauss.actual_bracket_ideal_congr line 276
  20. theorem OAI.CompletedGauss.residual_equiv_coefficient line 283
  21. theorem OAI.CubicEisenstein.FixedFourierGeometry.stratumBranchTerm_tsum_eq_rawValue line 333
  22. def OAI.CanonicalRowCompletion.HasFixedShellModels line 410
  23. lemma OAI.CanonicalRowCompletion.normTwistedSource_contDiff line 421
  24. theorem OAI.CanonicalRowCompletion.hasCanonicalThetaModels_of_fixed_shell_models line 431
  25. lemma OAI.CompletedGauss.ReflectedBranchData.rawValue_congr_phase_at line 476
  26. lemma OAI.CompletedGauss.ReflectedBranchData.rawValue_zero_phase line 483
  27. lemma OAI.CompletedGauss.ReflectedBranchData.rawValue_mul_phase_at line 487
  28. lemma OAI.CompletedGauss.ReflectedBranchData.rawValue_select_phase_at line 496
  29. def OAI.CanonicalRowCompletion.completeActiveSet line 516
  30. lemma OAI.CanonicalRowCompletion.completeActiveSet_residual line 520
  31. lemma OAI.CanonicalRowCompletion.optionalPrimeActive_completeActiveSet line 525
  32. def OAI.CanonicalRowCompletion.selectedActiveEquiv line 538
  33. lemma OAI.CanonicalRowCompletion.selectedActiveEquiv_inl line 549
  34. lemma OAI.CanonicalRowCompletion.selectedActiveEquiv_inr line 553
  35. def OAI.CanonicalRowCompletion.ActualFiber.maskElement line 564
  36. def OAI.CanonicalRowCompletion.ActualFiber.maskIdeal line 565
  37. def OAI.CanonicalRowCompletion.ActualFiber.freeConductor line 566
  38. abbrev OAI.CanonicalRowCompletion.ActualFiber.RowIndex line 567
  39. lemma OAI.CanonicalRowCompletion.ActualFiber.maskElement_ne_zero line 570
  40. lemma OAI.CanonicalRowCompletion.ActualFiber.maskIdeal_ne_zero line 572
  41. lemma OAI.CanonicalRowCompletion.ActualFiber.mask_bad line 574
  42. def OAI.CanonicalRowCompletion.ActualFiber.data line 581
  43. def OAI.CanonicalRowCompletion.ActualFiber.splitIndex line 586
  44. def OAI.CanonicalRowCompletion.ActualFiber.activeSet line 598
  45. def OAI.CanonicalRowCompletion.ActualFiber.columnDivisor line 603
  46. def OAI.CanonicalRowCompletion.ActualFiber.rowScalar line 612
  47. lemma OAI.CanonicalRowCompletion.ActualFiber.rowScalar_norm line 623
  48. def OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber line 635
  49. lemma OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber_rowPhase line 643