OAI/Analysis/SymmetricDomains/BishopAnalyticDiscs.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.smooth_fixed_point_family_unique line 16
  2. lemma OAI.Release061.Wiener.normalizedHilbert_constant line 66
  3. lemma OAI.Release061.Wiener.realEvaluation_constant line 81
  4. def OAI.Release061.Wiener.realSchwarz line 86
  5. def OAI.Release061.Wiener.constantDisc line 89
  6. lemma OAI.Release061.Wiener.constantDisc_apply line 92
  7. lemma OAI.Release061.Wiener.realSchwarz_boundary line 95
  8. lemma OAI.Release061.Wiener.fourier_mem_closedDisc line 114
  9. lemma OAI.Release061.Wiener.schwarz_constant line 118
  10. def OAI.Release061.Wiener.bishopDisc line 130
  11. lemma OAI.Release061.Wiener.bishopDisc_smooth line 134
  12. lemma OAI.Release061.Wiener.bishopDisc_continuous_boundary line 142
  13. lemma OAI.Release061.Wiener.bishopDisc_analytic line 148
  14. lemma OAI.Release061.Wiener.bishopDisc_boundary line 157
  15. theorem OAI.Release061.Wiener.bishop_analytic_discs line 166