R : Type ?u.1285893
R' : Type ?u.1285896
𝕜 : Type u_2
𝕜₂ : Type ?u.1285902
𝕜₃ : Type ?u.1285905
𝕝 : Type ?u.1285908
E : Type u_1
E₂ : Type ?u.1285914
E₃ : Type ?u.1285917
F : Type ?u.1285920
G : Type ?u.1285923
ι : Type ?u.1285926
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ↑p (a • x + b • y) ≤ a • ↑p x + b • ↑p y
R : Type ?u.1285893
R' : Type ?u.1285896
𝕜 : Type u_2
𝕜₂ : Type ?u.1285902
𝕜₃ : Type ?u.1285905
𝕝 : Type ?u.1285908
E : Type u_1
E₂ : Type ?u.1285914
E₃ : Type ?u.1285917
F : Type ?u.1285920
G : Type ?u.1285923
ι : Type ?u.1285926
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
⊢ ConvexOn ℝ univ ↑p
refine' ⟨convex_univ, fun x _ y _ a b ha hb _ => _⟩
no goals
R : Type ?u.1285893
R' : Type ?u.1285896
𝕜 : Type u_2
𝕜₂ : Type ?u.1285902
𝕜₃ : Type ?u.1285905
𝕝 : Type ?u.1285908
E : Type u_1
E₂ : Type ?u.1285914
E₃ : Type ?u.1285917
F : Type ?u.1285920
G : Type ?u.1285923
ι : Type ?u.1285926
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ↑p (a • x + b • y) ≤ a • ↑p x + b • ↑p y
calc
  p (a • x + b • y) ≤ p (a • x) + p (b • y) := map_add_le_add p _ _
  _ = ‖a • (1 : 𝕜)‖ * p x + ‖b • (1 : 𝕜)‖ * p y := by
    rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
  _ = a * p x + b * p y := by
    rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
      Real.norm_of_nonneg hb]
no goals
R : Type ?u.1285893
R' : Type ?u.1285896
𝕜 : Type u_2
𝕜₂ : Type ?u.1285902
𝕜₃ : Type ?u.1285905
𝕝 : Type ?u.1285908
E : Type u_1
E₂ : Type ?u.1285914
E₃ : Type ?u.1285917
F : Type ?u.1285920
G : Type ?u.1285923
ι : Type ?u.1285926
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ↑p (a • x) + ↑p (b • y) = ‖a • 1‖ * ↑p x + ‖b • 1‖ * ↑p y
rw [← map_smul_eq_mul p, ← map_smul_eq_mul p, smul_one_smul, smul_one_smul]
no goals
R : Type ?u.1285893
R' : Type ?u.1285896
𝕜 : Type u_2
𝕜₂ : Type ?u.1285902
𝕜₃ : Type ?u.1285905
𝕝 : Type ?u.1285908
E : Type u_1
E₂ : Type ?u.1285914
E₃ : Type ?u.1285917
F : Type ?u.1285920
G : Type ?u.1285923
ι : Type ?u.1285926
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
x✝² : x ∈ univ
y : E
x✝¹ : y ∈ univ
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
x✝ : a + b = 1
⊢ ‖a • 1‖ * ↑p x + ‖b • 1‖ * ↑p y = a * ↑p x + b * ↑p y
rw [norm_smul, norm_smul, norm_one, mul_one, mul_one, Real.norm_of_nonneg ha,
  Real.norm_of_nonneg hb]