OAI/Geometry/Convex/GeneralMahler/Scatter.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The cone-valued maps in the entropy bound. Use cutoffs proven earlier to get pointwise spatially local Lipschitz control; this allows applying the injective-area formula directly on a conull set.

  1. structure OAI.GeneralMahler.Scatter line 15
  2. def OAI.GeneralMahler.Scatter.y line 31
  3. lemma OAI.GeneralMahler.Scatter.yc line 32
  4. lemma OAI.GeneralMahler.Scatter.yp line 35
  5. lemma OAI.GeneralMahler.Scatter.yl line 39
  6. lemma OAI.GeneralMahler.Scatter.zero_y line 43
  7. lemma OAI.GeneralMahler.Scatter.linear_y line 45
  8. def OAI.GeneralMahler.Scatter.ky line 48
  9. lemma OAI.GeneralMahler.Scatter.kc line 49
  10. lemma OAI.GeneralMahler.Scatter.km line 51
  11. lemma OAI.GeneralMahler.Scatter.ki line 70
  12. lemma OAI.GeneralMahler.Scatter.Ki line 72
  13. lemma OAI.GeneralMahler.Scatter.klip line 74
  14. def OAI.GeneralMahler.Scatter.t line 99
  15. lemma OAI.GeneralMahler.Scatter.tsm line 100
  16. lemma OAI.GeneralMahler.Scatter.tp line 101
  17. lemma OAI.GeneralMahler.Scatter.ti line 102
  18. lemma OAI.GeneralMahler.Scatter.t_in line 104
  19. lemma OAI.GeneralMahler.Scatter.t_injective line 118
  20. def OAI.GeneralMahler.Scatter.TJ line 147
  21. lemma OAI.GeneralMahler.Scatter.td line 148