OAI/Analysis/NumericalRange/PoissonBoundary.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.poissonExtension line 13
  2. lemma OAI.CompleteCrouzeix.continuousOn_unit_poisson line 16
  3. lemma OAI.CompleteCrouzeix.unit_poisson_nonneg line 23
  4. lemma OAI.CompleteCrouzeix.unit_poisson_normalized line 30
  5. lemma OAI.CompleteCrouzeix.poissonExtension_error_bound line 44
  6. theorem OAI.CompleteCrouzeix.poissonExtension_tendsto_boundary line 112
  7. theorem OAI.CompleteCrouzeix.harmonicOnNhd_poissonExtension line 142
  8. def OAI.CompleteCrouzeix.diskDirichlet line 161
  9. lemma OAI.CompleteCrouzeix.diskDirichlet_eq_boundary line 164
  10. theorem OAI.CompleteCrouzeix.harmonicOnNhd_diskDirichlet line 169
  11. theorem OAI.CompleteCrouzeix.continuousOn_diskDirichlet line 178
  12. lemma OAI.CompleteCrouzeix.harmonic_eventually_eq_of_isLocalMax line 211
  13. lemma OAI.CompleteCrouzeix.harmonic_eqOn_of_isPreconnected_of_isMaxOn line 230
  14. theorem OAI.CompleteCrouzeix.harmonic_exists_mem_frontier_isMaxOn line 253
  15. theorem OAI.CompleteCrouzeix.harmonic_le_of_frontier_le line 280
  16. theorem OAI.CompleteCrouzeix.harmonic_eqOn_closure_of_eqOn_frontier line 291
  17. lemma OAI.CompleteCrouzeix.circleAverage_conj line 309
  18. lemma OAI.CompleteCrouzeix.unit_poisson_conj line 317
  19. lemma OAI.CompleteCrouzeix.poissonExtension_odd line 321
  20. lemma OAI.CompleteCrouzeix.diskDirichlet_zero_real line 335
  21. def OAI.CompleteCrouzeix.upperDisk line 344
  22. def OAI.CompleteCrouzeix.upperClosedDisk line 345
  23. lemma OAI.CompleteCrouzeix.upperDisk_isOpen line 347
  24. lemma OAI.CompleteCrouzeix.closure_upperDisk_subset line 350
  25. lemma OAI.CompleteCrouzeix.upper_frontier_or line 356
  26. def OAI.CompleteCrouzeix.oddBoundary line 368
  27. lemma OAI.CompleteCrouzeix.oddBoundary_odd line 371
  28. lemma OAI.CompleteCrouzeix.continuousOn_oddBoundary line 386
  29. theorem OAI.CompleteCrouzeix.harmonic_reflection_upperDisk line 421