OAI/Geometry/Convex/GeneralMahler/Parameter.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Coordinate and covariance parameters in compact boxes.

  1. def OAI.GeneralMahler.tmin line 14

    Source comment

    Exact finite decimals of the paper as rationals cast to ℝ
    def tmin : ℝ := -22/1000
  2. def OAI.GeneralMahler.tmax line 15
  3. lemma OAI.GeneralMahler.add_cov_box line 18

    Source comment

    Use S bounded coarsely between I/2 and 2I; precise equation maintained.
    lemma add_cov_box {T : Mat m} (ht : T∈specBox m tmin tmax) :
    1+T∈specBox m (1/4:ℝ) 4 := by
…

    Mentions: OAI.GeneralMahler.Mat, OAI.GeneralMahler.specBox, OAI.GeneralMahler.tmin, OAI.GeneralMahler.tmax

  4. lemma OAI.GeneralMahler.scalar_mul line 30
  5. lemma OAI.GeneralMahler.scalar_psd line 33
  6. lemma OAI.GeneralMahler.root_box line 36
  7. def OAI.GeneralMahler.equivPD line 47
  8. lemma OAI.GeneralMahler.equivPD_spec line 49
  9. lemma OAI.GeneralMahler.inv_norm_box line 52
  10. def OAI.GeneralMahler.params line 73
  11. abbrev OAI.GeneralMahler.Param line 76
  12. def OAI.GeneralMahler.Param.B line 81
  13. def OAI.GeneralMahler.Param.T line 82
  14. lemma OAI.GeneralMahler.Param.in_box line 83
  15. def OAI.GeneralMahler.Param.S line 86
  16. lemma OAI.GeneralMahler.Param.S_box line 87
  17. lemma OAI.GeneralMahler.Param.S_pos line 88
  18. def OAI.GeneralMahler.Param.transE line 90
  19. lemma OAI.GeneralMahler.Param.trans_apply line 93
  20. lemma OAI.GeneralMahler.Param.contra_eq line 97
  21. def OAI.GeneralMahler.Param.instanceQ line 111
  22. lemma OAI.GeneralMahler.Param.sigma_choice line 124
  23. lemma OAI.GeneralMahler.Param.Bound_instance line 129