Theorem: UniformlyBoundedOn.deriv (RMT4/Montel.lean)

State before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
⊢ UniformlyBoundedOn (_root_.deriv ∘ F) U
Tactic:
rintro K ⟨hK1, hK2⟩
State after:
case intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q

State before:
case intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q
Tactic:
obtain ⟨δ, hδ, h⟩ := hK2.exists_cthickening_subset_open hU hK1
State after:
case intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q

State before:
case intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q
Tactic:
have e1 : cthickening δ K ∈ compacts U :=
  ⟨h, isCompact_of_isClosed_isBounded isClosed_cthickening hK2.isBounded.cthickening⟩
State after:
case intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q

State before:
case intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q
Tactic:
obtain ⟨Q, hQ1, hQ2⟩ := h1 _ e1
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q
Tactic:
obtain ⟨M, hM⟩ := hQ1.isBounded.subset_closedBall 0
State after:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q

State before:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∃ Q, IsCompact Q ∧ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K Q
Tactic:
refine ⟨closedBall 0 (M / δ), isCompact_closedBall _ _, ?_⟩
State after:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K (closedBall 0 (M / δ))

State before:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
⊢ ∀ (i : ι), MapsTo ((_root_.deriv ∘ F) i) K (closedBall 0 (M / δ))
Tactic:
intro i x hx
State after:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ (_root_.deriv ∘ F) i x ∈ closedBall 0 (M / δ)

State before:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ (_root_.deriv ∘ F) i x ∈ closedBall 0 (M / δ)
Tactic:
simp only [mem_closedBall_zero_iff]
State after:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ ‖(_root_.deriv ∘ F) i x‖ ≤ M / δ

State before:
case intro.intro.intro.intro.intro.intro
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ ‖(_root_.deriv ∘ F) i x‖ ≤ M / δ
Tactic:
refine norm_deriv_le_aux hδ ?_ ?_
State after:
case intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ DiffContOnCl ℂ (F i) (ball x δ)

case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ ∀ z ∈ sphere x δ, ‖F i z‖ ≤ M

State before:
case intro.intro.intro.intro.intro.intro.refine_1
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ DiffContOnCl ℂ (F i) (ball x δ)
Tactic:
exact (h2 i).diffContOnCl_ball ((closedBall_subset_cthickening hx δ).trans h)
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
U K✝ : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
⊢ ∀ z ∈ sphere x δ, ‖F i z‖ ≤ M
Tactic:
rintro z hz
State after:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
U K✝ : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
z : ℂ
hz : z ∈ sphere x δ
⊢ ‖F i z‖ ≤ M

State before:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
U K✝ : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
z : ℂ
hz : z ∈ sphere x δ
⊢ ‖F i z‖ ≤ M
Tactic:
have : z ∈ cthickening δ K :=
  sphere_subset_closedBall.trans (closedBall_subset_cthickening hx δ) hz
State after:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
U K✝ : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
z : ℂ
hz : z ∈ sphere x δ
this : z ∈ cthickening δ K
⊢ ‖F i z‖ ≤ M

State before:
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type u_1
U K✝ : Set ℂ
z✝ : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
h1 : UniformlyBoundedOn F U
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
K : Set ℂ
hK1 : K ⊆ U
hK2 : IsCompact K
δ : ℝ
hδ : 0 < δ
h : cthickening δ K ⊆ U
e1 : cthickening δ K ∈ compacts U
Q : Set ℂ
hQ1 : IsCompact Q
hQ2 : ∀ (i : ι), MapsTo (F i) (cthickening δ K) Q
M : ℝ
hM : Q ⊆ closedBall 0 M
i : ι
x : ℂ
hx : x ∈ K
z : ℂ
hz : z ∈ sphere x δ
this : z ∈ cthickening δ K
⊢ ‖F i z‖ ≤ M
Tactic:
simpa using hM (hQ2 i this)
State after:
no goals