OAI/Geometry/Convex/GeneralMahler/ScatterField.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Two projection maps implementing Scatter.

  1. lemma OAI.GeneralMahler.ProjField.s_poly line 13
  2. lemma OAI.GeneralMahler.ProjField.loc_ends line 18
  3. lemma OAI.GeneralMahler.ProjField.xt_d line 34
  4. lemma OAI.GeneralMahler.ProjField.S_inj line 61
  5. def OAI.GeneralMahler.ProjField.primalMap line 62
  6. def OAI.GeneralMahler.ProjField.dualMap line 79
  7. lemma OAI.GeneralMahler.ProjField.X_sc line 127
  8. lemma OAI.GeneralMahler.ProjField.Y_sc line 130