OAI/NumberTheory/DirichletL/Eisenstein/ReflectionFibers.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.FixedFourierGeometry.stratum_model_coefficient line 88
  2. theorem OAI.CubicEisenstein.FixedFourierGeometry.reflectedValue_eq_model_series line 100
  3. abbrev OAI.CubicEisenstein.CuspIdealIndex line 149
  4. def OAI.CubicEisenstein.thetaFullToIdealIndex line 151
  5. lemma OAI.CubicEisenstein.thetaFullToIdealIndex_injective line 154
  6. lemma OAI.CubicEisenstein.fixedCuspArrayWithPhase_eligible line 163
  7. theorem OAI.CubicEisenstein.fixedCuspArrayWithPhase_tsum_primary_pairs line 169
  8. theorem OAI.CubicEisenstein.fixedCuspArrayWithPhase_tsum_full_index line 192
  9. def OAI.CompletedGauss.mandatoryActiveEquiv line 225
  10. lemma OAI.CompletedGauss.sum_mandatory_active line 252
  11. theorem OAI.CompletedGauss.inactive_weight_mandatory_active line 271
  12. lemma OAI.CompletedGauss.inactive_product_complement line 286
  13. theorem OAI.CompletedGauss.inactive_weight_optional_active line 311
  14. lemma OAI.CanonicalRowCompletion.excluded_prime_dvd_row_mask line 328
  15. lemma OAI.CanonicalRowCompletion.residual_prime_not_excluded line 336
  16. lemma OAI.CanonicalRowCompletion.residual_coprime_fixed_conductor line 344
  17. def OAI.CompletedGauss.representativeRowFiber line 370
  18. def OAI.CompletedGauss.reconstructFiberRow line 373
  19. lemma OAI.CompletedGauss.reconstructFiberRow_ne_zero line 376
  20. lemma OAI.CompletedGauss.reconstructFiberRow_of_original line 380
  21. lemma OAI.CompletedGauss.residual_reconstructFiberRow line 387
  22. lemma OAI.CompletedGauss.representativeRowFiber_injective line 394
  23. def OAI.CompletedGauss.fiberResidualIndex line 399
  24. lemma OAI.CompletedGauss.fiberResidualIndex_injective line 406
  25. def OAI.CompletedGauss.extendFiberRowScalar line 415
  26. lemma OAI.CompletedGauss.extendFiberRowScalar_norm_le_one line 421
  27. lemma OAI.CompletedGauss.extendFiberRowScalar_zero line 430
  28. lemma OAI.CompletedGauss.extendFiberRowScalar_at_original line 437
  29. def OAI.CompletedGauss.extendSelectedFiberRowScalar line 447
  30. lemma OAI.CompletedGauss.extendSelectedFiberRowScalar_norm_le_one line 454
  31. lemma OAI.CompletedGauss.extendSelectedFiberRowScalar_at_original line 466
  32. lemma OAI.CompletedGauss.sum_extendSelectedFiberRowScalar line 478
  33. theorem OAI.CompletedGauss.reconstructFiberRow_valid_iff line 494
  34. lemma OAI.CompletedGauss.representativeFiber_parts line 511
  35. lemma OAI.CompletedGauss.representativeFiber_pool line 516
  36. lemma OAI.CompletedGauss.representativeFiber_filtered_pool line 524
  37. lemma OAI.CompletedGauss.representativeFiber_exponent line 530
  38. lemma OAI.CompletedGauss.representativeFiber_extractedDivisor line 538
  39. lemma OAI.CompletedGauss.representativeFiber_residualScale line 551
  40. lemma OAI.CompletedGauss.representativeFiber_branchScale line 557
  41. def OAI.CompletedGauss.FreeReflection.fixedRayFiberFromRows line 575
  42. lemma OAI.CompletedGauss.FreeReflection.fixedRayFiberFromRows_rowPhase line 584
  43. lemma OAI.CompletedGauss.FreeReflection.fixedRayFiberFromRows_weight line 601