OAI/Geometry/Cannon/Beltrami/Axis.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonBeltrami.multiplier_strong_convergence_filter line 25
  2. lemma OAI.CannonBeltrami.multiplier_variable_convergence line 61
  3. lemma OAI.CannonBeltrami.multiplier_coefficient_slope line 79
  4. theorem OAI.CannonBeltrami.hasDerivAt_multiplier_product line 100
  5. lemma OAI.CannonBeltrami.translate_multiplier line 137
  6. lemma OAI.CannonBeltrami.lipschitz_coefficient_quotient line 154
  7. theorem OAI.CannonBeltrami.hasDerivAt_translate_multiplier line 168
  8. theorem OAI.CannonBeltrami.differentiated_beltrami line 195
  9. lemma OAI.CannonBeltrami.translateL2_comp line 225
  10. lemma OAI.CannonBeltrami.hasDerivAt_translateL2_at line 234
  11. lemma OAI.CannonBeltrami.translation_line_bound line 250
  12. theorem OAI.CannonBeltrami.translation_bound_of_coordinate_derivatives line 259
  13. theorem OAI.CannonBeltrami.beltrami_solution_difference line 281
  14. theorem OAI.CannonBeltrami.beltrami_translation_estimate line 310
  15. theorem OAI.CannonBeltrami.beltrami_difference_quotient_bound line 339
  16. def OAI.CannonBeltrami.axis line 357
  17. def OAI.CannonBeltrami.Sobolev line 359
  18. def OAI.CannonBeltrami.BoundedSmooth line 364
  19. lemma OAI.CannonBeltrami.BoundedSmooth.zero line 370
  20. lemma OAI.CannonBeltrami.Sobolev.add line 376
  21. lemma OAI.CannonBeltrami.hasDerivAt_translate_beurling line 389
  22. lemma OAI.CannonBeltrami.Sobolev.beurling line 396
  23. lemma OAI.CannonBeltrami.coefficient_derivative_bound line 405
  24. lemma OAI.CannonBeltrami.Sobolev.multiplier line 414
  25. lemma OAI.CannonBeltrami.Sobolev.translation_bound line 434
  26. theorem OAI.CannonBeltrami.beltrami_sobolev line 441
  27. lemma OAI.CannonBeltrami.schwartz_lipschitz line 476
  28. lemma OAI.CannonBeltrami.schwartz_line_derivative line 484
  29. lemma OAI.CannonBeltrami.schwartz_boundedSmooth line 491
  30. lemma OAI.CannonBeltrami.fourier_schwartz_derivative_ae line 500
  31. lemma OAI.CannonBeltrami.hasDerivAt_translateL2_of_fourier line 513
  32. lemma OAI.CannonBeltrami.schwartz_translation_derivative line 527
  33. lemma OAI.CannonBeltrami.schwartz_sobolev line 532
  34. theorem OAI.CannonBeltrami.solve_schwartz_beltrami line 539
  35. lemma OAI.CannonBeltrami.Sobolev.smul line 549
  36. lemma OAI.CannonBeltrami.Sobolev.sub line 561
  37. def OAI.CannonBeltrami.SmoothL2 line 565
  38. lemma OAI.CannonBeltrami.SmoothL2.derivative line 567
  39. lemma OAI.CannonBeltrami.directionSymbol_square_sum line 583
  40. lemma OAI.CannonBeltrami.bessel_pointwise line 597
  41. lemma OAI.CannonBeltrami.fourier_bessel_ae line 609
  42. lemma OAI.CannonBeltrami.SmoothL2.bessel_step line 622
  43. lemma OAI.CannonBeltrami.SmoothL2.fourier_weighted_memLp line 635
  44. lemma OAI.CannonBeltrami.inverse_weight_memLp line 649
  45. lemma OAI.CannonBeltrami.SmoothL2.fourier_weighted_integrable line 660
  46. lemma OAI.CannonBeltrami.SmoothL2.fourier_moments line 673
  47. lemma OAI.CannonBeltrami.SmoothL2.fourier_integrable line 686
  48. def OAI.CannonBeltrami.smoothRepresentative line 691
  49. lemma OAI.CannonBeltrami.SmoothL2.contDiff line 693