OAI/Analysis/Mahler/ConvexApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SymmetricMahler.continuous_pairing line 16
2. lemma OAI.SymmetricMahler.coordinatePolar_antitone line 19
3. lemma OAI.SymmetricMahler.zero_mem_coordinatePolar line 22
4. lemma OAI.SymmetricMahler.isClosed_coordinatePolar line 26
5. lemma OAI.SymmetricMahler.pairing_of_dual line 33
6. theorem OAI.SymmetricMahler.exists_coordinatePolar_separator line 47

   Source documentation

   Strict separation normalized by a positive separator level. The origin membership makes that level positive, without assuming a supporting maximum.

   theorem exists_coordinatePolar_separator [DecidableEq I] {K : Set (I → ℝ)}
       (hconv : Convex ℝ K) (hclosed : IsClosed K) (hzero : (0 : I → ℝ) ∈ K)
       {x : I → ℝ} (hx : x ∉ K) :
       ∃ p ∈ coordinatePolar K, 1 < ∑ i, p i * x i := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar

7. lemma OAI.SymmetricMahler.polar_pairing_abs line 60
8. theorem OAI.SymmetricMahler.dense_polar_strips_intersection line 69

   Source documentation

   Dense polar constraints recover the original closed convex set.

   theorem dense_polar_strips_intersection [DecidableEq I] {K : Set (I → ℝ)}
       (hconv : Convex ℝ K) (hclosed : IsClosed K) (hzero : (0 : I → ℝ) ∈ K)
       (hsym : ∀ x ∈ K, -x ∈ K)
       (a : ℕ → coordinatePolar K) (ha : DenseRange a) :
       {x : I → ℝ | ∀ j, |∑ i, (a j).val i * x i| ≤ 1} = K := by
   …

   Mentions: OAI.SymmetricMahler.coordinatePolar