OAI/Analysis/Crouzeix/PhysicalDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Physical Density.

  1. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.operatorDensity line 29
  2. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.operatorDensity_nonneg line 33
  3. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.integral_operatorDensity line 42
  4. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.integral_operatorDensity_pullback line 49
  5. def OAI.CrouzeixHilbert.operatorToMatrix line 65
  6. lemma OAI.CrouzeixHilbert.operatorToMatrix_apply line 68
  7. def OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixDensity line 75
  8. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.matrixDensity_posSemidef line 80
  9. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.integral_matrixDensity line 87
  10. lemma OAI.CrouzeixHilbert.Conformal.ExteriorCollar.tensorIntegral_matrixDensity_pullback line 99