OAI/Geometry/Convex/GeneralMahler/Laplace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Geometric Mahler bounds from cone Laplace integrals and profile inequalities.

  1. structure OAI.GeneralMahler.Input091 line 12
  2. lemma OAI.GeneralMahler.orthant_pull line 19
  3. lemma OAI.GeneralMahler.ConeLap line 30
  4. lemma OAI.GeneralMahler.Body.CLift line 54

    Source comment

    transfer through an isometric identification with Rn(n+1)
    lemma CLift (h:Input091) (C:ProperCone ℝ (LiftSpace n)) (U V:LiftSpace n)
    (hU:U∈interior (C:Set (LiftSpace n))) (hV:V∈interior (posDual C:Set (LiftSpace n)))
    (he:⟪U,V⟫=((n+1:ℕ):ℝ)):
    1 ≤ chi C V*chi (posDual C) U ∧
      (chi C V*chi (posDual C) U=1 → IsLinearOrthant (n+1) C) := by
…

    Mentions: OAI.GeneralMahler.Input091, OAI.GeneralMahler.LiftSpace, OAI.GeneralMahler.posDual, OAI.GeneralMahler.chi, OAI.GeneralMahler.IsLinearOrthant

  5. lemma OAI.GeneralMahler.Body.bound_at line 100
  6. theorem OAI.GeneralMahler.Body.main_with_profiles line 121