OAI/NumberTheory/DirichletL/Eisenstein/SmoothTests.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CubicEisenstein.hyperbolicSpatialChartedSpace line 79
  2. instance OAI.CubicEisenstein.hyperbolicSpatialIsManifold line 82
  3. lemma OAI.CubicEisenstein.kernelLocalLift_source_out line 85
  4. instance OAI.CubicEisenstein.kernelSpatialChartedSpace line 90
  5. instance OAI.CubicEisenstein.kernelSpatialIsManifold line 96
  6. lemma OAI.CubicEisenstein.hyperbolicSpatial_chartAt line 103
  7. lemma OAI.CubicEisenstein.kernelSpatial_chartAt line 106
  8. lemma OAI.CubicEisenstein.kernelProjection_contMDiff line 109
  9. def OAI.CubicEisenstein.kernelSmoothTests line 140
  10. lemma OAI.CubicEisenstein.kernelSmoothTests_memLp line 148
  11. def OAI.CubicEisenstein.kernelSmoothTestsToL2 line 152
  12. lemma OAI.CubicEisenstein.kernelSmoothTestsToL2_injective line 157
  13. lemma OAI.CubicEisenstein.kernelL2_smooth_compact_approx line 163
  14. lemma OAI.CubicEisenstein.kernelSmoothTestsToL2_dense line 205
  15. lemma OAI.CubicEisenstein.hyperbolicSpatialChart_symm_eq line 226
  16. lemma OAI.CubicEisenstein.kernelQuotientDefect_coordinate line 235
  17. lemma OAI.CubicEisenstein.kernelQuotientDefect_contMDiff line 243
  18. def OAI.CubicEisenstein.kernelDefectSmoothTest line 263
  19. lemma OAI.CubicEisenstein.kernelDefectSmoothTest_toL2 line 267
  20. lemma OAI.InitialMeanSquare.quotient_span_fixed line 286
  21. lemma OAI.InitialMeanSquare.quotient_norm_fixed line 292
  22. lemma OAI.InitialMeanSquare.residualScale_fixed line 297
  23. theorem OAI.InitialMeanSquare.postCommonSmoothPair_fixed_mask line 306
  24. theorem OAI.InitialMeanSquare.sourceWeight_norm_fixed line 318
  25. lemma OAI.InitialMeanSquare.normCharacter_norm_le_one line 330
  26. lemma OAI.InitialMeanSquare.conjugateMonoid_norm_le_one line 333
  27. def OAI.InitialMeanSquare.sourceLogZ line 346
  28. def OAI.InitialMeanSquare.sourceLogE line 348
  29. def OAI.InitialMeanSquare.sourceLogV line 350
  30. def OAI.InitialMeanSquare.sourceLogK line 352
  31. theorem OAI.InitialMeanSquare.initial_sector_fixed_profiles line 356
  32. theorem OAI.InitialMeanSquare.initial_sector_transfer line 411
  33. theorem OAI.SecondPassArithmetic.descent_ideal_inverse_sum line 492
  34. theorem OAI.SecondPassArithmetic.descent_normLogBin_small_power line 528
  35. def OAI.SecondPassArithmetic.cubeProductIdeal line 547
  36. def OAI.SecondPassArithmetic.cubeParityKey line 551
  37. def OAI.SecondPassArithmetic.cubeDivisorKey line 556
  38. theorem OAI.SecondPassArithmetic.cubeParityKey_product line 561
  39. theorem OAI.SecondPassArithmetic.cubeDivisorKey_dvd line 570
  40. theorem OAI.SecondPassArithmetic.cubeParityKey_ne_zero line 586
  41. theorem OAI.SecondPassArithmetic.cubeProductIdeal_ne_zero line 594
  42. theorem OAI.SecondPassArithmetic.cubeDivisorKey_injective_on_product line 601
  43. theorem OAI.SecondPassArithmetic.cubeParityKey_fiber_card line 628