Theorem: QuasiconvexOn.monotone_comp (Sion/Concavexity.lean)

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
⊢ QuasiconvexOn 𝕜 s (g ∘ f)
Tactic:
intro c
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
⊢ Convex 𝕜 {x | x ∈ s ∧ (g ∘ f) x ≤ c}

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
⊢ Convex 𝕜 {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
intro x hx y hy
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
y : E
hy : y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
y : E
hy : y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
simp only [Function.comp_apply, mem_setOf_eq] at hx hy
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
intro a b ha hb hab
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ {x | x ∈ s ∧ (g ∘ f) x ≤ c}
Tactic:
simp only [Function.comp_apply, mem_setOf_eq]
State after:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

State before:
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
cases le_total (f x) (f y) with
| inl h => 
    specialize hf (f y) ⟨hx.1, h⟩ ⟨hy.1, le_rfl⟩ ha hb hab
    simp only [mem_setOf_eq] at hf 
    exact ⟨hf.1, le_trans (hg hf.2) hy.2⟩
| inr h =>
    specialize hf (f x) ⟨hx.1, le_rfl⟩ ⟨hy.1, h⟩ ha hb hab
    simp only [mem_setOf_eq] at hf 
    exact ⟨hf.1, le_trans (hg hf.2) hx.2⟩
State after:
no goals

State before:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
specialize hf (f y) ⟨hx.1, h⟩ ⟨hy.1, le_rfl⟩ ha hb hab
State after:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ {x | x ∈ s ∧ f x ≤ f y}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

State before:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ {x | x ∈ s ∧ f x ≤ f y}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
simp only [mem_setOf_eq] at hf
State after:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

State before:
case inl
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f x ≤ f y
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f y
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
exact ⟨hf.1, le_trans (hg hf.2) hy.2⟩
State after:
no goals

State before:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
hf : QuasiconvexOn 𝕜 s f
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
specialize hf (f x) ⟨hx.1, le_rfl⟩ ⟨hy.1, h⟩ ha hb hab
State after:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

State before:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ {x_1 | x_1 ∈ s ∧ f x_1 ≤ f x}
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
simp only [mem_setOf_eq] at hf
State after:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c

State before:
case inr
𝕜 : Type u_1
E : Type u_2
β✝ : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : SMul 𝕜 E
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder β
inst✝ : Preorder γ
s : Set E
f : E → β
g : β → γ
hg : Monotone g
c : γ
x : E
hx : x ∈ s ∧ g (f x) ≤ c
y : E
hy : y ∈ s ∧ g (f y) ≤ c
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : f y ≤ f x
hf : a • x + b • y ∈ s ∧ f (a • x + b • y) ≤ f x
⊢ a • x + b • y ∈ s ∧ g (f (a • x + b • y)) ≤ c
Tactic:
exact ⟨hf.1, le_trans (hg hf.2) hx.2⟩
State after:
no goals