E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U ∨ z ∈ U
⊢ ‖f z‖ ≤ C
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ closure U
⊢ ‖f z‖ ≤ C
rw [closure_eq_self_union_frontier, union_comm, mem_union] at hz
case inl
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C

case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
⊢ ‖f z‖ ≤ C
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U ∨ z ∈ U
⊢ ‖f z‖ ≤ C
cases' hz with hz hz
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
⊢ ‖f z‖ ≤ C
case inr
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
⊢ ‖f z‖ ≤ C
rcases exists_ne z with ⟨w, hne⟩
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
⊢ ‖f z‖ ≤ C
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
⊢ ‖f z‖ ≤ C
set e := (lineMap z w : ℂ → E)
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖f z‖ ≤ C
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
⊢ ‖f z‖ ≤ C
have hde : Differentiable ℂ e := (differentiable_id.smul_const (w - z)).add_const z
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ ‖f z‖ ≤ C
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
⊢ ‖f z‖ ≤ C
have hL : AntilipschitzWith (nndist z w)⁻¹ e := antilipschitzWith_lineMap hne.symm
case hd
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)

case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ ‖f z‖ ≤ C
replace hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
case hd
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
⊢ DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)

case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
exact hd.comp hde.diffContOnCl (mapsTo_preimage _ _)
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
⊢ ‖f z‖ ≤ C
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ ‖f z‖ ≤ C
have h₀ : (0 : ℂ) ∈ e ⁻¹' U := by simpa only [mem_preimage, lineMap_apply_zero]
case inr.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C
case inr.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
⊢ ‖f z‖ ≤ C
rcases exists_mem_frontier_isMaxOn_norm (hL.bounded_preimage hU) ⟨0, h₀⟩ hd with ⟨ζ, hζU, hζ⟩
no goals
case inr.intro.intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ ≤ C
calc
  ‖f z‖ = ‖f (e 0)‖ := by simp only [lineMap_apply_zero]
  _ ≤ ‖f (e ζ)‖ := (hζ (subset_closure h₀))
  _ ≤ C := hC _ (hde.continuous.frontier_preimage_subset _ hζU)
no goals
case inl
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ frontier U
⊢ ‖f z‖ ≤ C
exact hC z hz
no goals
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ 0 ∈ e ⁻¹' U
simpa only [mem_preimage, lineMap_apply_zero]
no goals
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Metric.Bounded U
C : ℝ
hC : ∀ (z : E), z ∈ frontier U → ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : (a : ℂ) → (fun a => E) a := ↑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ = ‖f (e 0)‖
simp only [lineMap_apply_zero]