OAI/Geometry/Convex/GeneralMahler/Contact.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Layer covariances and scalar contact term.

  1. def OAI.GeneralMahler.ProjField.Lr line 15
  2. def OAI.GeneralMahler.ProjField.ct line 25
  3. def OAI.GeneralMahler.ProjField.Ct line 26
  4. lemma OAI.GeneralMahler.ProjField.ct_pos line 27
  5. def OAI.GeneralMahler.ProjField.ipt line 34

    Source comment

    local notation centered pairing with normalized inner product
    def ipt (f g:Rn m→Rn m) := (∫ x,⟪f x,g x⟫ ∂normal m)/(m:ℝ)

    Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.normal

  6. lemma OAI.GeneralMahler.ProjField.ipt_i line 35
  7. lemma OAI.GeneralMahler.ProjField.ipt_sym line 39
  8. lemma OAI.GeneralMahler.ProjField.regneg line 42
  9. lemma OAI.GeneralMahler.ProjField.regsub line 44
  10. lemma OAI.GeneralMahler.ProjField.regconst line 46
  11. lemma OAI.GeneralMahler.ProjField.ipt_add line 48
  12. lemma OAI.GeneralMahler.ProjField.ipt_sub line 52
  13. lemma OAI.GeneralMahler.ProjField.ipt_smul line 56
  14. lemma OAI.GeneralMahler.ProjField.ipt_const line 59
  15. lemma OAI.GeneralMahler.ProjField.Z_reg line 65
  16. lemma OAI.GeneralMahler.ProjField.Z_mean line 67
  17. lemma OAI.GeneralMahler.ProjField.X_reg line 70
  18. lemma OAI.GeneralMahler.ProjField.Y_reg line 72
  19. lemma OAI.GeneralMahler.ProjField.zz_cov line 77
  20. def OAI.GeneralMahler.ProjField.Xcenter line 107
  21. lemma OAI.GeneralMahler.ProjField.Xc_reg line 108
  22. lemma OAI.GeneralMahler.ProjField.Xc_mean line 110
  23. lemma OAI.GeneralMahler.ProjField.xz_cov line 112
  24. lemma OAI.GeneralMahler.ProjField.xx_cov line 117
  25. lemma OAI.GeneralMahler.ProjField.Zs_reg line 128
  26. lemma OAI.GeneralMahler.ProjField.ww_cov0 line 130
  27. lemma OAI.GeneralMahler.ProjField.WW_pair_cov line 144