concave Jensen

Stream: general

[Stanislas Polu]

I'm looking at docs#convex_on.map_sum_le and am wondering if we have a concave Jensen available? Or maybe a convenient way to go from one to the other?

[Johan Commelin]

@Yaël Dillies is working very hard on refactoring the convexity library. I think this will fall out of his refactor.

[Stanislas Polu]

Ah! Fascinating (and good news!). So in practice right now I'm stuck with the convex version right?

[Yaël Dillies]

Eheheh, that's what I'm doing at this very moment. Little preview for the curious.

/-- Convex **Jensen's inequality**, `finset.linear_combination` version. -/
lemma convex_on.map_linear_combination_le (hf : convex_on 𝕜 s f)
  (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1)
  (hmem : ∀ i ∈ t, p i ∈ s) : f (t.linear_combination p w) ≤ t.linear_combination (f ∘ p) w :=
begin
  have hmem' : ∀ i ∈ t, (p i, (f ∘ p) i) ∈ {p : E × β | p.1 ∈ s ∧ f p.1 ≤ p.2},
    from λ i hi, ⟨hmem i hi, le_rfl⟩,
  convert (hf.convex_epigraph.linear_combination_mem h₀ h₁ hmem').2;
    simp only [linear_combination, function.comp, prod.smul_fst, prod.fst_sum,
      prod.smul_snd, prod.snd_sum],
end

/-- Concave **Jensen's inequality**, `finset.linear_combination` version. -/
lemma concave_on.le_map_linear_combination (hf : concave_on 𝕜 s f)
  (h₀ : ∀ i ∈ t, 0 ≤ w i) (h₁ : ∑ i in t, w i = 1)
  (hmem : ∀ i ∈ t, p i ∈ s) : t.linear_combination (f ∘ p) w ≤ f (t.linear_combination p w) :=
@convex_on.map_linear_combination_le 𝕜 E (order_dual β) _ _ _ _ _ _ _ _ _ _ _ _ hf h₀ h₁ hmem

[Yaël Dillies]

I swear I didn't even scroll in VScode to pick that.

[Stanislas Polu]

@Yaël Dillies when do you expect this to land on master?

[Stanislas Polu]

oh wait going from one to the other is trivial, just use (-f) and multiply by -1 right.

[Yaël Dillies]

You can make do like that for now.

[Stanislas Polu]

:+1:

[Yaël Dillies]

Erhm... This depends on #9268 for linear_combination to be under that form, and there's currently discussion so as to whether we even want linear_combination. I was expecting #9268 to be merged quickly but the events took another turn, so I will probably open this PR tomorrow and arrange myself so that it can go through before #9268. So I'd say a week?

[Stanislas Polu]

This is fine, I think formalizing some proofs using the current version and a manual transformation for concave functions shouldn't be too hard to port to this new format :+1:

[Stanislas Polu]

@Yaël Dillies how does one go about proving that a function is convex? do we have proofs for the usual suspects (xlogx, -logx, x^a or -x^a, real.exp(a*x)) avaialble?

[Yaël Dillies]

Your heaven lies here: analysis.convex.specific_functions. Many functions are still missing, though.

[Stanislas Polu]

Thanks!

[Johan Commelin]

@Stanislas Polu Btw, this was added in #9356 a couple of days ago

[Stanislas Polu]

@Johan Commelin Yes! Already using it !! :100:

[Yaël Dillies]

This is what I call short cycle production!