OAI/Analysis/HotSpots/Conformal.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StrictHotSpots.Conformal.CoordinatePlane line 13
  2. def OAI.StrictHotSpots.Conformal.coordinate line 14
  3. def OAI.StrictHotSpots.Conformal.planeMul line 16
  4. lemma OAI.StrictHotSpots.Conformal.planeMul_apply line 21
  5. lemma OAI.StrictHotSpots.Conformal.planeMul_det line 25
  6. lemma OAI.StrictHotSpots.Conformal.plane_gradient_comp line 39
  7. lemma OAI.StrictHotSpots.Conformal.plane_norm_gradient_comp line 56
  8. lemma OAI.StrictHotSpots.Conformal.plane_integral_target line 63
  9. lemma OAI.StrictHotSpots.Conformal.plane_dirichlet_energy line 70
  10. def OAI.StrictHotSpots.Conformal.planeChart line 84
  11. lemma OAI.StrictHotSpots.Conformal.planeChart_source line 89
  12. lemma OAI.StrictHotSpots.Conformal.planeChart_target line 94
  13. lemma OAI.StrictHotSpots.Conformal.planeChart_apply line 99
  14. lemma OAI.StrictHotSpots.Conformal.planeChart_hasFDerivAt line 102
  15. def OAI.CompactChart.transport line 126
  16. lemma OAI.CompactChart.transport_apply line 128
  17. lemma OAI.CompactChart.transport_source line 131
  18. lemma OAI.CompactChart.support_transport_subset line 135
  19. lemma OAI.CompactChart.compact_image_tsupport line 143
  20. lemma OAI.CompactChart.tsupport_transport_subset line 147
  21. lemma OAI.CompactChart.hasCompactSupport_transport line 151
  22. lemma OAI.CompactChart.transport_support_target line 156
  23. lemma OAI.CompactChart.transport_eventuallyEq line 162
  24. lemma OAI.CompactChart.contDiff_transport line 167
  25. lemma OAI.CompactChart.transport_add line 178
  26. lemma OAI.CompactChart.transport_smul line 183
  27. lemma OAI.CompactChart.transport_comp_eventuallyEq line 188
  28. lemma OAI.CompactChart.transport_symm_transport line 193
  29. def OAI.StrictHotSpots.Conformal.transportTest line 216
  30. lemma OAI.StrictHotSpots.Conformal.test_grad_sq line 224
  31. lemma OAI.StrictHotSpots.Conformal.test_value_sq line 231
  32. lemma OAI.StrictHotSpots.Conformal.transportTest_grad_sq line 238
  33. lemma OAI.StrictHotSpots.Conformal.transportTest_value_sq line 252
  34. lemma OAI.StrictHotSpots.Conformal.scalar_norm_bound line 262
  35. lemma OAI.StrictHotSpots.Conformal.transportTest_bound line 274
  36. def OAI.StrictHotSpots.Conformal.transportH10 line 317
  37. lemma OAI.StrictHotSpots.Conformal.transportH10_test line 321
  38. lemma OAI.StrictHotSpots.Conformal.transportH10_grad_sq line 329
  39. lemma OAI.StrictHotSpots.Conformal.transportH10_inner_grad line 345
  40. lemma OAI.StrictHotSpots.Conformal.transportTest_symm line 357
  41. lemma OAI.StrictHotSpots.Conformal.transportH10_symm line 363
  42. lemma OAI.StrictHotSpots.Conformal.transported_dirichlet line 382
  43. lemma OAI.StrictHotSpots.Conformal.transported_subcritical line 393
  44. def OAI.StrictHotSpots.Conformal.chartMeasure line 420
  45. lemma OAI.StrictHotSpots.Conformal.chartMeasure_ac line 423
  46. lemma OAI.StrictHotSpots.Conformal.chart_aemeasurable line 426
  47. lemma OAI.StrictHotSpots.Conformal.map_chartMeasure line 429
  48. def OAI.StrictHotSpots.Conformal.measurableChart line 439
  49. lemma OAI.StrictHotSpots.Conformal.measurableChart_ae line 442
  50. lemma OAI.StrictHotSpots.Conformal.measurableChart_preserving line 445
  51. def OAI.StrictHotSpots.Conformal.chartPull line 451
  52. lemma OAI.StrictHotSpots.Conformal.chartPull_ae line 455
  53. lemma OAI.StrictHotSpots.Conformal.chartPull_test_ae line 461
  54. lemma OAI.StrictHotSpots.Conformal.ae_chart_source line 471
  55. lemma OAI.LpDensityClosure.ae_eq_of_tendsto line 492
  56. lemma OAI.LpDensityClosure.isClosed_graph line 504
  57. lemma OAI.LpDensityClosure.ae_eq_of_dense line 511
  58. def OAI.StrictHotSpots.Conformal.weightedValue line 541
  59. lemma OAI.StrictHotSpots.Conformal.weightedValue_test line 545
  60. lemma OAI.StrictHotSpots.Conformal.weightedValue_ae line 564
  61. lemma OAI.StrictHotSpots.Conformal.weightedValue_norm line 577
  62. lemma OAI.StrictHotSpots.Conformal.value_memLp_chartMeasure line 583
  63. lemma OAI.StrictHotSpots.Conformal.physical_value_sq line 589
  64. theorem OAI.StrictHotSpots.Conformal.weighted_subcritical line 603