OAI/Geometry/Convex/GeneralMahler/Santalo.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Santaló center

Rather than the spherical integral, we use equivalently the cone Laplace integral and its divergence at the dual boundary. This way of proving the center claims includes dimension 1 without a separate case.

  1. def OAI.GeneralMahler.Body.polarVol line 19
  2. lemma OAI.GeneralMahler.Body.chi_pair_one line 21
  3. lemma OAI.GeneralMahler.Body.mem_int' line 32
  4. lemma OAI.GeneralMahler.Body.polarVol_strict line 39
  5. theorem OAI.GeneralMahler.Body.santalo_exists line 61

    Source documentation

    Existence and uniqueness of the polar-volume minimizer.

    theorem santalo_exists (K : Body n) :
    ∃! x, x ∈ interior (K : Set (Rn n)) ∧ IsMinOn K.polarVol (interior (K:Set (Rn n))) x := by
…

    Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.Rn

  6. def OAI.GeneralMahler.Body.santalo line 96
  7. theorem OAI.GeneralMahler.Body.santalo_spec line 98
  8. def OAI.GeneralMahler.Body.productAt line 103
  9. def OAI.GeneralMahler.Body.P line 104
  10. theorem OAI.GeneralMahler.Body.product_min line 106
  11. theorem OAI.GeneralMahler.Body.product_inf line 110