OAI/Analysis/LpDimension/ConvexSelection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SubpolynomialLp.hilbertMul line 16
2. lemma OAI.SubpolynomialLp.hilbertMul_add line 18
3. lemma OAI.SubpolynomialLp.hilbertMul_smul line 23
4. lemma OAI.SubpolynomialLp.hilbertMul_mul line 28
5. lemma OAI.SubpolynomialLp.hilbertMul_inner line 34
6. lemma OAI.SubpolynomialLp.hilbertMul_contraction line 40
7. lemma OAI.SubpolynomialLp.weighted_error_to_uniform line 59
8. lemma OAI.SubpolynomialLp.convex_cost_selection line 160

   Source documentation

   Convex separation replaces fixed-point reweighting.

   lemma convex_cost_selection {X : Type uX} {E : Type uE} [AddCommGroup X] [Module ℝ X]
       [Fintype E] [Nonempty E] {A : Set X} (hA : Convex ℝ A)
       (c : E → X → ℝ) (hc : ∀ e, ConvexOn ℝ A (c e))
       (hcn : ∀ e x, x ∈ A → 0 ≤ c e x) (B : ℝ) (hB : 0 < B)
       (hw : ∀ w : E → ℝ, (∀ e, 0 < w e) → (∑ e, w e) = 1 →
         ∃ x ∈ A, (∑ e, w e*c e x) ≤ B) :
       ∃ x ∈ A, ∀ e, c e x < 2*B := by
   …

9. lemma OAI.SubpolynomialLp.simultaneous_convex_cost_selection line 187