OAI/Geometry/Convex/GeneralMahler/Orthant.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Full-dimensional simplicial cones, coordinates and Laplace integrals.

  1. def OAI.GeneralMahler.orthant line 16
  2. theorem OAI.GeneralMahler.mem_orthant line 32
  3. theorem OAI.GeneralMahler.basis_mem_orthant line 35
  4. lemma OAI.GeneralMahler.mem_interior_orthant line 41
  5. def OAI.GeneralMahler.rebase line 66

    Source documentation

    Simplifying two bases via coefficient equivalence.

    def rebase (a : Basis (Fin m) ℝ E) : E ≃ₗ[ℝ] E :=
…
  6. lemma OAI.GeneralMahler.pushCone_rebase line 69
  7. lemma OAI.GeneralMahler.rebase_apply_basis line 78
  8. def OAI.GeneralMahler.IsLinearOrthant line 87

    Source documentation

    Exact cone equality class in the proof: image of a coordinate orthant by an invertible linear map. Basis vectors serve as generating rays.

    def IsLinearOrthant (m : ℕ) (C : ProperCone ℝ E) :=
…
  9. lemma OAI.GeneralMahler.eq_basis_ip line 96
  10. lemma OAI.GeneralMahler.ip_onb line 101
  11. lemma OAI.GeneralMahler.orthant_self_dual line 108
  12. theorem OAI.GeneralMahler.chi_orthant line 122