OAI/NumberTheory/DirichletL/RowCompletion/CompletedEnergy.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalRowCompletion.outsideLogEnergy line 85
  2. theorem OAI.CanonicalRowCompletion.outsideLogEnergy_eq_completed line 94
  3. def OAI.CanonicalRowCompletion.HasCanonicalThetaModels line 104
  4. theorem OAI.CanonicalRowCompletion.outsideLogEnergy_terminal_constant line 121
  5. def OAI.CompletedGauss.fractionalThetaPoint line 159
  6. lemma OAI.CompletedGauss.embedding_lambda_ne_zero line 162
  7. theorem OAI.CompletedGauss.fractionalThetaPoint_clear line 169
  8. lemma OAI.CompletedGauss.embedding_lambda_norm_sq line 177
  9. theorem OAI.CompletedGauss.fractionalThetaPoint_norm_sq line 181
  10. theorem OAI.CompletedGauss.fractionalThetaPoint_ne_zero line 197
  11. theorem OAI.CompletedGauss.fractional_cusp_coefficient line 219
  12. def OAI.CompletedGauss.normalizedThetaAmplitude line 233
  13. theorem OAI.CompletedGauss.normalizedThetaAmplitude_norm line 239
  14. theorem OAI.CompletedGauss.cusp_summand_eq_local_branches line 255
  15. def OAI.CompletedGauss.paperLambda line 281
  16. def OAI.CompletedGauss.paperLambdaUnit line 283
  17. lemma OAI.CompletedGauss.paperLambdaUnit_six line 295
  18. lemma OAI.CompletedGauss.paperLambda_eq line 301
  19. lemma OAI.CompletedGauss.paperLambda_embedding_ne_zero line 308
  20. def OAI.CompletedGauss.paperFractionalThetaPoint line 312
  21. def OAI.CompletedGauss.paperUnitReindex line 315
  22. lemma OAI.CompletedGauss.paperUnitReindex_apply line 317
  23. theorem OAI.CompletedGauss.paperFractionalThetaPoint_eq line 320
  24. theorem OAI.CompletedGauss.paperFractionalThetaPoint_clear line 333
  25. theorem OAI.CompletedGauss.paperFractionalThetaPoint_norm_sq line 341
  26. theorem OAI.CompletedGauss.paperIntegralArgument_eq line 346
  27. theorem OAI.CompletedGauss.paperBracket_transport line 355
  28. lemma OAI.CompletedGauss.paperLambdaUnit_four line 365
  29. theorem OAI.CompletedGauss.paperBracket_one_transport line 371
  30. lemma OAI.CanonicalCubeSeparation.columnWindowRadius_exp line 389
  31. theorem OAI.CanonicalCubeSeparation.fixed_reopening_profiles line 394
  32. lemma OAI.CanonicalCubeSeparation.fixed_reopening_child_radius line 417
  33. theorem OAI.CanonicalRowCompletion.canonicalShortState_geometry line 429
  34. theorem OAI.CanonicalRowCompletion.canonicalShortState_uniform_twist line 469
  35. def OAI.CanonicalCubeSeparation.radiusIter line 513
  36. theorem OAI.CanonicalCubeSeparation.radiusIter_zero line 517
  37. theorem OAI.CanonicalCubeSeparation.radiusIter_succ line 518
  38. theorem OAI.CanonicalCubeSeparation.radiusIter_mono_base line 521
  39. theorem OAI.CanonicalCubeSeparation.radiusIter_nonneg line 526
  40. theorem OAI.CanonicalCubeSeparation.radiusIter_mono_depth line 531
  41. theorem OAI.CanonicalCubeSeparation.le_radiusIter line 536
  42. theorem OAI.CanonicalCubeSeparation.radiusIter_child_le line 539
  43. theorem OAI.CanonicalCubeSeparation.common_pool_parent line 543
  44. theorem OAI.CanonicalCubeSeparation.common_pool_child line 549
  45. def OAI.QuadraticAllOddCRT.character line 563
  46. theorem OAI.QuadraticAllOddCRT.normalized_prime_eq_square_sum line 568
  47. theorem OAI.QuadraticAllOddCRT.normalized_product_eq_square_sum line 583
  48. theorem OAI.QuadraticAllOddCRT.quadraticGamma_product line 603