OAI/Geometry/Cannon/Beltrami/CauchySymbol.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonBeltrami.integral_inverse_fourier_mul line 23
  2. lemma OAI.CannonBeltrami.inverse_fourier_l2_test line 35
  3. lemma OAI.CannonBeltrami.inverse_fourier_l2_real_test line 51
  4. lemma OAI.CannonBeltrami.continuous_inverse_fourier line 64
  5. theorem OAI.CannonBeltrami.inverse_fourier_l2_ae line 69
  6. lemma OAI.CannonBeltrami.SmoothL2.representative_ae line 83
  7. lemma OAI.CannonBeltrami.SmoothL2.beurling line 90
  8. lemma OAI.CannonBeltrami.fourierSMulRight_inverse line 93
  9. lemma OAI.CannonBeltrami.SmoothL2.integrable_fourierSMulRight line 102
  10. theorem OAI.CannonBeltrami.SmoothL2.representative_derivative line 111
  11. lemma OAI.CannonBeltrami.smooth_beltrami_equation line 130
  12. lemma OAI.CannonBeltrami.smooth_beltrami_compactSupport line 147
  13. theorem OAI.CannonBeltrami.solve_compact_smooth_beltrami line 162
  14. def OAI.CannonBeltrami.cauchySymbol line 186
  15. lemma OAI.CannonBeltrami.measurable_cauchySymbol line 188
  16. lemma OAI.CannonBeltrami.norm_cauchySymbol line 192
  17. lemma OAI.CannonBeltrami.cauchySymbol_le_on_compl line 195
  18. lemma OAI.CannonBeltrami.cauchy_fourier_moments line 201
  19. lemma OAI.CannonBeltrami.cauchy_fourier_integrable line 234
  20. def OAI.CannonBeltrami.cauchyTransform line 240
  21. lemma OAI.CannonBeltrami.contDiff_cauchyTransform line 243
  22. lemma OAI.CannonBeltrami.cauchyTransform_zero_at_infty line 253
  23. lemma OAI.CannonBeltrami.schwartz_smoothL2 line 268
  24. lemma OAI.CannonBeltrami.smoothRepresentative_schwartz line 271
  25. def OAI.CannonBeltrami.smoothBeurling line 277
  26. lemma OAI.CannonBeltrami.contDiff_smoothBeurling line 280
  27. lemma OAI.CannonBeltrami.smoothBeurling_fourier line 283
  28. lemma OAI.CannonBeltrami.inverse_fourier_derivative line 293
  29. lemma OAI.CannonBeltrami.cauchySymbol_x line 309
  30. lemma OAI.CannonBeltrami.cauchySymbol_y line 318
  31. lemma OAI.CannonBeltrami.integrable_beurling_fourier line 329
  32. lemma OAI.CannonBeltrami.inverseFourier_add line 336
  33. lemma OAI.CannonBeltrami.inverseFourier_mul line 342
  34. lemma OAI.CannonBeltrami.inverseFourier_sub line 347
  35. lemma OAI.CannonBeltrami.cauchyTransform_derivative_x line 354
  36. lemma OAI.CannonBeltrami.cauchyTransform_derivative_y line 369
  37. def OAI.CannonBeltrami.partialZ line 384
  38. def OAI.CannonBeltrami.partialBar line 387
  39. theorem OAI.CannonBeltrami.cauchyTransform_partials line 390
  40. lemma OAI.CannonBeltrami.realCLM_apply line 399
  41. lemma OAI.CannonBeltrami.fderiv_wirtinger line 406
  42. lemma OAI.CannonBeltrami.differentiableAt_of_partialBar_zero line 416
  43. lemma OAI.CannonBeltrami.partialBar_zero_of_differentiableAt line 424
  44. lemma OAI.CannonBeltrami.partials_const line 437
  45. lemma OAI.CannonBeltrami.partials_id line 441
  46. lemma OAI.CannonBeltrami.partials_add line 445
  47. lemma OAI.CannonBeltrami.partials_sub line 456
  48. lemma OAI.CannonBeltrami.partials_mul line 467
  49. lemma OAI.CannonBeltrami.partials_exp line 477
  50. lemma OAI.CannonBeltrami.contDiff_partials line 484
  51. lemma OAI.CannonBeltrami.wirtinger_commute line 492
  52. lemma OAI.CannonBeltrami.liouville_partialBar line 526