OAI/NumberTheory/DirichletL/GaussSum/FixedRayFibers.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CompletedGauss.FreeReflection.FixedBranchIndex line 82
  2. def OAI.CompletedGauss.FreeReflection.fixedRayFiber line 85
  3. lemma OAI.CompletedGauss.FreeReflection.fixedRayFiber_pool line 103
  4. theorem OAI.CompletedGauss.FreeReflection.fixedRayFiber_value line 110
  5. def OAI.CompletedGauss.residualArgumentPhase line 156
  6. lemma OAI.CompletedGauss.residualArgumentPhase_norm_le_one line 159
  7. theorem OAI.CompletedGauss.residual_bracket_extracted_argument line 162
  8. def OAI.CompletedGauss.residualArgumentRowPhase line 180
  9. lemma OAI.CompletedGauss.residualArgumentRowPhase_norm_le_one line 184
  10. theorem OAI.CompletedGauss.residual_coefficient_eq_canonical_argument line 192
  11. lemma OAI.CompletedGauss.reflectedBranch_local_support line 223
  12. lemma OAI.CompletedGauss.reflectionExtractedDivisor_dvd_of_local line 238
  13. theorem OAI.CompletedGauss.reflectedBranch_extracted_divisibility line 265
  14. def OAI.CompletedGauss.fixedCuspBranchNumerator line 282
  15. theorem OAI.CompletedGauss.fixedCuspBranchNumerator_support line 289
  16. def OAI.CompletedGauss.nonzeroDualDilation line 312
  17. lemma OAI.CompletedGauss.nonzeroDualDilation_injective line 317
  18. theorem OAI.CompletedGauss.tsum_nonzeroDualDilation line 329
  19. theorem OAI.CompletedGauss.fixedCuspBranch_tsum_extract line 362
  20. lemma OAI.CubicEisenstein.fixedConjugateCuspArray_nonzero line 396
  21. lemma OAI.CubicEisenstein.fixedCusp_ramified_index_pos line 409
  22. def OAI.CubicEisenstein.sourcePhaseUnit line 427
  23. def OAI.CubicEisenstein.sourcePhaseExponent line 430
  24. lemma OAI.CubicEisenstein.paperLambdaQuotient_succ line 433
  25. theorem OAI.CubicEisenstein.sourceCuspPhaseNumerator_columns line 453
  26. theorem OAI.CubicEisenstein.fixedCuspArray_phase_brackets line 476
  27. def OAI.CubicEisenstein.FixedCuspShape.phaseUpperUnit line 501
  28. lemma OAI.CubicEisenstein.FixedCuspShape.phaseUpperUnit_val line 503
  29. def OAI.CubicEisenstein.FixedCuspShape.modelDualNumerator line 505
  30. theorem OAI.CubicEisenstein.FixedCuspShape.model_array_brackets line 508
  31. def OAI.CubicEisenstein.ControlledStratumArithmetic.activePhase line 552
  32. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.activePhase_norm line 558
  33. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.bracketProduct_eq line 571
  34. def OAI.CubicEisenstein.ControlledStratumArithmetic.modelRowPhase line 578
  35. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.modelRowPhase_norm line 586
  36. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.model_coefficient line 597
  37. lemma OAI.CubicEisenstein.fixed_stratum_kernel_scale line 623