OAI/Analysis/Crouzeix/Faber.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Faber.

  1. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.twice_coordinate_mem line 21
  2. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.outerMap line 25
  3. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.outerDomain line 30
  4. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.isOpen_outerDomain line 32
  5. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.closure_subset_outerDomain line 35
  6. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.outer_difference_ne_zero line 42
  7. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient line 47
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_physicalCoefficient line 52
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient_inside line 70
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient_inside_neg line 93
  11. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient_inside_zero line 101
  12. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionMoment line 108
  13. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.continuousOn_correctionMoment_integrand line 111
  14. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_correctionMoment_integrand line 126
  15. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.differentiableOn_correctionMoment line 131
  16. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionMoment_zero line 138
  17. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionMoment_zero_index line 141
  18. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient_closed_neg line 148
  19. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient_closed_zero line 155
  20. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.correctionMoment_outer line 162
  21. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.circle_model_moment line 179
  22. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physicalCoefficient_boundary line 195