OAI/Analysis/HotSpots/ClosedSolution.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.complex_maps_disk line 14
  2. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.complex_maps_closed line 19
  3. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.complex_maps_boundary line 24
  4. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.complex_inverse_disk line 29
  5. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.complex_inverse_boundary line 35
  6. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.complex_inverse_image line 40
  7. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.connected_complex_pull line 54
  8. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.circleBoundaryHomeomorph line 69
  9. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.boundary_scalar_extension line 110
  10. lemma OAI.StrictHotSpots.HilbertMultipliers.coordinate_lipschitz line 127
  11. lemma OAI.StrictHotSpots.PlaneGreen.norm_le_of_mem_closure_disk line 149
  12. lemma OAI.StrictHotSpots.PlaneGreen.mem_disk_of_norm_lt line 153
  13. lemma OAI.StrictHotSpots.PlaneGreen.kernel_zero_left line 156
  14. lemma OAI.StrictHotSpots.PlaneGreen.kernel_continuousAt_left_closed line 159
  15. lemma OAI.StrictHotSpots.PlaneGreen.kernel_memLp_closed line 174
  16. lemma OAI.StrictHotSpots.PlaneGreen.kernel_uniform_three_bound_closed line 183
  17. def OAI.StrictHotSpots.PlaneGreen.closedRow line 195
  18. lemma OAI.StrictHotSpots.PlaneGreen.closedRow_coe_ae line 198
  19. lemma OAI.StrictHotSpots.PlaneGreen.closedRow_continuous line 203
  20. lemma OAI.StrictHotSpots.PlaneGreen.green_integral_eq_closedInner line 224
  21. lemma OAI.StrictHotSpots.PlaneGreen.green_integral_continuousOn_closure line 231
  22. lemma OAI.StrictHotSpots.PlaneGreen.green_integral_boundary line 238
  23. def OAI.StrictHotSpots.PlaneGreen.boundaryClosedPoisson line 259
  24. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedPoisson_interior line 262
  25. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedPoisson_trace line 267
  26. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedPoisson_continuousOn line 273
  27. def OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution line 283
  28. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_interior line 289
  29. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_continuousOn line 296
  30. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_trace line 302
  31. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_value_ae line 309
  32. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_hasH1Gradient line 317
  33. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_K line 325
  34. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.inverse_map_chartMeasure line 345
  35. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pull_ae_to_physical line 358
  36. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_pull_ae line 370
  37. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physicalSolution_closed_ae line 389
  38. lemma OAI.StrictHotSpots.PlaneGreen.boundaryClosedSolution_tendsto line 420
  39. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_closed_ae line 456
  40. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.scalarSolution_mul_tendsto line 465
  41. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.multiplierTrace line 486
  42. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.multiplierTrace_lipschitz line 492
  43. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.physical_lipschitzMul_closed_ae line 498