internlm/Lean-Github huggingface dataset:
Theorem: cindex_eventually_eq_order
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)
Tactic:
obtain ⟨R, hR, hf⟩ := exists_cindex_eq_order hp
Proof state after:
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)
Theorem: cindex_eventually_eq_order
Proof state before:
case intro.intro
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
⊢ ∃ ε > 0, ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Set.Ioi 0 → cindex z₀ y f = ↑(FormalMultilinearSeries.order p)
Tactic:
exact ⟨R, hR, λ r hr1 hr2 => hf r ⟨hr2, by simpa using lt_of_abs_lt hr1⟩⟩
Proof state after:
no goals
Theorem: cindex_eventually_eq_order
Proof state before:
f g : ℂ → ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
z z₀ c : ℂ
n : ℕ
U : Set ℂ
r✝ : ℝ
hp : HasFPowerSeriesAt f p z₀
R : ℝ
hR : R > 0
hf : ∀ r ∈ Set.Ioo 0 R, cindex z₀ r f = ↑(FormalMultilinearSeries.order p)
r : ℝ
hr1 : dist r 0 < R
hr2 : r ∈ Set.Ioi 0
⊢ r < R
Tactic:
simpa using lt_of_abs_lt hr1
Proof state after:
no goals
Theorem: UniformlyBoundedOn.deriv
Proof 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⟩
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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⟩
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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 _ _, ?_⟩
Proof 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 / δ))
Theorem: UniformlyBoundedOn.deriv
Proof 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
Proof 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 / δ)
Theorem: UniformlyBoundedOn.deriv
Proof 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]
Proof 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 / δ
Theorem: UniformlyBoundedOn.deriv
Proof 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δ ?_ ?_
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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)
Proof state after:
no goals
Theorem: UniformlyBoundedOn.deriv
Proof 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
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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
Proof 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
Theorem: UniformlyBoundedOn.deriv
Proof 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)
Proof state after:
no goals
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof 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
hK : K ∈ compacts U
⊢ EquicontinuousOn F K
Tactic:
apply (equicontinuous_restrict_iff _).mp
Proof state after:
ι : 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
hK : K ∈ compacts U
⊢ Equicontinuous (restrict K ∘ F)
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof 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
hK : K ∈ compacts U
⊢ Equicontinuous (restrict K ∘ F)
Tactic:
rintro ⟨z, hz⟩
Proof state after:
case mk
ι : 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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk
ι : 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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
obtain ⟨δ, hδ, h⟩ := nhds_basis_closedBall.mem_iff.1 (hU.mem_nhds (hK.1 hz))
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
have : ∃ M > 0, ∀ i, MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M) := by
  obtain ⟨Q, hQ1, hQ2⟩ := h1.deriv hU h2 (closedBall z δ) ⟨h, isCompact_closedBall _ _⟩
  obtain ⟨M, hM⟩ := hQ1.isBounded.subset_closedBall 0
  refine ⟨M ⊔ 1, by simp, fun i => ?_⟩
  exact ((hQ2 i).mono_right hM).mono_right <| closedBall_subset_closedBall le_sup_left
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
this : ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
this : ∃ M > 0, ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
obtain ⟨M, hMp, hM⟩ := this
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ EquicontinuousAt (restrict K ∘ F) { val := z, property := hz }
Tactic:
rw [equicontinuousAt_iff]
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (x : ↑K),
        dist x { val := z, property := hz } < δ →
          ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (x : ↑K),
        dist x { val := z, property := hz } < δ →
          ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε
Tactic:
rintro ε hε
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ (x : ↑K),
      dist x { val := z, property := hz } < δ →
        ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ (x : ↑K),
      dist x { val := z, property := hz } < δ →
        ∀ (i : ι), dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i x) < ε
Tactic:
refine ⟨δ ⊓ ε / M, gt_iff_lt.2 (lt_inf_iff.2 ⟨hδ, div_pos hε hMp⟩), λ w hw i => ?_⟩
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i w) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist ((restrict K ∘ F) i { val := z, property := hz }) ((restrict K ∘ F) i w) < ε
Tactic:
simp
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist (F i z) (F i ↑w) < ε
Theorem: UniformlyBoundedOn.equicontinuousOn
Proof state before:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
⊢ dist (F i z) (F i ↑w) < ε
Tactic:
have e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x :=
  λ x hx => (h2 i).differentiableAt (hU.mem_nhds (h hx))
Proof state after:
case mk.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
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
δ : ℝ
hδ : 0 < δ
h : closedBall z δ ⊆ U
M : ℝ
hMp : M > 0
hM : ∀ (i : ι), MapsTo (_root_.deriv (F i)) (closedBall z δ) (closedBall 0 M)
ε : ℝ
hε : ε > 0
w : ↑K
hw : dist w { val := z, property := hz } < δ ⊓ ε / M
i : ι
e1 : ∀ x ∈ closedBall z δ, DifferentiableAt ℂ (F i) x
⊢ dist (F i z) (F i ↑w) < ε