Theorem: ConvexOn.convex_le' (PowerCalc/Examples/ConvexFunctions.lean)

State before:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
⊢ Convex 𝕜 { x | x ∈ s ∧ f x ≤ r }
Tactic:
intro x hx y hy a b ha hb hab
State after:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ { x | x ∈ s ∧ f x ≤ r }

State before:
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ { x | x ∈ s ∧ f x ≤ r }
Tactic:
constructor
State after:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r

State before:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s

case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Tactic:
{exact hf.1 hx.1 hy.1 ha hb hab}
State after:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r

State before:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Tactic:
{calc
  f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
  _ ≤ a • r + b • r :=
    (add_le_add (smul_le_smul_of_nonneg hx.2 ha) (smul_le_smul_of_nonneg hy.2 hb))
  _ = r := Convex.combo_self hab r
}
State after:
no goals

State before:
case left
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
Tactic:
exact hf.1 hx.1 hy.1 ha hb hab
State after:
no goals

State before:
case right
𝕜 : Type u_1
E : Type u_2
F : Type ?u.19360
α : Type ?u.19363
β : Type u_3
ι : Type ?u.19369
inst✝⁹ : OrderedSemiring 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : OrderedAddCommMonoid α
inst✝⁵ : OrderedAddCommMonoid β
inst✝⁴ : SMul 𝕜 E
inst✝³ : DistribMulAction 𝕜 β
s✝ : Set E
f✝ g : E → β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
r : β
x : E
hx : x ∈ { x | x ∈ s ∧ f x ≤ r }
y : E
hy : y ∈ { x | x ∈ s ∧ f x ≤ r }
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) ≤ r
Tactic:
calc
 f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx.1 hy.1 ha hb hab
 _ ≤ a • r + b • r :=
   (add_le_add (smul_le_smul_of_nonneg hx.2 ha) (smul_le_smul_of_nonneg hy.2 hb))
 _ = r := Convex.combo_self hab r
State after:
no goals