OAI/Analysis/Crouzeix/PhysicalCalculus.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Physical Calculus.

  1. def OAI.CrouzeixHilbert.Conformal.InteriorCollar.pullbackDomain line 23
  2. lemma OAI.CrouzeixHilbert.Conformal.InteriorCollar.isOpen_pullbackDomain line 25
  3. lemma OAI.CrouzeixHilbert.Conformal.InteriorCollar.closedDisk_subset_pullbackDomain line 28
  4. lemma OAI.CrouzeixHilbert.Conformal.InteriorCollar.differentiableOn_pullback line 32
  5. def OAI.CrouzeixHilbert.Conformal.InteriorCollar.diskTrace line 36
  6. lemma OAI.CrouzeixHilbert.Conformal.InteriorCollar.holomorphic_intertwines line 46
  7. lemma OAI.CrouzeixHilbert.Conformal.InteriorCollar.matrixHolomorphic_intertwines line 80
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.h_interiorAngle line 104
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.integral_operatorDensity_holomorphic line 113
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.physical_intertwines line 131