OAI/Analysis/Mahler/ConvexPolarBody.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.convex_coordinatePolar line 10
2. lemma OAI.SymmetricMahler.symmetric_coordinatePolar line 23
3. theorem OAI.SymmetricMahler.zero_mem_interior_coordinatePolar line 32

   Source documentation

   A compact K gives an open l1 neighborhood of zero inside the literal polar.

   theorem zero_mem_interior_coordinatePolar [DecidableEq I] {K : Set (I → ℝ)} (hK : IsCompact K) :
       (0 : I → ℝ) ∈ interior (coordinatePolar K) := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar

4. theorem OAI.SymmetricMahler.coordinatePolar_is_symmetric_convex_body line 55

   Source documentation

   The polar of an origin-symmetric convex body is again such a body.

   theorem coordinatePolar_is_symmetric_convex_body {K : Set (I → ℝ)} (hK : IsCompact K)
       (hconv : Convex ℝ K) (hsym : ∀ x ∈ K, -x ∈ K) (hint : (interior K).Nonempty) :
       IsCompact (coordinatePolar K) ∧ Convex ℝ (coordinatePolar K) ∧
         (∀ p ∈ coordinatePolar K, -p ∈ coordinatePolar K) ∧
         (interior (coordinatePolar K)).Nonempty :=
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar