Polar.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Polar bodies, translations, and slices.

def OAI.GeneralMahler.polarAt line 12
Source documentation
(K-z)^o from the manuscript.
Distinct definitions of this name: ComparatorChallenges/GeneralMahler.lean:15 (different declaration text). Qualify references as OAI.GeneralMahler.polarAt@path.
```
def polarAt (K : Set (Rn n)) (z : Rn n) : Set (Rn n) :=
…
```
Mentions: OAI.GeneralMahler.Rn
def OAI.GeneralMahler.Body.off line 18
Source documentation
K translated by -z.
```
def off (K : Body n) (z : Rn n) : Body n where
…
```
Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.Rn
theorem OAI.GeneralMahler.Body.mem_off line 39
theorem OAI.GeneralMahler.Body.off_interior line 42
theorem OAI.GeneralMahler.Body.polar_off line 49
lemma OAI.GeneralMahler.Body.dual_height line 61
Source documentation
Uniform lower bound for height in the dual cone to K with 0 interior.
```
lemma dual_height {K : Body n} (hk : 0 ∈ interior (K:Set (Rn n))) :
    ∃ c > 0, ∀ p ∈ posDual K.cone, c * ‖p‖ ≤ hgt p := by
…
```
Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.Rn, OAI.GeneralMahler.posDual, OAI.GeneralMahler.hgt
lemma OAI.GeneralMahler.Body.dual_head line 75
def OAI.GeneralMahler.Body.polarSlice line 95
Source documentation
Slice t=1 of the dual, a reflected polar.
```
def polarSlice (K : Body n) (hk : 0 ∈ interior (K:Set (Rn n))) : Body n where
…
```
Mentions: OAI.GeneralMahler.Body, OAI.GeneralMahler.Rn
theorem OAI.GeneralMahler.Body.cone_polarSlice line 126
theorem OAI.GeneralMahler.Body.polarSlice_volume line 154