OAI/Geometry/Convex/GeneralMahler/Eq13.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Eq13 covariance equals Q+Ct on centered tests.

  1. lemma OAI.GeneralMahler.ProjField.mixed_contract line 15
  2. lemma OAI.GeneralMahler.ProjField.ipt_double line 34
  3. lemma OAI.GeneralMahler.ProjField.Ct_integrable line 67
  4. lemma OAI.GeneralMahler.ProjField.eq13 line 82