-- Mathlib/Analysis/Convex/Jensen.lean
/-- Convex **strict Jensen inequality**.

If the function is strictly convex, the weights are strictly positive and the indexed family of
points is non-constant, then Jensen's inequality is strict.

See also `StrictConvexOn.map_sum_eq_iff`. -/
lemma StrictConvexOn.map_sum_lt (hf : StrictConvexOn 𝕜 s f) (h₀ : ∀ i ∈ t, 0 < w i)
    (h₁ : ∑ i ∈ t, w i = 1) (hmem : ∀ i ∈ t, p i ∈ s) (hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) :
    f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ j ∈ cons j (cons k u hk✝) ⋯

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Tactic:
have hj : j ∉ u := by simp [u]

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj✝ : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
hj : j ∉ u
⊢ f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
h₀ : ∀ i ∈ t, 0 < w i
h₁ : ∑ i ∈ t, w i = 1
hmem : ∀ i ∈ t, p i ∈ s
j : ι
hj : j ∈ t
k : ι
hk : k ∈ t
hjk : p j ≠ p k
this : k ∈ t.erase j
u : Finset ι := (t.erase j).erase k
⊢ j ∉ u

Tactic:
simp [u]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) =
    w j • f (p j) + w k • f (p k) + ∑ x ∈ u, w x • f (p x)

Tactic:
match_scalars <;> field_simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
⊢ f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))

Tactic:
let c := w j + w k

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
⊢ f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_4
ι : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : OrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
w : ι → 𝕜
p : ι → E
hf : StrictConvexOn 𝕜 s f
j k : ι
hjk : p j ≠ p k
u : Finset ι
hj✝ : j ∉ u
hk✝ : k ∉ u
h₀ : ∀ i ∈ cons j (cons k u hk✝) ⋯, 0 < w i
h₁ : ∑ i ∈ cons j (cons k u hk✝) ⋯, w i = 1
hmem : ∀ i ∈ cons j (cons k u hk✝) ⋯, p i ∈ s
hj : j ∈ cons j (cons k u hk✝) ⋯
hk : k ∈ cons j (cons k u hk✝) ⋯
this✝¹ : k ∈ (cons j (cons k u hk✝) ⋯).erase j
this✝ : 0 < w j
this : 0 < w k
c : 𝕜 := w j + w k
hc : w j / c + w k / c = 1
⊢ f (w j • p j + (w k • p k + ∑ i ∈ u, w i • p i)) < w j • f (p j) + (w k • f (p k) + ∑ i ∈ u, w i • f (p i))

Tactic:
calc f (w j • p j + (w k • p k + ∑ x ∈ u, w x • p x))
  _ = f (c • ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • p x) := by
    congrm f ?_
    match_scalars <;> field_simp
  _ ≤ c • f ((w j / c) • p j + (w k / c) • p k) + ∑ x ∈ u, w x • f (p x) :=
    hf.convexOn.map_add_sum_le (fun i hi ↦ (h₀ _ <| by simp [hi]).le)
        (by simpa [-cons_eq_insert, ← add_assoc] using h₁)
        (forall_of_forall_cons <| forall_of_forall_cons hmem) (by positivity) <| by
         refine hf.1 (hmem _ <| by simp) (hmem _ <| by simp) ?_ ?_ hc <;> positivity
  _ < c • ((w j / c) • f (p j) + (w k / c) • f (p k)) + ∑ x ∈ u, w x • f (p x) := by
    gcongr; refine hf.2 (hmem _ <| by simp) (hmem _ <| by simp) hjk ?_ ?_ hc <;> positivity
  _ = (w j • f (p j) + w k • f (p k)) + ∑ x ∈ u, w x • f (p x) := by
    match_scalars <;> field_simp
  _ = w j • f (p j) + (w k • f (p k) + ∑ x ∈ u, w x • f (p x)) := by abel_nf

Result:
no goals