OAI/Analysis/SymmetricDomains/BishopBoundarySolution.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.smooth_fixed_point_family line 17
  2. lemma OAI.Release061.Wiener.realEvaluation_ext line 61
  3. lemma OAI.Release061.Wiener.eval_zero_input line 70
  4. lemma OAI.Release061.Wiener.cons_zero_norm line 76
  5. lemma OAI.Release061.Wiener.exists_boundary_lift line 88
  6. abbrev OAI.Release061.Wiener.BishopParams line 117
  7. abbrev OAI.Release061.Wiener.BoundarySpace line 118
  8. def OAI.Release061.Wiener.bishopInput line 120
  9. lemma OAI.Release061.Wiener.bishopInput_apply line 136
  10. def OAI.Release061.Wiener.bishopRHS line 141
  11. lemma OAI.Release061.Wiener.bishopRHS_smooth line 146
  12. lemma OAI.Release061.Wiener.bishopRHS_zero_unknown line 164
  13. theorem OAI.Release061.Wiener.bishop_boundary_solution line 172