OAI/NumberTheory/DirichletL/Eisenstein/LocalCutoffs.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CubicEisenstein.PositiveChartCutoff line 81
  2. lemma OAI.CubicEisenstein.kernelChartCutoff_exists line 87
  3. def OAI.CubicEisenstein.kernelLocalizedField line 105
  4. lemma OAI.CubicEisenstein.kernelLocalizedField_compact line 108
  5. lemma OAI.CubicEisenstein.kernelLocalizedField_tsupport line 111
  6. lemma OAI.CubicEisenstein.kernelLocalizedField_smooth line 114
  7. def OAI.CubicEisenstein.kernelLocalizedSchwartz line 126
  8. lemma OAI.CubicEisenstein.kernelLocalizedSchwartz_coe line 130
  9. def OAI.CubicEisenstein.kernelLocalizedH1 line 133
  10. lemma OAI.CubicEisenstein.kernelLocalizedH1_embedding line 140
  11. lemma OAI.CubicEisenstein.kernelLocalizedH1_gradient line 144
  12. lemma OAI.CubicEisenstein.kernelLocalizedField_fderiv line 148
  13. lemma OAI.CubicEisenstein.complex_norm_add_sq_le line 158
  14. lemma OAI.CubicEisenstein.kernelLocalizedField_energy_bound line 164
  15. def OAI.CubicEisenstein.kernelEuclideanProjection line 201
  16. lemma OAI.CubicEisenstein.kernelEuclideanProjection_measurable line 204
  17. lemma OAI.CubicEisenstein.euclideanToHyperbolic_measurePreserving_on line 207
  18. lemma OAI.CubicEisenstein.euclideanToHyperbolic_image_positive line 220
  19. lemma OAI.CubicEisenstein.kernelEuclideanProjection_measurePreserving_on line 230
  20. lemma OAI.CubicEisenstein.kernelEuclideanProjection_integral line 252
  21. lemma OAI.CubicEisenstein.kernelEuclideanProjection_integral_le line 263
  22. lemma OAI.CubicEisenstein.kernelLocalEnergy_le line 272
  23. lemma OAI.CubicEisenstein.kernelSmoothTestsToL2_norm_sq line 280
  24. lemma OAI.CubicEisenstein.kernelLocalMass_le line 295
  25. lemma OAI.CubicEisenstein.euclideanVolume_le_heightCube_hyperbolic line 303
  26. lemma OAI.CubicEisenstein.kernelEuclideanProjection_volume_integral_le line 326
  27. theorem OAI.CompletedGauss.completed_scaled_shape line 351
  28. theorem OAI.CompletedGauss.completedBranchScale_div line 365
  29. theorem OAI.CompletedGauss.completed_reflected_fiber_fixed_scale line 372
  30. structure OAI.CompletedGauss.ReflectedBranchData line 425
  31. def OAI.CompletedGauss.ReflectedBranchData.value line 447
  32. theorem OAI.CompletedGauss.ReflectedBranchData.energy_bound line 455
  33. structure OAI.CompletedGauss.ReflectedFiberData line 475
  34. def OAI.CompletedGauss.ReflectedFiberData.value line 485
  35. theorem OAI.CompletedGauss.ReflectedFiberData.finite_energy_bound line 489
  36. theorem OAI.CompletedGauss.ReflectedFiberData.energy_bound line 513
  37. theorem OAI.CompletedGauss.one_le_completedResidualScale line 562
  38. def OAI.CompletedGauss.ReflectedFiberData.idealValue line 573
  39. theorem OAI.CompletedGauss.ReflectedFiberData.idealValue_at line 577
  40. def OAI.CompletedGauss.HasExactCompletedModels line 584
  41. theorem OAI.CompletedGauss.completed_energy_of_exact_models line 592