OAI/Geometry/Convex/GeneralMahler/NtLayer.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Nonthreshold kernel and integration over the ordered halves. We use (l,z) as pair of variables and ordinary product volume.

  1. abbrev OAI.GeneralMahler.Plane line 11
  2. def OAI.GeneralMahler.Edge.NTm line 16
  3. def OAI.GeneralMahler.Edge.nt0 line 18
  4. lemma OAI.GeneralMahler.Edge.nt_sym line 19
  5. lemma OAI.GeneralMahler.Edge.nt_pos line 20
  6. lemma OAI.GeneralMahler.Edge.nt_meas line 23
  7. lemma OAI.GeneralMahler.Edge.nt_mixed line 29
  8. lemma OAI.GeneralMahler.Edge.n0_meas line 49
  9. lemma OAI.GeneralMahler.Edge.n0_mixed line 50
  10. lemma OAI.GeneralMahler.Edge.n0_i line 58
  11. lemma OAI.GeneralMahler.Edge.n0_int line 61
  12. lemma OAI.GeneralMahler.Edge.nt_ref line 65

    Source comment

    reflection swap on ordered band
    lemma nt_ref (u x) : e.ref.nt0 (-u.swap) x=e.nt0 u x := by
…
  13. def OAI.GeneralMahler.Edge.BandS line 70
  14. lemma OAI.GeneralMahler.Edge.meas_BS line 71
  15. lemma OAI.GeneralMahler.Edge.band_area line 78
  16. def OAI.GeneralMahler.Edge.rs line 110

    Source comment

    measure transformations preserving volume
    def rs (u:Plane) := -u.swap

    Mentions: OAI.GeneralMahler.Plane

  17. lemma OAI.GeneralMahler.Edge.rs_int line 111
  18. lemma OAI.GeneralMahler.Edge.total_surplus line 116