OAI/NumberTheory/DirichletL/Eisenstein/CutoffApproximation.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.l2_norm_sq_integral line 86
  2. lemma OAI.CubicEisenstein.l2_toLp_sub_norm_sq line 93
  3. theorem OAI.CubicEisenstein.l2_tendsto_of_bounded_eventuallyEq line 102
  4. instance OAI.CubicEisenstein.kernelFundamentalVolume_finite line 131
  5. def OAI.CubicEisenstein.kernelFunctionField line 138
  6. lemma OAI.CubicEisenstein.kernelFunctionField_smooth line 141
  7. def OAI.CubicEisenstein.kernelFunctionGradient line 148
  8. lemma OAI.CubicEisenstein.kernelFunctionGradient_continuous line 152
  9. lemma OAI.CubicEisenstein.norm_three_vector_bound line 164
  10. lemma OAI.CubicEisenstein.kernelFunctionGradient_bound line 174
  11. lemma OAI.CubicEisenstein.kernelFunctionGradient_memLp line 182
  12. def OAI.CubicEisenstein.kernelFunctionCutoff line 191
  13. lemma OAI.CubicEisenstein.kernelFunctionCutoff_apply line 203
  14. lemma OAI.CubicEisenstein.kernelFunctionCutoff_field line 207
  15. lemma OAI.CubicEisenstein.kernelFunctionGradient_of_test line 212
  16. lemma OAI.CubicEisenstein.kernelFunctionCutoff_field_eventually line 218
  17. lemma OAI.CubicEisenstein.kernelFunctionCutoff_gradient_eventually line 232
  18. lemma OAI.CubicEisenstein.kernelFunctionCutoff_mass_bound line 243
  19. lemma OAI.CubicEisenstein.kernelFunctionCutoff_scaled_deriv_bound line 250
  20. lemma OAI.CubicEisenstein.kernelFunctionCutoff_gradient_bound line 285
  21. theorem OAI.CubicEisenstein.kernelFunctionCutoff_mass_tendsto line 302
  22. theorem OAI.CubicEisenstein.kernelFunctionCutoff_gradient_tendsto line 316
  23. theorem OAI.CubicEisenstein.kernel_bounded_smooth_energy_exists line 331
  24. def OAI.CubicEisenstein.kernelEisensteinRemainderL2 line 352
  25. lemma OAI.CubicEisenstein.kernelEisensteinRemainderL2_ae line 357
  26. theorem OAI.CubicEisenstein.kernelEisensteinRemainder_energy line 363
  27. lemma OAI.CubicEisenstein.axis_update_contDiff line 386
  28. lemma OAI.CubicEisenstein.smooth_positive_axis_regular line 395
  29. lemma OAI.CubicEisenstein.axisLaplacian_sub_smooth line 406
  30. lemma OAI.CubicEisenstein.eisensteinRemainder_coordinate_equation line 426
  31. lemma OAI.CubicEisenstein.kernelQuotientDefect_euclidean_eq line 436
  32. theorem OAI.CubicEisenstein.kernelEisensteinRemainder_operator_equation line 446
  33. lemma OAI.CubicEisenstein.kernelFunctionCutoff_uniform_near line 467
  34. lemma OAI.CubicEisenstein.kernelBoundedFunction_form_equation line 491
  35. theorem OAI.CubicEisenstein.kernel_bounded_smooth_operator_graph line 520
  36. theorem OAI.CubicEisenstein.kernelEisensteinRemainderL2_graph line 553
  37. theorem OAI.CubicEisenstein.kernelEisensteinL2Correction_eq_remainder line 586
  38. theorem OAI.CubicEisenstein.kernelEisensteinL2Correction_initial_overlap line 595