internlm/Lean-Github huggingface dataset:
Theorem: Super.isClosed_critical_not_a
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a z✝ : S
d n : ℕ
s : Super f d a
c : ℂ
z : S
za : ¬z = a
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
⊢ ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → Critical (f x.1) x.2 → x.2 = a
Tactic:
intro ⟨e, w⟩ a b
Proof state after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ (e, w).2 = a✝
Theorem: Super.isClosed_critical_not_a
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ (e, w).2 = a✝
Tactic:
exfalso
Proof state after:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ False
Theorem: Super.isClosed_critical_not_a
Proof state before:
case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c✝ : ℂ
a✝ z✝ : S
d n : ℕ
s : Super f d a✝
c : ℂ
z : S
za : ¬z = a✝
m : ¬Critical (f c) z
o : ∀ (x : ℂ × S), ¬Critical (f x.1) x.2 → ∀ᶠ (y : ℂ × S) in 𝓝 x, ¬Critical (f y.1) y.2
e : ℂ
w : S
a : ¬Critical (f (e, w).1) (e, w).2
b : Critical (f (e, w).1) (e, w).2
⊢ False
Tactic:
exact a b
Proof state after:
no goals
Theorem: Super.bottcherNearIter_mfderiv_ne_zero
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬Precritical (f c) z
⊢ mfderiv I I (s.bottcherNearIter n c) z ≠ 0
Tactic:
apply mderiv_comp_ne_zero' b0
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬Precritical (f c) z
⊢ mfderiv I I (f c)^[n] z ≠ 0
Theorem: Super.bottcherNearIter_mfderiv_ne_zero
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬Precritical (f c) z
⊢ mfderiv I I (f c)^[n] z ≠ 0
Tactic:
contrapose f0
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬mfderiv I I (f c)^[n] z ≠ 0
⊢ ¬¬Precritical (f c) z
Theorem: Super.bottcherNearIter_mfderiv_ne_zero
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : ¬mfderiv I I (f c)^[n] z ≠ 0
⊢ ¬¬Precritical (f c) z
Tactic:
simp only [not_not] at f0 ⊢
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : mfderiv I I (f c)^[n] z = 0
⊢ Precritical (f c) z
Theorem: Super.bottcherNearIter_mfderiv_ne_zero
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
b0 : mfderiv I I (s.bottcherNear c) ((f c)^[n] z) ≠ 0
f0 : mfderiv I I (f c)^[n] z = 0
⊢ Precritical (f c) z
Tactic:
exact critical_iter s.fa.along_snd f0
Proof state after:
no goals
Theorem: Super.iter_nontrivial_a
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
Tactic:
induction' n with n h
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[0] z) a

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Theorem: Super.iter_nontrivial_a
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[0] z) a

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (fun z => z) a

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Theorem: Super.iter_nontrivial_a
Proof state before:
case zero
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (fun z => z) a

case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Tactic:
apply nontrivialHolomorphicAt_id
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Theorem: Super.iter_nontrivial_a
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => (f c)^[n + 1] z) a
Tactic:
simp only [Function.iterate_succ_apply']
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => f c ((f c)^[n] z)) a
Theorem: Super.iter_nontrivial_a
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (fun z => f c ((f c)^[n] z)) a
Tactic:
refine NontrivialHolomorphicAt.comp ?_ h
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) ((f c)^[n] a)
Theorem: Super.iter_nontrivial_a
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) ((f c)^[n] a)
Tactic:
simp only [s.iter_a]
Proof state after:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) a
Theorem: Super.iter_nontrivial_a
Proof state before:
case succ
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
h : NontrivialHolomorphicAt (fun z => (f c)^[n] z) a
⊢ NontrivialHolomorphicAt (f c) a
Tactic:
exact s.f_nontrivial c
Proof state after:
no goals
Theorem: Super.bottcherNearIter_nontrivial_a
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (s.bottcherNear c) ((f c)^[n] a)
Tactic:
simp only [s.iter_a]
Proof state after:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (s.bottcherNear c) a
Theorem: Super.bottcherNearIter_nontrivial_a
Proof state before:
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ NontrivialHolomorphicAt (s.bottcherNear c) a
Tactic:
exact nontrivialHolomorphicAt_of_mfderiv_ne_zero
  (s.bottcherNear_holomorphic _ (s.mem_near c)).along_snd
  (s.bottcherNear_mfderiv_ne_zero c)
Proof state after:
no goals
Theorem: uniformVanishing_to_summable
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
⊢ Summable fun n => f n z
Tactic:
rw [summable_iff_vanishing_norm]
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < ε
Theorem: uniformVanishing_to_summable
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < ε
Tactic:
intro e ep
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e
Theorem: uniformVanishing_to_summable
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e
Tactic:
rcases h e ep with ⟨m, hm⟩
Proof state after:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e
Theorem: uniformVanishing_to_summable
Proof state before:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∃ s, ∀ (t : Finset ℕ), Disjoint t s → ‖t.sum fun i => f i z‖ < e
Tactic:
use Finset.range m
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∀ (t : Finset ℕ), Disjoint t (Finset.range m) → ‖t.sum fun i => f i z‖ < e
Theorem: uniformVanishing_to_summable
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∀ (t : Finset ℕ), Disjoint t (Finset.range m) → ‖t.sum fun i => f i z‖ < e
Tactic:
intro A d
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
d : Disjoint A (Finset.range m)
⊢ ‖A.sum fun i => f i z‖ < e
Theorem: uniformVanishing_to_summable
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
d : Disjoint A (Finset.range m)
⊢ ‖A.sum fun i => f i z‖ < e
Tactic:
calc ‖A.sum (fun n ↦ f n z)‖
  _ ≤ A.sum (fun n ↦ ‖f n z‖) := by bound
  _ < e := hm _ _ (late_iff_disjoint_range.mpr d) zs
Proof state after:
no goals
Theorem: uniformVanishing_to_summable
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
z : ℂ
zs : z ∈ s
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
d : Disjoint A (Finset.range m)
⊢ ‖A.sum fun n => f n z‖ ≤ A.sum fun n => ‖f n z‖
Tactic:
bound
Proof state after:
no goals
Theorem: uniformVanishing_to_uniform_cauchy_series
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ UniformCauchySeqOn (fun N z => N.sum fun n => f n z) atTop s
Tactic:
rw [Metric.uniformCauchySeqOn_iff]
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < ε
Theorem: uniformVanishing_to_uniform_cauchy_series
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < ε
Tactic:
intro e ep
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e
Theorem: uniformVanishing_to_uniform_cauchy_series
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e
Tactic:
rcases h e ep with ⟨m, hm⟩
Proof state after:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e
Theorem: uniformVanishing_to_uniform_cauchy_series
Proof state before:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (m.sum fun n => f n x) (n.sum fun n => f n x) < e
Tactic:
use Finset.range m
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∀ m_1 ≥ Finset.range m, ∀ n ≥ Finset.range m, ∀ x ∈ s, dist (m_1.sum fun n => f n x) (n.sum fun n => f n x) < e
Theorem: uniformVanishing_to_uniform_cauchy_series
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
⊢ ∀ m_1 ≥ Finset.range m, ∀ n ≥ Finset.range m, ∀ x ∈ s, dist (m_1.sum fun n => f n x) (n.sum fun n => f n x) < e
Tactic:
intro A HA B HB z zs
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
HA : A ≥ Finset.range m
B : Finset ℕ
HB : B ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (A.sum fun n => f n z) (B.sum fun n => f n z) < e
Theorem: uniformVanishing_to_uniform_cauchy_series
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e
A : Finset ℕ
HA : A ≥ Finset.range m
B : Finset ℕ
HB : B ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (A.sum fun n => f n z) (B.sum fun n => f n z) < e
Tactic:
calc dist (A.sum fun n ↦ f n z) (B.sum fun n ↦ f n z)
  _ ≤ (A ∆ B).sum fun n ↦ abs (f n z) := symmDiff_bound _ _ _
  _ < e := hm (A ∆ B) z (symmDiff_late HA HB) zs
Proof state after:
no goals
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ HasUniformSum f (tsumOn f) s
Tactic:
rw [HasUniformSum, Metric.tendstoUniformlyOn_iff]
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
⊢ ∀ ε > 0, ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < ε
Tactic:
intro e ep
Proof state after:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Tactic:
rcases h (e / 4) (by linarith) with ⟨m, hm⟩
Proof state after:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
⊢ ∀ᶠ (n : Finset ℕ) in atTop, ∀ x ∈ s, dist (tsumOn f x) (n.sum fun n => f n x) < e
Tactic:
rw [Filter.eventually_atTop]
Proof state after:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
⊢ ∃ a, ∀ b ≥ a, ∀ x ∈ s, dist (tsumOn f x) (b.sum fun n => f n x) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
case intro
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
⊢ ∃ a, ∀ b ≥ a, ∀ x ∈ s, dist (tsumOn f x) (b.sum fun n => f n x) < e
Tactic:
use Finset.range m
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
⊢ ∀ b ≥ Finset.range m, ∀ x ∈ s, dist (tsumOn f x) (b.sum fun n => f n x) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
⊢ ∀ b ≥ Finset.range m, ∀ x ∈ s, dist (tsumOn f x) (b.sum fun n => f n x) < e
Tactic:
intro N Nm z zs
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (N.sum fun n => f n z) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (tsumOn f z) (N.sum fun n => f n z) < e
Tactic:
rw [tsumOn]
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (N.sum fun n => f n z) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
⊢ dist (∑' (n : ℕ), f n z) (N.sum fun n => f n z) < e
Tactic:
generalize G : tsum (fun n ↦ f n z) = g
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
⊢ dist g (N.sum fun n => f n z) < e
Theorem: uniformVanishing_to_tendsto_uniformly_on
Proof state before:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
⊢ dist g (N.sum fun n => f n z) < e
Tactic:
have S : Summable (fun n ↦ f n z) := uniformVanishing_to_summable zs h
Proof state after:
case h
f : ℕ → ℂ → ℂ
s : Set ℂ
h : UniformVanishing f s
e : ℝ
ep : e > 0
m : ℕ
hm : ∀ (N : Finset ℕ) (z : ℂ), Late N m → z ∈ s → (N.sum fun n => Complex.abs (f n z)) < e / 4
N : Finset ℕ
Nm : N ≥ Finset.range m
z : ℂ
zs : z ∈ s
g : ℂ
G : ∑' (n : ℕ), f n z = g
S : Summable fun n => f n z
⊢ dist g (N.sum fun n => f n z) < e