OAI/Analysis/HotSpots/GreenSolution.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.L2Limits.unifIntegrable_two_of_three line 15
  2. lemma OAI.StrictHotSpots.PlaneGreen.kernel_plane_formula line 55
  3. lemma OAI.StrictHotSpots.PlaneGreen.kernel_continuousAt_left line 59
  4. lemma OAI.StrictHotSpots.PlaneGreen.row_eq_toLp line 73
  5. theorem OAI.StrictHotSpots.PlaneGreen.row_continuous line 82
  6. lemma OAI.StrictHotSpots.PlaneGreen.green_integral_eq_inner line 105
  7. lemma OAI.StrictHotSpots.PlaneGreen.green_integral_continuous line 111
  8. lemma OAI.StrictHotSpots.PlaneGreen.angleBoundary_coe line 130
  9. lemma OAI.StrictHotSpots.PlaneGreen.angleBoundary_dist line 140
  10. def OAI.StrictHotSpots.PlaneGreen.boundaryAngleData line 147
  11. lemma OAI.StrictHotSpots.PlaneGreen.boundaryAngleData_apply line 151
  12. lemma OAI.StrictHotSpots.PlaneGreen.boundaryAngleData_lipschitz line 154
  13. lemma OAI.StrictHotSpots.PlaneGreen.integral_boundary_angle line 160
  14. lemma OAI.StrictHotSpots.PlaneGreen.poissonExtension_eq_planePoisson line 167
  15. def OAI.StrictHotSpots.PlaneGreen.boundaryPoissonH1 line 189
  16. lemma OAI.StrictHotSpots.PlaneGreen.boundaryPoissonH1_harmonic line 193
  17. lemma OAI.StrictHotSpots.PlaneGreen.boundaryPoissonH1_value_ae line 198
  18. lemma OAI.StrictHotSpots.PlaneGreen.boundaryPoissonH1_observe line 210
  19. lemma OAI.StrictHotSpots.PlaneGreen.integral_boundary_prod_angle line 234
  20. lemma OAI.StrictHotSpots.PlaneGreen.real_complex_inner_quotient line 245
  21. lemma OAI.StrictHotSpots.PlaneGreen.boundaryRealCross_geometric line 252
  22. theorem OAI.StrictHotSpots.PlaneGreen.boundaryPoissonH1_energy line 268
  23. def OAI.StrictHotSpots.PlaneGreen.boundarySolution line 294
  24. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolution_weak line 298
  25. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolution_class line 306
  26. theorem OAI.StrictHotSpots.PlaneGreen.boundarySolution_energy line 313
  27. lemma OAI.StrictHotSpots.DirichletOperator.solution_comp line 353
  28. lemma OAI.StrictHotSpots.PlaneGreen.solve_value_eq_integralOperator line 365
  29. lemma OAI.StrictHotSpots.PlaneGreen.solve_value_ae line 376
  30. def OAI.StrictHotSpots.PlaneGreen.boundarySolutionValue line 386
  31. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolutionValue_eq_fullExtension line 392
  32. lemma OAI.StrictHotSpots.PlaneGreen.poissonExtension_continuousOn line 397
  33. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolutionValue_continuousOn line 403
  34. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolution_value_eq line 409
  35. lemma OAI.StrictHotSpots.PlaneGreen.value_add_ae line 429
  36. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolution_value_ae line 436
  37. theorem OAI.StrictHotSpots.PlaneGreen.boundarySolution_K line 447
  38. lemma OAI.StrictHotSpots.PlaneGreen.boundaryPoissonH1_real_class line 469
  39. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolution_eq_of_trace line 489
  40. lemma OAI.StrictHotSpots.PlaneGreen.boundarySolutionValue_eq_of_trace line 502
  41. theorem OAI.StrictHotSpots.PlaneGreen.value_K_of_trace line 518
  42. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.boundary_mem_closed line 544
  43. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.datumTrace line 548
  44. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.datumTrace_lipschitz line 553
  45. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_Poisson_class line 560
  46. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_comp_H1 line 569
  47. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.pullDatum_comp_toH1 line 580