OAI/Analysis/DirectCrouzeix/PoissonBoundary.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectCrouzeix.Conformal.poissonExtension line 31
  2. theorem OAI.DirectCrouzeix.Conformal.poisson_continuous_circle line 34
  3. theorem OAI.DirectCrouzeix.Conformal.poisson_nonnegative_circle line 41
  4. theorem OAI.DirectCrouzeix.Conformal.poisson_average_one line 50
  5. theorem OAI.DirectCrouzeix.Conformal.poisson_boundary_limit line 55
  6. theorem OAI.DirectCrouzeix.Conformal.harmonic_eventually_eq_of_isLocalMax line 151
  7. theorem OAI.DirectCrouzeix.Conformal.harmonic_le_boundary line 167
  8. def OAI.DirectCrouzeix.Conformal.herglotzExtension line 199
  9. theorem OAI.DirectCrouzeix.Conformal.herglotz_analytic line 202
  10. theorem OAI.DirectCrouzeix.Conformal.herglotz_re line 209
  11. theorem OAI.DirectCrouzeix.Conformal.poisson_harmonic line 224