OAI/Geometry/Convex/GeneralMahler/Transform.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Linear transformations in the paper's Cone reduction lemma.

  1. def OAI.GeneralMahler.pushCone line 13

    Source documentation

    Linear image, using the inverse so the cone is obviously closed.

    def pushCone (B : E ≃ₗ[ℝ] E) (C : ProperCone ℝ E) : ProperCone ℝ E :=
…
  2. lemma OAI.GeneralMahler.mem_pushCone line 16
  3. lemma OAI.GeneralMahler.pushCone_carrier line 19
  4. lemma OAI.GeneralMahler.apply_mem_interior_pushCone line 25
  5. def OAI.GeneralMahler.contra line 34

    Source documentation

    Inverse transpose in Euclidean metric.

    def contra (B : E ≃ₗ[ℝ] E) : E ≃ₗ[ℝ] E :=
…
  6. lemma OAI.GeneralMahler.pair_contra line 52
  7. lemma OAI.GeneralMahler.dual_pushCone line 58
  8. def OAI.GeneralMahler.jac line 72
  9. lemma OAI.GeneralMahler.jac_ne_zero line 75
  10. lemma OAI.GeneralMahler.jac_mul_contra line 79
  11. lemma OAI.GeneralMahler.chi_transform' line 91
  12. theorem OAI.GeneralMahler.chi_transform line 111