OAI/NumberTheory/DirichletL/MeanSquare/TransformedColumns.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InitialMeanSquare.inputColumn line 85
  2. def OAI.InitialMeanSquare.transformedColumn line 88
  3. lemma OAI.InitialMeanSquare.inputColumn_eq line 95
  4. lemma OAI.InitialMeanSquare.transformedColumn_eq line 100
  5. theorem OAI.InitialMeanSquare.transformedColumn_union line 106
  6. def OAI.InitialMeanSquare.initialPair line 117
  7. lemma OAI.InitialMeanSquare.initialPair_eq line 124
  8. def OAI.InitialMeanSquare.childSum line 130
  9. lemma OAI.InitialMeanSquare.childSum_eq line 134
  10. theorem OAI.InitialMeanSquare.initialPair_eq_children line 140
  11. instance OAI.CubicEisenstein.fullSLContinuousAction line 159
  12. instance OAI.CubicEisenstein.hyperbolicVolume_fullSupport line 162
  13. instance OAI.CubicEisenstein.kernelQuotientVolume_fullSupport line 179
  14. lemma OAI.CubicEisenstein.kernel_continuous_eq_of_ae_eq line 208
  15. lemma OAI.CubicEisenstein.integral_upper_triangular_height line 221
  16. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_high_zero line 234
  17. theorem OAI.CubicEisenstein.kernelQuotientDefect_hasCompactSupport line 267
  18. def OAI.CubicEisenstein.hyperbolicSpatialCoordinates line 283
  19. lemma OAI.CubicEisenstein.hyperbolicSpatialCoordinates_continuous line 286
  20. lemma OAI.CubicEisenstein.hyperbolicSpatialCoordinates_positive line 294
  21. lemma OAI.CubicEisenstein.hyperbolicSpatialCoordinates_reconstruct line 297
  22. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_continuous line 305
  23. lemma OAI.CubicEisenstein.kernelQuotientDefect_continuous line 318
  24. lemma OAI.CubicEisenstein.actual_smoothCuspSeedDefect_contDiffAt line 322
  25. theorem OAI.SecondPassArithmetic.globalChildBudget_height line 345
  26. theorem OAI.SecondPassArithmetic.globalChildBudget_density line 361
  27. theorem OAI.SecondPassArithmetic.globalChildBudget_integral line 370
  28. def OAI.SecondPassArithmetic.globalFirstFiniteEnergy line 380
  29. theorem OAI.SecondPassArithmetic.globalFirstFiniteEnergy_integrable line 386
  30. theorem OAI.CanonicalQuadraticSieve.finite_inverse_norm_sum line 413
  31. theorem OAI.CanonicalQuadraticSieve.ideal_reciprocal_cauchy line 447
  32. def OAI.CanonicalQuadraticSieve.columnSquareFiber line 461
  33. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_injective line 464
  34. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_bounds line 476
  35. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_card line 494
  36. theorem OAI.CanonicalQuadraticSieve.columnSquareFiber_energy line 513
  37. theorem OAI.CanonicalQuadraticSieve.columnSquareParts_bounds line 568
  38. theorem OAI.CanonicalQuadraticSieve.bounded_supported_quadratic_norm line 585