[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
⊢ (fun z => z.im ^ ↑n) =O[l] fun z => (z.re ^ r) ^ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
⊢ (fun z => z.im ^ n) =O[l] fun z => (z.re ^ r) ^ n
[PROOFSTEP]
exact hr.pow n
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
z : ℂ
hz : 0 ≤ z.re
⊢ (fun z => (z.re ^ r) ^ ↑n) z = (fun z => z.re ^ (r * ↑n)) z
[PROOFSTEP]
simp only [Real.rpow_mul hz r n, Real.rpow_nat_cast]
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ ↑n
⊢ im =O[l] fun z => z.re ^ ↑n
[PROOFSTEP]
norm_cast at hr
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ n
⊢ im =O[l] fun z => z.re ^ ↑n
[PROOFSTEP]
simpa only [Real.rpow_nat_cast]
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => |z.im|
⊢ im =O[l] fun z => z.re ^ ↑0
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => |z.im|
⊢ im =O[l] fun z => z.re ^ 0
[PROOFSTEP]
simpa only [pow_zero] using @IsBoundedUnder.isBigO_const ℂ ℝ ℝ _ _ _ l him 1 one_ne_zero
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ (x : ℂ), ((fun z => z.im ^ ↑n) ^ 2) x = (x.im ^ ↑n) ^ 2
[PROOFSTEP]
simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ ↑n) ^ 2 = x✝.im ^ (2 * ↑n)
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ n) ^ 2 = x✝.im ^ (2 * n)
[PROOFSTEP]
rw [pow_mul']
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => z.im ^ (2 * ↑n)) =O[l] fun z => Real.exp z.re
[PROOFSTEP]
have := hl.isBigO_im_pow_re (2 * n)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
this : (fun z => z.im ^ ↑(2 * n)) =O[l] fun z => Real.exp z.re
⊢ (fun z => z.im ^ (2 * ↑n)) =O[l] fun z => Real.exp z.re
[PROOFSTEP]
norm_cast at *
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
[PROOFSTEP]
rw [pow_one]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => Real.exp z.re ^ 1) =o[l] fun z => Real.exp z.re ^ 2
[PROOFSTEP]
have := (isLittleO_pow_pow_atTop_of_lt one_lt_two).comp_tendsto <| Real.tendsto_exp_atTop.comp hl.tendsto_re
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
this : ((fun x => x ^ 1) ∘ Real.exp ∘ re) =o[l] ((fun x => x ^ 2) ∘ Real.exp ∘ re)
⊢ (fun z => Real.exp z.re ^ 1) =o[l] fun z => Real.exp z.re ^ 2
[PROOFSTEP]
simpa only [pow_one, Real.rpow_one, Real.rpow_two]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ (x : ℂ), Real.exp x.re ^ 2 = ((fun z => Real.exp z.re) ^ 2) x
[PROOFSTEP]
simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => |z.im| ^ ↑n) ≤ᶠ[l] fun z => Real.exp z.re
[PROOFSTEP]
simpa using (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have h2 : 0 < Real.sqrt 2 := by simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < Real.sqrt 2
[PROOFSTEP]
simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have hz' : 1 ≤ abs z := hz.trans (re_le_abs z)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have _ : 0 < abs z := one_pos.trans_le hz'
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
rw [one_mul, Real.norm_eq_abs, _root_.abs_of_nonneg (Real.log_nonneg hz')]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ Real.log (↑abs z) ≤ ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
refine' le_trans _ (le_abs_self _)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ Real.log (↑abs z) ≤ Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)
[PROOFSTEP]
rw [← Real.log_mul, Real.log_le_log, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ ↑abs z ≤ Real.sqrt 2 * max |z.re| |z.im|
case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ 0 < ↑abs z
case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ 0 < Real.sqrt 2 * max z.re |z.im|
case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ Real.sqrt 2 ≠ 0
case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ max z.re |z.im| ≠ 0
[PROOFSTEP]
exacts [abs_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖
[PROOFSTEP]
filter_upwards [isLittleO_iff_nat_mul_le'.1 hl.isLittleO_log_re_re n, hl.abs_im_pow_eventuallyLE_exp_re n,
  hl.tendsto_re.eventually_gt_atTop 1] with z hre him h₁
[GOAL]
case h
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
cases' le_total |z.im| z.re with hle hle
[GOAL]
case h.inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
rwa [max_eq_left hle]
[GOAL]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
have H : 1 < |z.im| := h₁.trans_le hle
[GOAL]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
norm_cast at *
[GOAL]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
hle : z.re ≤ |z.im|
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H), ← Real.log_pow,
  Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _), abs_of_pos (one_pos.trans h₁)]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
z : ℂ
hz : z ≠ 0
⊢ (let_fun this := fun z => ↑abs z ^ a.re;
      this)
      z =
    (fun z => Real.exp (a.re * Real.log (↑abs z))) z
[PROOFSTEP]
simp only [Real.rpow_def_of_pos, abs.pos hz, mul_comm]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun z => Real.exp (a.re * Real.log (↑abs z))) =o[l] fun x => ‖exp (↑b * x)‖
[PROOFSTEP]
simp only [norm_eq_abs, abs_exp, ofReal_mul_re, Real.isLittleO_exp_comp_exp_comp]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * x.re - a.re * Real.log (↑abs x)) l atTop
[PROOFSTEP]
refine' (IsEquivalent.refl.sub_isLittleO _).symm.tendsto_atTop (hl.tendsto_re.const_mul_atTop hb)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun x => a.re * Real.log (↑abs x)) =o[l] fun x => b * x.re
[PROOFSTEP]
exact (hl.isLittleO_log_abs_re.const_mul_left _).const_mul_right hb.ne'
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z => z ^ a₁ * exp (↑b₁ * z)) z = (fun z => z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)) z
[PROOFSTEP]
simp only
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * exp (↑b₁ * z) = z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)
[PROOFSTEP]
rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel'_right]
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₁ * z) * exp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
[PROOFSTEP]
simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel'_right]
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ (fun z => exp (↑b * z)) =o[l] fun z => z ^ a
[PROOFSTEP]
simpa using hl.isLittleO_cpow_mul_exp hb 0 a
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℕ
⊢ (fun z => z ^ ↑m * exp (↑b₁ * z)) =o[l] fun z => z ^ ↑n * exp (↑b₂ * z)
[PROOFSTEP]
simpa only [cpow_nat_cast] using hl.isLittleO_cpow_mul_exp hb m n
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
m n : ℤ
⊢ (fun z => z ^ ↑m * exp (↑b₁ * z)) =o[l] fun z => z ^ ↑n * exp (↑b₂ * z)
[PROOFSTEP]
simpa only [cpow_int_cast] using hl.isLittleO_cpow_mul_exp hb m n


[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have hp₀' : 0 < 1 / p := by positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < 1 / p
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have hp₁' : 1 < 1 / p := by rw [one_lt_div hp₀]; exact hp₁
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ 1 < 1 / p
[PROOFSTEP]
rw [one_lt_div hp₀]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
⊢ p < 1
[PROOFSTEP]
exact hp₁
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
let f := NNReal.orderIsoRpow (1 / p) hp₀'
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have h₁ : StrictConvexOn ℝ≥0 univ f :=
  by
  refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
  exact
    (strictConvexOn_rpow hp₁').2 (by positivity : 0 ≤ x) (by positivity : 0 ≤ y) (by simp [hxy]) ha hb
      (by simp; norm_cast)
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
⊢ StrictConvexOn ℝ≥0 univ ↑f
[PROOFSTEP]
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑f (a • x + b • y) < a • ↑f x + b • ↑f y
[PROOFSTEP]
exact
  (strictConvexOn_rpow hp₁').2 (by positivity : 0 ≤ x) (by positivity : 0 ≤ y) (by simp [hxy]) ha hb
    (by simp; norm_cast)
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ x
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 ≤ y
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (fun a => ↑a) x ≠ (fun a => ↑a) y
[PROOFSTEP]
simp [hxy]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑(↑(RingHom.id ℝ≥0) a) + ↑(↑(RingHom.id ℝ≥0) b) = 1
[PROOFSTEP]
simp
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑a + ↑b = 1
[PROOFSTEP]
norm_cast
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
have h₂ : ∀ x, f.symm x = x ^ p := by simp [NNReal.orderIsoRpow_symm_eq]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
⊢ ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
[PROOFSTEP]
simp [NNReal.orderIsoRpow_symm_eq]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
h₂ : ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
h₂ : ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
simp only [← h₂]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
hp₀' : 0 < 1 / p
hp₁' : 1 < 1 / p
f : ℝ≥0 ≃o ℝ≥0 := orderIsoRpow (1 / p) hp₀'
h₁ : StrictConvexOn ℝ≥0 univ ↑f
h₂ : ∀ (x : ℝ≥0), ↑(OrderIso.symm f) x = x ^ p
x : ℝ≥0
x✝¹ : x ∈ univ
y : ℝ≥0
x✝ : y ∈ univ
hxy : x ≠ y
a b : ℝ≥0
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑(OrderIso.symm (orderIsoRpow (1 / p) hp₀')) x + b • ↑(OrderIso.symm (orderIsoRpow (1 / p) hp₀')) y <
    ↑(OrderIso.symm (orderIsoRpow (1 / p) hp₀')) (a • x + b • y)
[PROOFSTEP]
exact (f.strictConcaveOn_symm h₁).2 (Set.mem_univ x) (Set.mem_univ y) hxy ha hb hab
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : ¬p = 0 ⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_univ, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
x✝⁷ : ℝ≥0
x✝⁶ : x✝⁷ ∈ univ
x✝⁵ : ℝ≥0
x✝⁴ : x✝⁵ ∈ univ
x✝³ x✝² : ℝ≥0
x✝¹ : 0 ≤ x✝³
x✝ : 0 ≤ x✝²
hab : x✝³ + x✝² = 1
⊢ x✝³ • (fun x => x ^ p) x✝⁷ + x✝² • (fun x => x ^ p) x✝⁵ ≤ (fun x => x ^ p) (x✝³ • x✝⁷ + x✝² • x✝⁵)
[PROOFSTEP]
simp [hp, hab]
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp
  by_cases hp' : p = 1
  case pos => exact ⟨convex_univ, by simp [hp']⟩
  case neg =>
    push_neg at hp'
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp
  by_cases hp' : p = 1
  case pos => exact ⟨convex_univ, by simp [hp']⟩
  case neg =>
    push_neg at hp'
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
push_neg at hp
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
by_cases hp' : p = 1
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : p ≠ 0 hp' : ¬p = 1 ⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_univ, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_univ, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ∀ ⦃x : ℝ≥0⦄,
    x ∈ univ →
      ∀ ⦃y : ℝ≥0⦄,
        y ∈ univ →
          ∀ ⦃a b : ℝ≥0⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → a • (fun x => x ^ p) x + b • (fun x => x ^ p) y ≤ (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
simp [hp']
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp'
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp'
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
push_neg at hp'
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ ConcaveOn ℝ≥0 univ fun x => x ^ p
[PROOFSTEP]
exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
⊢ StrictConcaveOn ℝ≥0 univ ↑sqrt
[PROOFSTEP]
have : NNReal.sqrt = fun (x : ℝ≥0) ↦ x ^ (1 / (2 : ℝ)) := by ext x; exact_mod_cast NNReal.sqrt_eq_rpow x
[GOAL]
⊢ ↑sqrt = fun x => x ^ (1 / 2)
[PROOFSTEP]
ext x
[GOAL]
case h.a
x : ℝ≥0
⊢ ↑(↑sqrt x) = ↑(x ^ (1 / 2))
[PROOFSTEP]
exact_mod_cast NNReal.sqrt_eq_rpow x
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ ↑sqrt
[PROOFSTEP]
rw [this]
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ≥0 univ fun x => x ^ (1 / 2)
[PROOFSTEP]
exact strictConcaveOn_rpow (by positivity) (by linarith)
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ 0 < 1 / 2
[PROOFSTEP]
positivity
[GOAL]
this : ↑sqrt = fun x => x ^ (1 / 2)
⊢ 1 / 2 < 1
[PROOFSTEP]
linarith
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ StrictConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
refine ⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let x' : ℝ≥0 := ⟨x, hx⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let y' : ℝ≥0 := ⟨y, hy⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let a' : ℝ≥0 := ⟨a, by positivity⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
⊢ 0 ≤ a
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
let b' : ℝ≥0 := ⟨b, by positivity⟩
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
⊢ 0 ≤ b
[PROOFSTEP]
positivity
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hx' : (fun z => z ^ p) x = (fun z => z ^ p) x' := rfl
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hy' : (fun z => z ^ p) y = (fun z => z ^ p) y' := rfl
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hxy' : x' ≠ y' := Subtype.ne_of_val_ne hxy
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
have hab' : a' + b' = 1 := by ext; simp [hab]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
⊢ a' + b' = 1
[PROOFSTEP]
ext
[GOAL]
case a
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
⊢ ↑(a' + b') = ↑1
[PROOFSTEP]
simp [hab]
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ a • (fun x => x ^ p) x + b • (fun x => x ^ p) y < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
rw [hx', hy']
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ a • ↑((fun z => z ^ p) x') + b • ↑((fun z => z ^ p) y') < (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
exact
  (NNReal.strictConcaveOn_rpow hp₀ hp₁).2 (Set.mem_univ x') (Set.mem_univ y') hxy' (by exact_mod_cast ha)
    (by exact_mod_cast hb) hab'
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ 0 < a'
[PROOFSTEP]
exact_mod_cast ha
[GOAL]
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
x' : ℝ≥0 := { val := x, property := hx }
y' : ℝ≥0 := { val := y, property := hy }
a' : ℝ≥0 := { val := a, property := (_ : 0 ≤ a) }
b' : ℝ≥0 := { val := b, property := (_ : 0 ≤ b) }
hx' : (fun z => z ^ p) x = ↑((fun z => z ^ p) x')
hy' : (fun z => z ^ p) y = ↑((fun z => z ^ p) y')
hxy' : x' ≠ y'
hab' : a' + b' = 1
⊢ 0 < b'
[PROOFSTEP]
exact_mod_cast hb
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : ¬p = 0 ⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_Ici 0, fun _ _ _ _ _ _ _ _ hab => by simp [hp, hab]⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p = 0
x✝⁷ : ℝ
x✝⁶ : x✝⁷ ∈ Ici 0
x✝⁵ : ℝ
x✝⁴ : x✝⁵ ∈ Ici 0
x✝³ x✝² : ℝ
x✝¹ : 0 ≤ x✝³
x✝ : 0 ≤ x✝²
hab : x✝³ + x✝² = 1
⊢ x✝³ • (fun x => x ^ p) x✝⁷ + x✝² • (fun x => x ^ p) x✝⁵ ≤ (fun x => x ^ p) (x✝³ • x✝⁷ + x✝² • x✝⁵)
[PROOFSTEP]
simp [hp, hab]
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp
  by_cases hp' : p = 1
  case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
  case neg =>
    push_neg at hp'
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp
  by_cases hp' : p = 1
  case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
  case neg =>
    push_neg at hp'
    exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : ¬p = 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
push_neg at hp
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
by_cases hp' : p = 1
[GOAL]
case pos
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
case neg p : ℝ hp₀ : 0 ≤ p hp₁ : p ≤ 1 hp : p ≠ 0 hp' : ¬p = 1 ⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case pos => exact ⟨convex_Ici 0, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact ⟨convex_Ici 0, by simp [hp']⟩
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p = 1
⊢ ∀ ⦃x : ℝ⦄,
    x ∈ Ici 0 →
      ∀ ⦃y : ℝ⦄,
        y ∈ Ici 0 →
          ∀ ⦃a b : ℝ⦄,
            0 ≤ a →
              0 ≤ b → a + b = 1 → a • (fun x => x ^ p) x + b • (fun x => x ^ p) y ≤ (fun x => x ^ p) (a • x + b • y)
[PROOFSTEP]
simp [hp']
[GOAL]
case neg
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp'
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
case neg =>
  push_neg at hp'
  exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : ¬p = 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
push_neg at hp'
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ ConcaveOn ℝ (Ici 0) fun x => x ^ p
[PROOFSTEP]
exact (strictConcaveOn_rpow (by positivity) (lt_of_le_of_ne hp₁ hp')).concaveOn
[GOAL]
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
hp : p ≠ 0
hp' : p ≠ 1
⊢ 0 < p
[PROOFSTEP]
positivity
[GOAL]
⊢ StrictConcaveOn ℝ (Ici 0) sqrt
[PROOFSTEP]
have : Real.sqrt = fun (x : ℝ) ↦ x ^ (1 / (2 : ℝ)) := by ext x; exact Real.sqrt_eq_rpow x
[GOAL]
⊢ sqrt = fun x => x ^ (1 / 2)
[PROOFSTEP]
ext x
[GOAL]
case h
x : ℝ
⊢ sqrt x = x ^ (1 / 2)
[PROOFSTEP]
exact Real.sqrt_eq_rpow x
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ (Ici 0) sqrt
[PROOFSTEP]
rw [this]
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ StrictConcaveOn ℝ (Ici 0) fun x => x ^ (1 / 2)
[PROOFSTEP]
exact strictConcaveOn_rpow (by positivity) (by linarith)
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ 0 < 1 / 2
[PROOFSTEP]
positivity
[GOAL]
this : sqrt = fun x => x ^ (1 / 2)
⊢ 1 / 2 < 1
[PROOFSTEP]
linarith


[GOAL]
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : SMul 𝕜 E
S T : ProperCone 𝕜 E
h : S.toConvexCone = T.toConvexCone
⊢ S = T
[PROOFSTEP]
cases S
[GOAL]
case mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : SMul 𝕜 E
T : ProperCone 𝕜 E
toConvexCone✝ : ConvexCone 𝕜 E
nonempty'✝ : Set.Nonempty toConvexCone✝.carrier
is_closed'✝ : IsClosed toConvexCone✝.carrier
h : { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ }.toConvexCone = T.toConvexCone
⊢ { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ } = T
[PROOFSTEP]
cases T
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : SMul 𝕜 E
toConvexCone✝¹ : ConvexCone 𝕜 E
nonempty'✝¹ : Set.Nonempty toConvexCone✝¹.carrier
is_closed'✝¹ : IsClosed toConvexCone✝¹.carrier
toConvexCone✝ : ConvexCone 𝕜 E
nonempty'✝ : Set.Nonempty toConvexCone✝.carrier
is_closed'✝ : IsClosed toConvexCone✝.carrier
h :
  { toConvexCone := toConvexCone✝¹, nonempty' := nonempty'✝¹, is_closed' := is_closed'✝¹ }.toConvexCone =
    { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ }.toConvexCone
⊢ { toConvexCone := toConvexCone✝¹, nonempty' := nonempty'✝¹, is_closed' := is_closed'✝¹ } =
    { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
inst✝⁴ : OrderedSemiring 𝕜
E : Type u_2
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : Module 𝕜 E
⊢ ConvexCone.Pointed 0.toConvexCone
[PROOFSTEP]
simp [ConvexCone.pointed_zero]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
K : ProperCone ℝ E
⊢ (map (ContinuousLinearMap.id ℝ E) K).toConvexCone = K.toConvexCone
[PROOFSTEP]
simpa using IsClosed.closure_eq K.isClosed
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
K : ProperCone ℝ E
y : E
⊢ y ∈ dual K ↔ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner x y
[PROOFSTEP]
rw [← mem_coe, coe_dual, mem_innerDualCone _ _]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
K : ProperCone ℝ E
y : E
⊢ (∀ (x : E), x ∈ ↑K → 0 ≤ inner x y) ↔ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner x y
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ 0 ∈ (ConvexCone.comap (↑f) S.toConvexCone).carrier
[PROOFSTEP]
simp only [ConvexCone.comap, mem_preimage, map_zero, SetLike.mem_coe, mem_coe]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ 0 ∈ S
[PROOFSTEP]
apply ProperCone.pointed
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ IsClosed (ConvexCone.comap (↑f) S.toConvexCone).carrier
[PROOFSTEP]
simp only [ConvexCone.comap, ContinuousLinearMap.coe_coe]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ IsClosed (↑f ⁻¹' ↑S.toConvexCone)
[PROOFSTEP]
apply IsClosed.preimage f.2 S.isClosed
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
g : F →L[ℝ] G
f : E →L[ℝ] F
S : ProperCone ℝ G
⊢ ↑(comap f (comap g S)) = ↑(comap (comp g f) S)
[PROOFSTEP]
congr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ b ∈ map f K → ∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b
[PROOFSTEP]
simp only [ProperCone.mem_map, ProperCone.mem_dual, adjoint_inner_right, ConvexCone.mem_closure,
  mem_closure_iff_seq_limit]
  -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ (∃ x, (∀ (n : ℕ), x n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)) ∧ Tendsto x atTop (nhds b)) →
    ∀ (y : F), (∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y) → 0 ≤ inner y b
[PROOFSTEP]
rintro ⟨seq, hmem, htends⟩ y hinner
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
⊢ 0 ≤ inner y b
[PROOFSTEP]
suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
h : ∀ (n : ℕ), 0 ≤ inner y (seq n)
⊢ 0 ≤ inner y b
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
⊢ ∀ (n : ℕ), 0 ≤ inner y (seq n)
[PROOFSTEP]
exact ge_of_tendsto' (Continuous.seqContinuous (Continuous.inner (@continuous_const _ _ _ _ y) continuous_id) htends) h
[GOAL]
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
⊢ ∀ (n : ℕ), 0 ≤ inner y (seq n)
[PROOFSTEP]
intro n
[GOAL]
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
n : ℕ
⊢ 0 ≤ inner y (seq n)
[PROOFSTEP]
obtain ⟨_, h, hseq⟩ := hmem n
[GOAL]
case h.intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
n : ℕ
w✝ : E
h : w✝ ∈ ↑K.toConvexCone
hseq : ↑↑f w✝ = seq n
⊢ 0 ≤ inner y (seq n)
[PROOFSTEP]
simpa only [← hseq, real_inner_comm] using hinner h
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ (∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b) → b ∈ map f K
[PROOFSTEP]
intro h
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b
⊢ b ∈ map f K
[PROOFSTEP]
contrapose! h
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
⊢ ∃ y, ↑(↑adjoint f) y ∈ dual K ∧ inner y b < 0
[PROOFSTEP]
obtain ⟨y, hxy, hyb⟩ :=
  ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem _ (K.map f).nonempty (K.map f).isClosed h
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
⊢ ∃ y, ↑(↑adjoint f) y ∈ dual K ∧ inner y b < 0
[PROOFSTEP]
refine' ⟨y, _, hyb⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
⊢ ↑(↑adjoint f) y ∈ dual K
[PROOFSTEP]
simp_rw [ProperCone.mem_dual, adjoint_inner_right]
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
⊢ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
[PROOFSTEP]
intro x hxK
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ 0 ≤ inner (↑f x) y
[PROOFSTEP]
apply hxy (f x)
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑f x ∈ (map f K).toConvexCone
[PROOFSTEP]
rw [ProperCone.coe_map]
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑f x ∈ ConvexCone.closure (ConvexCone.map (↑f) K.toConvexCone)
[PROOFSTEP]
apply subset_closure
[GOAL]
case intro.intro.a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑f x ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
[PROOFSTEP]
rw [SetLike.mem_coe, ConvexCone.mem_map]
[GOAL]
case intro.intro.a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ∃ x_1, x_1 ∈ K.toConvexCone ∧ ↑↑f x_1 = ↑f x
[PROOFSTEP]
refine' ⟨x, hxK, by rw [coe_coe]⟩
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑↑f x = ↑f x
[PROOFSTEP]
rw [coe_coe]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ¬b ∈ map f K
⊢ ∃ y, ↑(↑adjoint f) y ∈ dual K ∧ inner y b < 0
[PROOFSTEP]
contrapose! disj
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b
⊢ b ∈ map f K
[PROOFSTEP]
rwa [K.hyperplane_separation]