[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
⊢ StrictConvex 𝕜 univ
[PROOFSTEP]
intro x _ y _ _ a b _ _ _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x✝ y✝ : E
a✝⁶ b✝ : 𝕜
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ interior univ
[PROOFSTEP]
rw [interior_univ]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x✝ y✝ : E
a✝⁶ b✝ : 𝕜
x : E
a✝⁵ : x ∈ univ
y : E
a✝⁴ : y ∈ univ
a✝³ : x ≠ y
a b : 𝕜
a✝² : 0 < a
a✝¹ : 0 < b
a✝ : a + b = 1
⊢ a • x + b • y ∈ univ
[PROOFSTEP]
exact mem_univ _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s ∩ t)
[PROOFSTEP]
intro x hx y hy hxy a b ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (s ∩ t)
[PROOFSTEP]
rw [interior_inter]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s ∩ interior t
[PROOFSTEP]
exact ⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 hxy ha hb hab⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x y : E
a b : 𝕜
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
⊢ StrictConvex 𝕜 (⋃ (i : ι), s i)
[PROOFSTEP]
rintro x hx y hy hxy a b ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : x ∈ ⋃ (i : ι), s i
y : E
hy : y ∈ ⋃ (i : ι), s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (⋃ (i : ι), s i)
[PROOFSTEP]
rw [mem_iUnion] at hx hy
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : ∃ i, x ∈ s i
y : E
hy : ∃ i, y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (⋃ (i : ι), s i)
[PROOFSTEP]
obtain ⟨i, hx⟩ := hx
[GOAL]
case intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hy : ∃ i, y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
⊢ a • x + b • y ∈ interior (⋃ (i : ι), s i)
[PROOFSTEP]
obtain ⟨j, hy⟩ := hy
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ a • x + b • y ∈ interior (⋃ (i : ι), s i)
[PROOFSTEP]
obtain ⟨k, hik, hjk⟩ := hdir i j
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ y✝ : E
a✝ b✝ : 𝕜
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ a • x + b • y ∈ interior (⋃ (i : ι), s i)
[PROOFSTEP]
exact interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
S : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S
hS : ∀ (s : Set E), s ∈ S → StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃₀ S)
[PROOFSTEP]
rw [sUnion_eq_iUnion]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x y : E
a b : 𝕜
S : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S
hS : ∀ (s : Set E), s ∈ S → StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃ (i : ↑S), ↑i)
[PROOFSTEP]
exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ↑f
⊢ StrictConvex 𝕜 (↑f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ↑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : ↑f x ≠ ↑f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ interior (↑f '' s)
[PROOFSTEP]
refine' hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, _⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommMonoid E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
s : Set E
inst✝³ : Semiring 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : Module 𝕝 F
inst✝ : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap ↑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : ↑f x ≠ ↑f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ↑f (a • x + b • y) = a • ↑f x + b • ↑f y
[PROOFSTEP]
rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
⊢ StrictConvex 𝕜 (↑f ⁻¹' s)
[PROOFSTEP]
intro x hx y hy hxy a b ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (↑f ⁻¹' s)
[PROOFSTEP]
refine' preimage_interior_subset_interior_preimage hf _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑f ⁻¹' interior s
[PROOFSTEP]
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ interior s
[PROOFSTEP]
exact hs hx hy (hfinj.ne hxy) ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
⊢ StrictConvex 𝕜 s
[PROOFSTEP]
refine' strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
⊢ (fun x y => openSegment 𝕜 x y ⊆ interior s) x y
[PROOFSTEP]
cases' hxy.lt_or_lt with hlt hlt <;> [skip; rw [openSegment_symm]]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
⊢ (fun x y => openSegment 𝕜 x y ⊆ interior s) x y
[PROOFSTEP]
cases' hxy.lt_or_lt with hlt hlt
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : x < y
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
skip
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
rw [openSegment_symm]
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : x < y
⊢ openSegment 𝕜 x y ⊆ interior s
[PROOFSTEP]
exact
  (openSegment_subset_Ioo hlt).trans (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹¹ : OrderedSemiring 𝕜
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalSpace F
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
s✝ : Set E
inst✝⁴ : TopologicalSpace β
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : OrderTopology β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set β
hs : OrdConnected s
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 y x ⊆ interior s
[PROOFSTEP]
exact
  (openSegment_subset_Ioo hlt).trans (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s)
[PROOFSTEP]
intro x hx y hy hxy a b ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior ((fun x => z + x) ⁻¹' s)
[PROOFSTEP]
refine' preimage_interior_subset_interior_preimage (continuous_add_left _) _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
[PROOFSTEP]
have h := hs hx hy ((add_right_injective _).ne hxy) ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ interior s
⊢ a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
[PROOFSTEP]
rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)
[PROOFSTEP]
simpa only [add_comm] using hs.preimage_add_right z
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s + t)
[PROOFSTEP]
rintro _ ⟨v, w, hv, hw, rfl⟩ _ ⟨x, y, hx, hy, rfl⟩ h a b ha hb hab
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x x_1 => x + x_1) v w + b • (fun x x_1 => x + x_1) x y ∈ interior (s + t)
[PROOFSTEP]
rw [smul_add, smul_add, add_add_add_comm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
[PROOFSTEP]
obtain rfl | hvx := eq_or_ne v x
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)
[PROOFSTEP]
refine' interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)
[PROOFSTEP]
rw [Convex.combo_self hab, singleton_add]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ v + (a • w + b • y) ∈ interior ((fun x x_1 => x + x_1) v '' t)
[PROOFSTEP]
exact (isOpenMap_add_left _).image_interior_subset _ (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
[PROOFSTEP]
exact subset_interior_add_left (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => z + x) '' s)
[PROOFSTEP]
simpa only [singleton_add] using (strictConvex_singleton z).add hs
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => x + z) '' s)
[PROOFSTEP]
simpa only [add_comm] using hs.add_left z
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
x : E
hs : StrictConvex 𝕜 s
c : 𝕝
⊢ StrictConvex 𝕜 (c • s)
[PROOFSTEP]
obtain rfl | hc := eq_or_ne c 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
x : E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (0 • s)
[PROOFSTEP]
exact (subsingleton_zero_smul_set _).strictConvex
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝¹⁰ : OrderedSemiring 𝕜
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : AddCommGroup E
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜 F
inst✝³ : LinearOrderedField 𝕝
inst✝² : Module 𝕝 E
inst✝¹ : ContinuousConstSMul 𝕝 E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
x : E
hs : StrictConvex 𝕜 s
c : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)
[PROOFSTEP]
exact hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
⊢ StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s)
[PROOFSTEP]
classical
obtain rfl | hc := eq_or_ne c 0
· simp_rw [zero_smul, preimage_const]
  split_ifs
  · exact strictConvex_univ
  · exact strictConvex_empty
refine' hs.linear_preimage (LinearMap.lsmul _ _ c) _ (smul_right_injective E hc)
unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
exact continuous_const_smul _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
⊢ StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s)
[PROOFSTEP]
obtain rfl | hc := eq_or_ne c 0
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 ((fun z => 0 • z) ⁻¹' s)
[PROOFSTEP]
simp_rw [zero_smul, preimage_const]
[GOAL]
case inl
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (if 0 ∈ s then univ else ∅)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
h✝ : 0 ∈ s
⊢ StrictConvex 𝕜 univ
[PROOFSTEP]
exact strictConvex_univ
[GOAL]
case neg
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
h✝ : ¬0 ∈ s
⊢ StrictConvex 𝕜 ∅
[PROOFSTEP]
exact strictConvex_empty
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s)
[PROOFSTEP]
refine' hs.linear_preimage (LinearMap.lsmul _ _ c) _ (smul_right_injective E hc)
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ Continuous ↑(↑(LinearMap.lsmul 𝕜 E) c)
[PROOFSTEP]
unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
[GOAL]
case inr
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : NoZeroSMulDivisors 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ Continuous
    ↑(↑{
            toAddHom :=
              {
                toFun := fun m =>
                  {
                    toAddHom :=
                      { toFun := (fun x x_1 => x • x_1) m,
                        map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                    map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) },
                map_add' :=
                  (_ :
                    ∀ (m₁ m₂ : 𝕜),
                      (fun m =>
                            {
                              toAddHom :=
                                { toFun := fun x => m • x,
                                  map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                              map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                          (m₁ + m₂) =
                        (fun m =>
                              {
                                toAddHom :=
                                  { toFun := fun x => m • x,
                                    map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                            m₁ +
                          (fun m =>
                              {
                                toAddHom :=
                                  { toFun := fun x => m • x,
                                    map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                            m₂) },
            map_smul' :=
              (_ :
                ∀ (c m : 𝕜),
                  AddHom.toFun
                      {
                        toFun := fun m =>
                          {
                            toAddHom :=
                              { toFun := fun x => m • x,
                                map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                            map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) },
                        map_add' :=
                          (_ :
                            ∀ (m₁ m₂ : 𝕜),
                              (fun m =>
                                    {
                                      toAddHom :=
                                        { toFun := fun x => m • x,
                                          map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                      map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                                  (m₁ + m₂) =
                                (fun m =>
                                      {
                                        toAddHom :=
                                          { toFun := fun x => m • x,
                                            map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                        map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                                    m₁ +
                                  (fun m =>
                                      {
                                        toAddHom :=
                                          { toFun := fun x => m • x,
                                            map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                        map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                                    m₂) }
                      (c • m) =
                    ↑(RingHom.id 𝕜) c •
                      AddHom.toFun
                        {
                          toFun := fun m =>
                            {
                              toAddHom :=
                                { toFun := fun x => m • x,
                                  map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                              map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) },
                          map_add' :=
                            (_ :
                              ∀ (m₁ m₂ : 𝕜),
                                (fun m =>
                                      {
                                        toAddHom :=
                                          { toFun := fun x => m • x,
                                            map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                        map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                                    (m₁ + m₂) =
                                  (fun m =>
                                        {
                                          toAddHom :=
                                            { toFun := fun x => m • x,
                                              map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                          map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                                      m₁ +
                                    (fun m =>
                                        {
                                          toAddHom :=
                                            { toFun := fun x => m • x,
                                              map_add' := (_ : ∀ (b₁ b₂ : E), m • (b₁ + b₂) = m • b₁ + m • b₂) },
                                          map_smul' := (_ : ∀ (c : 𝕜) (m_1 : E), m • c • m_1 = c • m • m_1) })
                                      m₂) }
                        m) }
        c)
[PROOFSTEP]
exact continuous_const_smul _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
⊢ x = y
[PROOFSTEP]
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
[PROOFSTEP]
classical
by_contra hxy
exact
  (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, rfl⟩).2
    (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel'_right _ _)
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
[PROOFSTEP]
by_contra hxy
[GOAL]
case intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace E
inst✝⁶ : TopologicalSpace F
inst✝⁵ : AddCommGroup E
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜 F
s t : Set E
x y : E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
hxy : ¬x = y
⊢ False
[PROOFSTEP]
exact
  (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel'_right _ _, rfl⟩).2
    (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel'_right _ _)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y ∈ interior s
[PROOFSTEP]
have h : x + t • y = (1 - t) • x + t • (x + y) := by
  rw [smul_add, ← add_assoc, ← _root_.add_smul, sub_add_cancel, one_smul]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y = (1 - t) • x + t • (x + y)
[PROOFSTEP]
rw [smul_add, ← add_assoc, ← _root_.add_smul, sub_add_cancel, one_smul]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ interior s
[PROOFSTEP]
rw [h]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ interior s
[PROOFSTEP]
refine' hs hx hxy (fun h => hy <| add_left_cancel _) (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel _ _)
[GOAL]
case refine'_1
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h✝ : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
⊢ ?refine'_2 h + y = ?refine'_2 h + 0
case refine'_2
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x = x + y → E
[PROOFSTEP]
rw [← h, add_zero]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ t • x ∈ interior s
[PROOFSTEP]
simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ 0 + x ∈ s
[PROOFSTEP]
simpa using hx
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ interior s
[PROOFSTEP]
apply h.openSegment_subset hx hy hxy
[GOAL]
case a
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y
[PROOFSTEP]
rw [openSegment_eq_image']
[GOAL]
case a
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
x y : E
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • (y - x) ∈ (fun θ => x + θ • (y - x)) '' Ioo 0 1
[PROOFSTEP]
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x y : E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
⊢ StrictConvex 𝕜 (↑f ⁻¹' s)
[PROOFSTEP]
intro x hx y hy hxy a b ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y✝ : E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (↑f ⁻¹' s)
[PROOFSTEP]
refine' preimage_interior_subset_interior_preimage hf _
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y✝ : E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑f ⁻¹' interior s
[PROOFSTEP]
rw [mem_preimage, Convex.combo_affine_apply hab]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ t : Set E
x✝ y✝ : E
s : Set F
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : Continuous ↑f
hfinj : Injective ↑f
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ interior s
[PROOFSTEP]
exact hs hx hy (hfinj.ne hxy) ha hb hab
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ↑f
⊢ StrictConvex 𝕜 (↑f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁶ : OrderedRing 𝕜
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x✝ y✝ : E
hs : StrictConvex 𝕜 s
f : E →ᵃ[𝕜] F
hf : IsOpenMap ↑f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : ↑f x ≠ ↑f y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ interior (↑f '' s)
[PROOFSTEP]
exact
  hf.image_interior_subset _ ⟨a • x + b • y, ⟨hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, Convex.combo_affine_apply hab⟩⟩
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
[PROOFSTEP]
apply h hx hy hxy (div_pos ha <| add_pos ha hb) (div_pos hb <| add_pos ha hb)
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ a / (a + b) + b / (a + b) = 1
[PROOFSTEP]
rw [← add_div]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a + b) / (a + b) = 1
[PROOFSTEP]
exact div_self (add_pos ha hb).ne'
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s
[PROOFSTEP]
convert h hx hy hxy ha hb
[GOAL]
case h.e'_4.h.e'_5.h.e'_5
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a = a / (a + b)
[PROOFSTEP]
rw [hab, div_one]
[GOAL]
case h.e'_4.h.e'_6.h.e'_5
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ b = b / (a + b)
[PROOFSTEP]
rw [hab, div_one]
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ x ∈ t • interior s
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans ht).ne']
[GOAL]
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
β : Type u_5
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t⁻¹ • x ∈ interior s
[PROOFSTEP]
exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (inv_pos.2 <| zero_lt_one.trans ht) (inv_lt_one ht)


[GOAL]
c : ℝ
⊢ IntegrableOn exp (Iic c)
[PROOFSTEP]
refine'
  integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c (fun y => intervalIntegrable_exp.1) tendsto_id
    (eventually_of_mem (Iic_mem_atBot 0) fun y _ => _)
[GOAL]
c y : ℝ
x✝ : y ∈ Iic 0
⊢ ∫ (x : ℝ) in id y..c, ‖exp x‖ ≤ exp c
[PROOFSTEP]
simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]
[GOAL]
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ exp (id y)
[PROOFSTEP]
exact (exp_pos _).le
[GOAL]
c : ℝ
⊢ ∫ (x : ℝ) in Iic c, exp x = exp c
[PROOFSTEP]
refine' tendsto_nhds_unique (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) _
[GOAL]
c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in id i..c, exp x) atBot (𝓝 (exp c))
[PROOFSTEP]
simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]
[GOAL]
c : ℝ
⊢ 𝓝 (exp c) = 𝓝 (exp c - 0)
[PROOFSTEP]
rw [sub_zero]
[GOAL]
c : ℝ
⊢ Tendsto (fun i => exp c - exp (id i)) atBot (𝓝 (exp c - 0))
[PROOFSTEP]
exact tendsto_exp_atBot.const_sub _
[GOAL]
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, exp (-x) = exp (-c)
[PROOFSTEP]
simpa only [integral_comp_neg_Ioi] using integral_exp_Iic (-c)
[GOAL]
⊢ ∫ (x : ℝ) in Ioi 0, exp (-x) = 1
[PROOFSTEP]
simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t => t ^ a) (Ioi c)
[PROOFSTEP]
have hd : ∀ (x : ℝ) (_ : x ∈ Ici c), HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x :=
  by
  intro x hx
  convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
  field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
[PROOFSTEP]
intro x hx
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
[PROOFSTEP]
convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
[GOAL]
case h.e'_7
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)
[PROOFSTEP]
field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ a + 1 < 0
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ IntegrableOn (fun t => t ^ a) (Ioi c)
[PROOFSTEP]
have ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1))) :=
  by
  apply Tendsto.div_const
  simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
[PROOFSTEP]
apply Tendsto.div_const
[GOAL]
case hf
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun a_1 => a_1 ^ (a + 1)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ 0 < -(a + 1)
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ IntegrableOn (fun t => t ^ a) (Ioi c)
[PROOFSTEP]
exact integrableOn_Ioi_deriv_of_nonneg' hd (fun t ht => rpow_nonneg_of_nonneg (hc.trans ht).le a) ht
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
[PROOFSTEP]
have hd : ∀ (x : ℝ) (_ : x ∈ Ici c), HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x :=
  by
  intro x hx
  convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
  field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
[PROOFSTEP]
intro x hx
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
[PROOFSTEP]
convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
[GOAL]
case h.e'_7
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)
[PROOFSTEP]
field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ a + 1 < 0
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
[PROOFSTEP]
have ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1))) :=
  by
  apply Tendsto.div_const
  simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
[PROOFSTEP]
apply Tendsto.div_const
[GOAL]
case hf
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun a_1 => a_1 ^ (a + 1)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ 0 < -(a + 1)
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
[PROOFSTEP]
convert integral_Ioi_of_hasDerivAt_of_tendsto' hd (integrableOn_Ioi_rpow_of_lt ha hc) ht using 1
[GOAL]
case h.e'_3
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ -c ^ (a + 1) / (a + 1) = 0 / (a + 1) - c ^ (a + 1) / (a + 1)
[PROOFSTEP]
simp only [neg_div, zero_div, zero_sub]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t => ↑t ^ a) (Ioi c)
[PROOFSTEP]
rw [IntegrableOn, ← integrable_norm_iff, ← IntegrableOn]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun a_1 => ‖↑a_1 ^ a‖) (Ioi c)
a : ℂ ha : a.re < -1 c : ℝ hc : 0 < c ⊢ AEStronglyMeasurable (fun t => ↑t ^ a) (Measure.restrict volume (Ioi c))
[PROOFSTEP]
refine' (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => _) measurableSet_Ioi
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖↑x ^ a‖
[PROOFSTEP]
dsimp only
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖↑x ^ a‖
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos (hc.trans hx)]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun t => ↑t ^ a) (Measure.restrict volume (Ioi c))
[PROOFSTEP]
refine' ContinuousOn.aestronglyMeasurable (fun t ht => _) measurableSet_Ioi
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (fun t => ↑t ^ a) (Ioi c) t
[PROOFSTEP]
exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ ∫ (t : ℝ) in Ioi c, ↑t ^ a = -↑c ^ (a + 1) / (a + 1)
[PROOFSTEP]
refine' tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi c (integrableOn_Ioi_cpow_of_lt ha hc) tendsto_id) _
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun i => ∫ (x : ℝ) in c..id i, ↑x ^ a) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
[PROOFSTEP]
suffices Tendsto (fun x : ℝ => ((x : ℂ) ^ (a + 1) - (c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 <| -c ^ (a + 1) / (a + 1))
  by
  refine' this.congr' ((eventually_gt_atTop 0).mp (eventually_of_forall fun x hx => _))
  dsimp only
  rw [integral_cpow, id.def]
  refine' Or.inr ⟨_, not_mem_uIcc_of_lt hc hx⟩
  apply_fun Complex.re
  rw [Complex.neg_re, Complex.one_re]
  exact ha.ne
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
⊢ Tendsto (fun i => ∫ (x : ℝ) in c..id i, ↑x ^ a) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
[PROOFSTEP]
refine' this.congr' ((eventually_gt_atTop 0).mp (eventually_of_forall fun x hx => _))
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1) = (fun i => ∫ (x : ℝ) in c..id i, ↑x ^ a) x
[PROOFSTEP]
dsimp only
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1) = ∫ (x : ℝ) in c..id x, ↑x ^ a
[PROOFSTEP]
rw [integral_cpow, id.def]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ -1 < a.re ∨ a ≠ -1 ∧ ¬0 ∈ uIcc c (id x)
[PROOFSTEP]
refine' Or.inr ⟨_, not_mem_uIcc_of_lt hc hx⟩
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a ≠ -1
[PROOFSTEP]
apply_fun Complex.re
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ (-1).re
[PROOFSTEP]
rw [Complex.neg_re, Complex.one_re]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this : Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a.re ≠ -1
[PROOFSTEP]
exact ha.ne
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun x => (↑x ^ (a + 1) - ↑c ^ (a + 1)) / (a + 1)) atTop (𝓝 (-↑c ^ (a + 1) / (a + 1)))
[PROOFSTEP]
simp_rw [← zero_sub, sub_div]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun x => ↑x ^ (a + 1) / (a + 1) - ↑c ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1) - ↑c ^ (a + 1) / (a + 1)))
[PROOFSTEP]
refine' (Tendsto.div_const _ _).sub_const _
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun x => ↑x ^ (a + 1)) atTop (𝓝 0)
[PROOFSTEP]
rw [tendsto_zero_iff_norm_tendsto_zero]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun e => ‖↑e ^ (a + 1)‖) atTop (𝓝 0)
[PROOFSTEP]
refine'
  (tendsto_rpow_neg_atTop (by linarith : 0 < -(a.re + 1))).congr'
    ((eventually_gt_atTop 0).mp (eventually_of_forall fun x hx => _))
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ 0 < -(a.re + 1)
[PROOFSTEP]
linarith
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
⊢ x ^ (- -(a.re + 1)) = (fun e => ‖↑e ^ (a + 1)‖) x
[PROOFSTEP]
simp_rw [neg_neg, Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]


[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ StrictConvexOn ℝ (Ici 0) fun x => x ^ n
[PROOFSTEP]
apply StrictMonoOn.strictConvexOn_of_deriv (convex_Ici _) (continuousOn_pow _)
[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (deriv fun x => x ^ n) (interior (Ici 0))
[PROOFSTEP]
rw [deriv_pow', interior_Ici]
[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ StrictMonoOn (fun x => ↑n * x ^ (n - 1)) (Ioi 0)
[PROOFSTEP]
exact fun x (hx : 0 < x) y hy hxy =>
  mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_left hxy hx.le <| Nat.sub_pos_of_lt hn)
    (Nat.cast_pos.2 <| zero_lt_two.trans_le hn)
[GOAL]
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictConvexOn ℝ univ fun x => x ^ n
[PROOFSTEP]
apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)
[GOAL]
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a => a ^ n)
[PROOFSTEP]
rw [deriv_pow']
[GOAL]
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
[PROOFSTEP]
replace h := Nat.pos_of_ne_zero h
[GOAL]
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
[PROOFSTEP]
exact StrictMono.const_mul (Odd.strictMono_pow <| Nat.Even.sub_odd h hn <| Nat.odd_iff.2 rfl) (Nat.cast_pos.2 h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
⊢ 0 ≤ (if f x ≤ 0 then -1 else 1) * f x
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : f x ≤ 0
⊢ 0 ≤ -1 * f x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : ¬f x ≤ 0
⊢ 0 ≤ 1 * f x
[PROOFSTEP]
simp at hx ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
x : α
x✝ : x ∈ s
hx : 0 < f x
⊢ 0 ≤ f x
[PROOFSTEP]
exact le_of_lt hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommRing β
f : α → β
inst✝ : DecidablePred fun x => f x ≤ 0
s : Finset α
h0 : Even (card (filter (fun x => f x ≤ 0) s))
⊢ ∏ x in s, (if f x ≤ 0 then -1 else 1) * f x = ∏ x in s, f x
[PROOFSTEP]
rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one, Finset.prod_const,
  neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]
[GOAL]
m : ℤ
n : ℕ
hn : Even n
⊢ 0 ≤ ∏ k in Finset.range n, (m - ↑k)
[PROOFSTEP]
rcases hn with ⟨n, rfl⟩
[GOAL]
case intro
m : ℤ
n : ℕ
⊢ 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
[PROOFSTEP]
induction' n with n ihn
[GOAL]
case intro.zero
m : ℤ
⊢ 0 ≤ ∏ k in Finset.range (Nat.zero + Nat.zero), (m - ↑k)
[PROOFSTEP]
simp
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (n + n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
[PROOFSTEP]
rw [← two_mul] at ihn
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ ∏ k in Finset.range (Nat.succ n + Nat.succ n), (m - ↑k)
[PROOFSTEP]
rw [← two_mul, Nat.succ_eq_add_one, mul_add, mul_one, ← one_add_one_eq_two, ← add_assoc, Finset.prod_range_succ,
  Finset.prod_range_succ, mul_assoc]
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (∏ x in Finset.range ((1 + 1) * n), (m - ↑x)) * ((m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1)))
[PROOFSTEP]
refine' mul_nonneg ihn _
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
⊢ 0 ≤ (m - ↑((1 + 1) * n)) * (m - ↑((1 + 1) * n + 1))
[PROOFSTEP]
generalize (1 + 1) * n = k
[GOAL]
case intro.succ
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
cases' le_or_lt m k with hmk hmk
[GOAL]
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
have : m ≤ k + 1 := hmk.trans (lt_add_one (k : ℤ)).le
[GOAL]
case intro.succ.inl
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
convert mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _
[GOAL]
case intro.succ.inl.convert_2
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : m ≤ ↑k
this : m ≤ ↑k + 1
⊢ m - ↑(k + 1) ≤ 0
[PROOFSTEP]
convert sub_nonpos_of_le this
[GOAL]
case intro.succ.inr
m : ℤ
n : ℕ
ihn : 0 ≤ ∏ k in Finset.range (2 * n), (m - ↑k)
k : ℕ
hmk : ↑k < m
⊢ 0 ≤ (m - ↑k) * (m - ↑(k + 1))
[PROOFSTEP]
exact mul_nonneg (sub_nonneg_of_le hmk.le) (sub_nonneg_of_le hmk)
[GOAL]
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
⊢ 0 < ∏ k in Finset.range n, (m - ↑k)
[PROOFSTEP]
refine' (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm _
[GOAL]
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : 0 = ∏ k in Finset.range n, (m - ↑k)
⊢ m ∈ Ico 0 ↑n
[PROOFSTEP]
rw [eq_comm, Finset.prod_eq_zero_iff] at h
[GOAL]
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
h : ∃ a, a ∈ Finset.range n ∧ m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
[PROOFSTEP]
obtain ⟨a, ha, h⟩ := h
[GOAL]
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ m ∈ Ico 0 ↑n
[PROOFSTEP]
rw [sub_eq_zero.1 h]
[GOAL]
case intro.intro
m : ℤ
n : ℕ
hn : Even n
hm : ¬m ∈ Ico 0 ↑n
a : ℕ
ha : a ∈ Finset.range n
h : m - ↑a = 0
⊢ ↑a ∈ Ico 0 ↑n
[PROOFSTEP]
exact ⟨Int.ofNat_zero_le _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩
[GOAL]
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (Ioi 0) fun x => x ^ m
[PROOFSTEP]
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
[GOAL]
case hf
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (fun x => x ^ m) (Ioi 0)
[PROOFSTEP]
exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ∀ (x : ℝ), x ∈ Ioi 0 → 0 < deriv^[2] (fun x => x ^ m) x
[PROOFSTEP]
intro x hx
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : x ∈ Ioi 0
⊢ 0 < deriv^[2] (fun x => x ^ m) x
[PROOFSTEP]
rw [mem_Ioi] at hx
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < deriv^[2] (fun x => x ^ m) x
[PROOFSTEP]
rw [iter_deriv_zpow]
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i in Finset.range 2, (↑m - ↑i)) * x ^ (m - ↑2)
[PROOFSTEP]
refine' mul_pos _ (zpow_pos_of_pos hx _)
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (↑m - ↑i)
[PROOFSTEP]
norm_cast
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < ∏ i in Finset.range 2, (m - ↑i)
[PROOFSTEP]
refine' int_prod_range_pos (by simp only) fun hm => _
[GOAL]
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ Even 2
[PROOFSTEP]
simp only
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ Ico 0 ↑2
⊢ False
[PROOFSTEP]
rw [← Finset.coe_Ico] at hm
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm✝ : m ∈ Ico 0 ↑2
hm : m ∈ ↑(Finset.Ico 0 ↑2)
⊢ False
[PROOFSTEP]
norm_cast at hm
[GOAL]
case hf''
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm✝ : m ∈ Ico 0 ↑2
hm : m ∈ Finset.Ico 0 2
⊢ False
[PROOFSTEP]
fin_cases hm
[GOAL]
case hf''.head
x : ℝ
hx : 0 < x
hm₀ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 0 ≠ 0
hm₁ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 0 ≠ 1
hm : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 0 ∈ Ico 0 ↑2
⊢ False
[PROOFSTEP]
simp_all
  -- Porting note: `simp_all` was `cc`
[GOAL]
case hf''.tail.head
x : ℝ
hx : 0 < x
hm₀ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 1 ≠ 0
hm₁ : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 1 ≠ 1
hm : ↑(Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0)) 1 ∈ Ico 0 ↑2
⊢ False
[PROOFSTEP]
simp_all
  -- Porting note: `simp_all` was `cc`
[GOAL]
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x => sqrt x * log x) ((2 + log x) / (2 * sqrt x)) x
[PROOFSTEP]
convert (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1
[GOAL]
case h.e'_7
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * sqrt x) = 1 / (2 * sqrt x) * log x + sqrt x * x⁻¹
[PROOFSTEP]
rw [add_div, div_mul_right (sqrt x) two_ne_zero, ← div_eq_mul_inv, sqrt_div_self', add_comm, div_eq_mul_one_div,
  mul_comm]
[GOAL]
x : ℝ
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
[PROOFSTEP]
cases' lt_or_le 0 x with hx hx
[GOAL]
case inl
x : ℝ
hx : 0 < x
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
[PROOFSTEP]
exact (hasDerivAt_sqrt_mul_log hx.ne').deriv
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = 0
[PROOFSTEP]
refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
[GOAL]
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => sqrt x * log x) 0 (Iic 0) x
[PROOFSTEP]
refine' (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => _) hx
[GOAL]
case inr
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ sqrt x * log x = 0
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, zero_mul]
[GOAL]
x : ℝ
⊢ deriv^[2] (fun x => sqrt x * log x) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
simp only [Nat.iterate, deriv_sqrt_mul_log']
[GOAL]
x : ℝ
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
cases' le_or_lt x 0 with hx hx
[GOAL]
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, zero_pow zero_lt_three, mul_zero, div_zero]
[GOAL]
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = 0
[PROOFSTEP]
refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
[GOAL]
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => (2 + log x) / (2 * sqrt x)) 0 (Iic 0) x
[PROOFSTEP]
refine' (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => _) hx
[GOAL]
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * sqrt x) = 0
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
[GOAL]
case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
have h₀ : sqrt x ≠ 0 := sqrt_ne_zero'.2 hx
[GOAL]
case inr
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
[PROOFSTEP]
convert
  (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
      mul_ne_zero two_ne_zero h₀).deriv using
  1
[GOAL]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) = (x⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
[PROOFSTEP]
nth_rw 3 [← mul_self_sqrt hx.le]
[GOAL]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) =
    ((sqrt x * sqrt x)⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -(log x * (sqrt x * sqrt x * (2 * sqrt x) * (2 * sqrt x) ^ 2)) =
    (2 * sqrt x * (2 * sqrt x) - sqrt x * sqrt x * ((2 + log x) * 2)) * (4 * sqrt x ^ 3)
[PROOFSTEP]
ring
[GOAL]
⊢ StrictConcaveOn ℝ (Ioi 1) fun x => sqrt x * log x
[PROOFSTEP]
apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_
[GOAL]
⊢ ContinuousOn (fun x => sqrt x * log x) (Ioi 1)
[PROOFSTEP]
exact continuous_sqrt.continuousOn.mul (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))
[GOAL]
x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x => sqrt x * log x) x < 0
[PROOFSTEP]
rw [deriv2_sqrt_mul_log x]
[GOAL]
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (↑4 * sqrt x ^ 3) < 0
[PROOFSTEP]
exact
  div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
    (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))
[GOAL]
⊢ StrictConcaveOn ℝ (Icc 0 π) sin
[PROOFSTEP]
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_sin fun x hx => ?_
[GOAL]
x : ℝ
hx : x ∈ interior (Icc 0 π)
⊢ deriv^[2] sin x < 0
[PROOFSTEP]
rw [interior_Icc] at hx
[GOAL]
x : ℝ
hx : x ∈ Ioo 0 π
⊢ deriv^[2] sin x < 0
[PROOFSTEP]
simp [sin_pos_of_mem_Ioo hx]
[GOAL]
⊢ StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos
[PROOFSTEP]
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_cos fun x hx => ?_
[GOAL]
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ deriv^[2] cos x < 0
[PROOFSTEP]
rw [interior_Icc] at hx
[GOAL]
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ deriv^[2] cos x < 0
[PROOFSTEP]
simp [cos_pos_of_mem_Ioo hx]


[GOAL]
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
cases' hx.lt_or_lt with hx hx
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
have : sqrt =ᶠ[𝓝 x] fun _ => 0 := (gt_mem_nhds hx).mono fun x hx => sqrt_eq_zero_of_nonpos hx.le
[GOAL]
case inl
x : ℝ
hx✝ : x ≠ 0
hx : x < 0
this : sqrt =ᶠ[𝓝 x] fun x => 0
⊢ HasStrictDerivAt sqrt 0 x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
exact
  ⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
    contDiffAt_const.congr_of_eventuallyEq this⟩
[GOAL]
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
have : ↑2 * sqrt x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
[GOAL]
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ 2 * sqrt x ^ (2 - 1) ≠ 0
[PROOFSTEP]
simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
[GOAL]
case inr
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x ∧ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
constructor
[GOAL]
case inr.left
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ HasStrictDerivAt sqrt (1 / (2 * sqrt x)) x
[PROOFSTEP]
simpa using sqLocalHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)
[GOAL]
case inr.right
x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
this : 2 * sqrt x ^ (2 - 1) ≠ 0
⊢ ∀ (n : ℕ∞), ContDiffAt ℝ n sqrt x
[PROOFSTEP]
exact fun n => sqLocalHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (sqrt x)) (contDiffAt_id.pow 2)
[GOAL]
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y => Real.sqrt (f y)) (f' / (2 * Real.sqrt (f x))) s x
[PROOFSTEP]
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasDerivAt_sqrt hx).comp_hasDerivWithinAt x hf
[GOAL]
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y => Real.sqrt (f y)) (f' / (2 * Real.sqrt (f x))) x
[PROOFSTEP]
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasDerivAt_sqrt hx).comp x hf
[GOAL]
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun t => Real.sqrt (f t)) (f' / (2 * Real.sqrt (f x))) x
[PROOFSTEP]
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasStrictDerivAt_sqrt hx).comp x hf


[GOAL]
x✝ y x : ℝ
⊢ exp (arsinh x) = x + sqrt (1 + x ^ 2)
[PROOFSTEP]
apply exp_log
[GOAL]
case hx
x✝ y x : ℝ
⊢ 0 < x + sqrt (1 + x ^ 2)
[PROOFSTEP]
rw [← neg_lt_iff_pos_add']
[GOAL]
case hx
x✝ y x : ℝ
⊢ -x < sqrt (1 + x ^ 2)
[PROOFSTEP]
apply lt_sqrt_of_sq_lt
[GOAL]
case hx.h
x✝ y x : ℝ
⊢ (-x) ^ 2 < 1 + x ^ 2
[PROOFSTEP]
simp
[GOAL]
x y : ℝ
⊢ arsinh 0 = 0
[PROOFSTEP]
simp [arsinh]
[GOAL]
x✝ y x : ℝ
⊢ arsinh (-x) = -arsinh x
[PROOFSTEP]
rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh]
[GOAL]
x✝ y x : ℝ
⊢ -x + sqrt (1 + (-x) ^ 2) = (x + sqrt (1 + x ^ 2))⁻¹
[PROOFSTEP]
apply eq_inv_of_mul_eq_one_left
[GOAL]
case h
x✝ y x : ℝ
⊢ (-x + sqrt (1 + (-x) ^ 2)) * (x + sqrt (1 + x ^ 2)) = 1
[PROOFSTEP]
rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel]
[GOAL]
case h
x✝ y x : ℝ
⊢ 0 ≤ 1 + x ^ 2
[PROOFSTEP]
exact add_nonneg zero_le_one (sq_nonneg _)
[GOAL]
x✝ y x : ℝ
⊢ sinh (arsinh x) = x
[PROOFSTEP]
rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq]
[GOAL]
x✝ y x : ℝ
⊢ (x + sqrt (1 + x ^ 2) - (-x + sqrt (1 + x ^ 2))) / 2 = x
[PROOFSTEP]
field_simp
[GOAL]
x✝ y x : ℝ
⊢ cosh (arsinh x) = sqrt (1 + x ^ 2)
[PROOFSTEP]
rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]
[GOAL]
x y : ℝ
⊢ 0 ≤ arsinh x ↔ 0 ≤ x
[PROOFSTEP]
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
[GOAL]
x y : ℝ
⊢ arsinh x ≤ 0 ↔ x ≤ 0
[PROOFSTEP]
rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
[GOAL]
x✝ y x : ℝ
⊢ HasStrictDerivAt arsinh (sqrt (1 + x ^ 2))⁻¹ x
[PROOFSTEP]
convert
  sinhHomeomorph.toLocalHomeomorph.hasStrictDerivAt_symm (mem_univ x) (cosh_pos _).ne' (hasStrictDerivAt_sinh _) using 2
[GOAL]
case h.e'_7.h.e'_3
x✝ y x : ℝ
⊢ sqrt (1 + x ^ 2) = cosh (↑(LocalHomeomorph.symm (Homeomorph.toLocalHomeomorph sinhHomeomorph)) x)
[PROOFSTEP]
exact (cosh_arsinh _).symm