OAI/Analysis/HotSpots/Poisson.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.Douglas.planeSeries_boundary line 16
  2. theorem OAI.StrictHotSpots.Douglas.harmonicSeries_boundary_class line 24
  3. theorem OAI.StrictHotSpots.Douglas.C3_boundary_class line 72
  4. def OAI.StrictHotSpots.SubcriticalExtension.observe line 96
  5. def OAI.StrictHotSpots.SubcriticalExtension.solve line 99
  6. lemma OAI.StrictHotSpots.SubcriticalExtension.solve_spec line 103
  7. lemma OAI.StrictHotSpots.SubcriticalExtension.observe_coe line 109
  8. lemma OAI.StrictHotSpots.SubcriticalExtension.observe_solve line 110
  9. lemma OAI.StrictHotSpots.SubcriticalExtension.grad_add_coe line 113
  10. lemma OAI.StrictHotSpots.SubcriticalExtension.observe_add_coe line 115
  11. def OAI.StrictHotSpots.SubcriticalExtension.extension line 120
  12. def OAI.StrictHotSpots.SubcriticalExtension.Harmonic line 123
  13. lemma OAI.StrictHotSpots.SubcriticalExtension.extension_observe line 126
  14. lemma OAI.StrictHotSpots.SubcriticalExtension.extension_grad line 139
  15. lemma OAI.StrictHotSpots.SubcriticalExtension.extension_weak line 145
  16. def OAI.StrictHotSpots.SubcriticalExtension.harmonicLift line 181
  17. lemma OAI.StrictHotSpots.SubcriticalExtension.harmonicLift_difference line 185
  18. lemma OAI.StrictHotSpots.SubcriticalExtension.harmonicLift_harmonic line 193
  19. lemma OAI.StrictHotSpots.SubcriticalExtension.h10_eq_zero_of_grad_norm_sq line 211
  20. lemma OAI.StrictHotSpots.SubcriticalExtension.harmonic_zero_class line 223
  21. lemma OAI.StrictHotSpots.SubcriticalExtension.harmonic_sub line 230
  22. lemma OAI.StrictHotSpots.SubcriticalExtension.harmonicLift_unique line 241
  23. lemma OAI.StrictHotSpots.PlaneGreen.poissonAverage_harmonic line 261
  24. lemma OAI.StrictHotSpots.PlaneGreen.harmonicAt_comp_linearIsometryEquiv line 282
  25. lemma OAI.StrictHotSpots.Douglas.harmonicSeries_re_harmonic line 300
  26. lemma OAI.StrictHotSpots.Douglas.planeSeries_harmonic line 311
  27. lemma OAI.StrictHotSpots.Douglas.planeSeries_weak_harmonic line 318
  28. theorem OAI.StrictHotSpots.Douglas.harmonicSeries_eq_harmonicLift line 332
  29. lemma OAI.StrictHotSpots.Douglas.chord_translate line 353
  30. def OAI.StrictHotSpots.Douglas.angleSmooth line 359
  31. lemma OAI.StrictHotSpots.Douglas.angleSmooth_smooth line 362
  32. lemma OAI.StrictHotSpots.Douglas.angleSmooth_periodic line 367
  33. lemma OAI.StrictHotSpots.Douglas.angleSmooth_integrable line 376
  34. lemma OAI.StrictHotSpots.Douglas.angleSmooth_chordLipschitz line 382
  35. lemma OAI.StrictHotSpots.Douglas.periodic_lift_continuous line 405
  36. def OAI.StrictHotSpots.Douglas.circleSmooth line 411
  37. lemma OAI.StrictHotSpots.Douglas.circleSmooth_coe line 415
  38. lemma OAI.StrictHotSpots.Douglas.circleSmooth_chordLipschitz line 418
  39. lemma OAI.StrictHotSpots.Douglas.circleSmooth_tendsto line 425
  40. lemma OAI.StrictHotSpots.Douglas.periodic_deriv line 442
  41. lemma OAI.StrictHotSpots.Douglas.angleLift_periodic line 447
  42. theorem OAI.StrictHotSpots.Douglas.summable_firstMoment_of_smooth_lift line 454
  43. lemma OAI.StrictHotSpots.Douglas.circleSmooth_firstMoment line 476
  44. theorem OAI.StrictHotSpots.Douglas.douglas_smooth_lift line 481
  45. theorem OAI.StrictHotSpots.Douglas.smooth_poisson_energy_tendsto line 502
  46. lemma OAI.StrictHotSpots.Douglas.chordLipschitz_sub line 525
  47. lemma OAI.StrictHotSpots.Douglas.boundaryEnergy_zero line 532
  48. theorem OAI.StrictHotSpots.Douglas.circleSmooth_boundaryError_tendsto line 538
  49. theorem OAI.StrictHotSpots.Douglas.circleSmooth_poisson_cauchy line 554
  50. lemma OAI.StrictHotSpots.Douglas.angleSmooth_norm_le line 585
  51. lemma OAI.StrictHotSpots.Douglas.circleSmooth_norm_le line 598
  52. theorem OAI.StrictHotSpots.Douglas.circleSmooth_poisson_tendsto line 604
  53. lemma OAI.StrictHotSpots.Douglas.real_component_gradient_bound line 636
  54. theorem OAI.StrictHotSpots.Douglas.planeSeries_energy_le line 662