OAI/Analysis/HotSpots/Multiplier.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictHotSpots.ambientSmooth line 13
  2. lemma OAI.StrictHotSpots.ambientSmooth_smooth line 16
  3. lemma OAI.StrictHotSpots.ambientSmooth_integrable line 20
  4. lemma OAI.StrictHotSpots.ambientSmooth_lipschitz line 26
  5. lemma OAI.StrictHotSpots.ambientSmooth_tendsto line 44
  6. lemma OAI.StrictHotSpots.ambientSmooth_fderiv line 50
  7. lemma OAI.StrictHotSpots.ambientSmooth_gradient line 81
  8. lemma OAI.StrictHotSpots.lipschitz_gradient_locallyIntegrable line 93
  9. lemma OAI.StrictHotSpots.ambientSmooth_gradient_tendsto line 103
  10. lemma OAI.StrictHotSpots.HasH1Gradient.of_tendsto_L2 line 124
  11. def OAI.StrictHotSpots.planeApproxBump line 137
  12. lemma OAI.StrictHotSpots.planeApproxBump_rOut_tendsto line 145
  13. lemma OAI.StrictHotSpots.planeApproxBump_ratio line 149
  14. lemma OAI.StrictHotSpots.planeApproxBump_rOut_le_one line 156
  15. lemma OAI.StrictHotSpots.ambientSmooth_error line 161
  16. lemma OAI.StrictHotSpots.lipschitz_gradient_bound line 169
  17. lemma OAI.StrictHotSpots.lipschitz_gradient_memLp_top line 175
  18. lemma OAI.StrictHotSpots.continuous_closure_memLp_top line 182
  19. lemma OAI.StrictHotSpots.ambientSmooth_uniform_bound line 190
  20. lemma OAI.StrictHotSpots.HasH1Gradient.mul_lipschitz line 205
  21. def OAI.StrictHotSpots.H1.lipschitzMul line 253
  22. lemma OAI.StrictHotSpots.H1.lipschitzMul_value_ae line 256
  23. lemma OAI.StrictHotSpots.H1.lipschitzMul_grad_ae line 260
  24. def OAI.StrictHotSpots.PhysicalHelmholtz.pair line 282
  25. lemma OAI.StrictHotSpots.PhysicalHelmholtz.pair_apply line 286
  26. lemma OAI.StrictHotSpots.PhysicalHelmholtz.pair_comm line 289
  27. def OAI.StrictHotSpots.PhysicalHelmholtz.incl line 295
  28. def OAI.StrictHotSpots.PhysicalHelmholtz.zeroPair line 297
  29. lemma OAI.StrictHotSpots.PhysicalHelmholtz.zeroPair_apply line 302
  30. lemma OAI.StrictHotSpots.PhysicalHelmholtz.zeroPair_pair line 305
  31. lemma OAI.StrictHotSpots.PhysicalHelmholtz.zeroPair_self line 307
  32. lemma OAI.StrictHotSpots.PhysicalHelmholtz.subcritical_numeric line 313
  33. lemma OAI.StrictHotSpots.PhysicalHelmholtz.zeroPair_coercive line 324
  34. def OAI.StrictHotSpots.PhysicalHelmholtz.forcing line 338
  35. def OAI.StrictHotSpots.PhysicalHelmholtz.correction line 343
  36. def OAI.StrictHotSpots.PhysicalHelmholtz.extension line 350
  37. lemma OAI.StrictHotSpots.PhysicalHelmholtz.correction_spec line 356
  38. lemma OAI.StrictHotSpots.PhysicalHelmholtz.extension_class line 366
  39. lemma OAI.StrictHotSpots.PhysicalHelmholtz.extension_weak line 372
  40. lemma OAI.StrictHotSpots.PhysicalHelmholtz.norm_zero_numeric line 384
  41. lemma OAI.StrictHotSpots.PhysicalHelmholtz.self_zero line 389
  42. lemma OAI.StrictHotSpots.PhysicalHelmholtz.pair_sub line 398
  43. lemma OAI.StrictHotSpots.PhysicalHelmholtz.unique line 402
  44. lemma OAI.StrictHotSpots.Conformal.inner_H1grad_add_single line 435
  45. lemma OAI.StrictHotSpots.Conformal.affine_H10_grad_pair line 441
  46. lemma OAI.StrictHotSpots.Conformal.affine_H10_mass_pair line 455
  47. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_mixed_grad line 471
  48. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_mixed_mass line 487
  49. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pair_forward line 515
  50. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_transported_weak line 520
  51. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_weak line 532
  52. lemma OAI.StrictHotSpots.H1.tendsto_of_components line 557
  53. lemma OAI.StrictHotSpots.smoothMul_tendsto_lipschitzMul line 564
  54. theorem OAI.StrictHotSpots.Hodge.boundaryDefect_lipschitz_multiplier line 621
  55. lemma OAI.StrictHotSpots.Hodge.vectorValue_lipschitzMul_ae line 647
  56. lemma OAI.StrictHotSpots.Hodge.divergenceL_lipschitzMul_ae line 658
  57. lemma OAI.StrictHotSpots.Hodge.normal_pair_lipschitzMul line 671
  58. theorem OAI.StrictHotSpots.Hodge.TangentWeak.lipschitzMul line 686
  59. theorem OAI.StrictHotSpots.Hodge.boundaryClass_lipschitz_multiplier_identity line 693
  60. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_weak line 732
  61. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.class_difference line 738
  62. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_eq_extension line 748
  63. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_eq_extension line 758
  64. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitzMultipliedGradient line 771
  65. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_tendsto line 776
  66. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitzMultipliedGradient_class line 789
  67. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitzMultipliedGradient_tangent line 795
  68. lemma OAI.StrictHotSpots.Hodge.vectorForm_tendsto line 805
  69. lemma OAI.StrictHotSpots.PlaneGreen.harmonic_square_bound line 828
  70. lemma OAI.StrictHotSpots.PlaneGreen.multiplier_integrand_bound line 833
  71. theorem OAI.StrictHotSpots.PlaneGreen.multiplier_kernel_tendsto line 854
  72. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_form line 893
  73. lemma OAI.StrictHotSpots.Hodge.cartesianForm_eq_sum line 915
  74. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multipliedGradient_coordinate_difference line 934
  75. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.datum_multiplier_integrable line 966
  76. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.smooth_multiplier_kernel line 987
  77. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.smooth_multiplier_kernel_nonneg line 1033
  78. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.closedGradient_trace_continuous line 1063
  79. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physical_boundary_lipschitz line 1070
  80. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.smooth_physical_boundary_bound line 1076
  81. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physical_multiplier_integral_tendsto line 1084
  82. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitz_multiplier_kernel line 1108
  83. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.lipschitzMultipliedGradient_nonneg line 1133
  84. lemma OAI.StrictHotSpots.HilbertMultipliers.orthonormal_countable line 1151
  85. lemma OAI.StrictHotSpots.HilbertMultipliers.coordinate_hasSum line 1170
  86. theorem OAI.StrictHotSpots.HilbertMultipliers.coordinate_energy_sum line 1178
  87. lemma OAI.StrictHotSpots.HilbertMultipliers.nonnegative_coordinate_energy_zero line 1228
  88. lemma OAI.StrictHotSpots.PlaneGreen.fullBoundaryN_nonneg line 1247
  89. lemma OAI.StrictHotSpots.PlaneGreen.boundary_pair_ne line 1252
  90. lemma OAI.StrictHotSpots.PlaneGreen.full_embedding_identity line 1257
  91. theorem OAI.StrictHotSpots.PlaneGreen.full_embedding_coordinate_sum line 1268
  92. lemma OAI.StrictHotSpots.PlaneGreen.boundary_K_vector_integrable line 1317
  93. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.boundary_gradient_integral_zero line 1332