OAI/Analysis/NodalLength/Elliptic.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Profiles.l2norm_add_le line 300
  2. lemma OAI.SharpNodal.Profiles.l2norm_const_mul line 313
  3. lemma OAI.SharpNodal.Profiles.memLp_smooth_compact line 318
  4. lemma OAI.SharpNodal.Profiles.kernel_global_L2_bound line 322
  5. lemma OAI.SharpNodal.Profiles.rconv_support_bound line 329
  6. lemma OAI.SharpNodal.Profiles.l2norm_support_bound line 340
  7. def OAI.SharpNodal.Profiles.localNewton line 359
  8. lemma OAI.SharpNodal.Profiles.smooth_localNewton line 361
  9. lemma OAI.SharpNodal.Profiles.compact_localNewton line 364
  10. lemma OAI.SharpNodal.Profiles.localNewton_partial line 368
  11. lemma OAI.SharpNodal.Profiles.laplacian_localNewton line 374
  12. lemma OAI.SharpNodal.Profiles.parametrixKernel_inner line 382
  13. lemma OAI.SharpNodal.Profiles.localNewton_equation line 391
  14. lemma OAI.SharpNodal.Profiles.l2sq_hessian_cross line 407
  15. lemma OAI.SharpNodal.Profiles.l2sq_hessian_identity line 422
  16. lemma OAI.SharpNodal.Profiles.l2norm_hessian_le line 430
  17. lemma OAI.SharpNodal.Profiles.l2norm_gradient_le line 441
  18. lemma OAI.SharpNodal.Profiles.memLp_logParametrix line 453
  19. lemma OAI.SharpNodal.Profiles.localNewton_L2_bounds line 456
  20. abbrev OAI.SharpNodal.Profiles.Elliptic.Kind line 512
  21. def OAI.SharpNodal.Profiles.Elliptic.jet line 514
  22. def OAI.SharpNodal.Profiles.Elliptic.operator line 518
  23. def OAI.SharpNodal.Profiles.Elliptic.Supported line 521
  24. def OAI.SharpNodal.Profiles.Elliptic.Good line 523
  25. lemma OAI.SharpNodal.Profiles.Elliptic.good_partial line 525
  26. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_jet line 553
  27. lemma OAI.SharpNodal.Profiles.Elliptic.compact_jet line 558
  28. lemma OAI.SharpNodal.Profiles.Elliptic.partial_jet line 563
  29. lemma OAI.SharpNodal.Profiles.Elliptic.smooth_operator line 579
  30. lemma OAI.SharpNodal.Profiles.Elliptic.compact_fun_sum line 582
  31. lemma OAI.SharpNodal.Profiles.Elliptic.compact_operator line 586
  32. lemma OAI.SharpNodal.Profiles.Elliptic.supported_operator line 591
  33. lemma OAI.SharpNodal.Profiles.Elliptic.good_operator line 597
  34. lemma OAI.SharpNodal.Profiles.Elliptic.partial_sum line 600
  35. lemma OAI.SharpNodal.Profiles.Elliptic.partial_operator line 606
  36. lemma OAI.SharpNodal.Profiles.Elliptic.l2norm_mul_le line 615
  37. lemma OAI.SharpNodal.Profiles.Elliptic.l2norm_sum_le line 621
  38. lemma OAI.SharpNodal.Profiles.Elliptic.operator_L2_bound line 634
  39. lemma OAI.SharpNodal.Profiles.Elliptic.operator_L2_bounded line 649
  40. def OAI.SharpNodal.Profiles.Elliptic.SNorm line 661
  41. lemma OAI.SharpNodal.Profiles.Elliptic.SNorm_nonneg line 665
  42. lemma OAI.SharpNodal.Profiles.Elliptic.SNorm_le_succ line 670
  43. lemma OAI.SharpNodal.Profiles.Elliptic.SNorm_partial_le line 673
  44. lemma OAI.SharpNodal.Profiles.Elliptic.l2norm_le_SNorm line 677
  45. lemma OAI.SharpNodal.Profiles.Elliptic.SNorm_add_le line 682
  46. lemma OAI.SharpNodal.Profiles.Elliptic.operator_SNorm_bounded line 700
  47. lemma OAI.SharpNodal.Profiles.Elliptic.operator_SNorm_leading line 728
  48. def OAI.SharpNodal.Profiles.Elliptic.iterate line 773
  49. lemma OAI.SharpNodal.Profiles.Elliptic.good_iterate line 777
  50. lemma OAI.SharpNodal.Profiles.Elliptic.iterate_SNorm_decay line 782
  51. def OAI.SharpNodal.Profiles.Elliptic.wordPartial line 818
  52. lemma OAI.SharpNodal.Profiles.Elliptic.wordPartial_append line 822
  53. lemma OAI.SharpNodal.Profiles.Elliptic.good_wordPartial line 828
  54. lemma OAI.SharpNodal.Profiles.Elliptic.SNorm_wordPartial_le line 833
  55. lemma OAI.SharpNodal.Profiles.Elliptic.wordPartial_newton line 840
  56. structure OAI.SharpNodal.Profiles.Elliptic.Regular line 848
  57. lemma OAI.SharpNodal.Profiles.Elliptic.half_summable line 852
  58. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.summable line 855
  59. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.partial line 859
  60. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.derivative_bound line 866
  61. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.hasFDeriv line 880
  62. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.partial_tsum line 886
  63. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.contDiff_tsum line 895
  64. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.smooth_tsum line 917
  65. lemma OAI.SharpNodal.Profiles.Elliptic.regular_newton_iterate line 920
  66. def OAI.SharpNodal.Profiles.Elliptic.fieldJet line 937
  67. def OAI.SharpNodal.Profiles.Elliptic.differential line 941
  68. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.regular_fieldJet line 944
  69. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.fieldJet_tsum line 950
  70. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.differential_tsum line 958
  71. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.laplacian_tsum line 965
  72. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.summable_laplacian line 972
  73. def OAI.SharpNodal.Profiles.Elliptic.solution line 976
  74. lemma OAI.SharpNodal.Profiles.Elliptic.solution_equation line 979
  75. lemma OAI.SharpNodal.Profiles.Elliptic.operator_SNorm_one_contraction line 999
  76. lemma OAI.SharpNodal.Profiles.Elliptic.iterate_SNorm_one_decay line 1015
  77. lemma OAI.SharpNodal.Profiles.Elliptic.Regular.abs_partial_tsum_le line 1025
  78. lemma OAI.SharpNodal.Profiles.Elliptic.solution_gradient_bound line 1037