internlm/Lean-Github huggingface dataset:
Theorem: to_uneven
Proof state before:
case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ closedBall c1 (r / 2) ⊆ closedBall c1 r
Tactic:
apply Metric.closedBall_subset_closedBall
Proof state after:
case ht.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ r / 2 ≤ r
Theorem: to_uneven
Proof state before:
case ht.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
⊢ r / 2 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: to_uneven
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
Tactic:
apply a.mono
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2) ⊆ ball c0' r0 ×ˢ ball c1 r
Theorem: to_uneven
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2) ⊆ ball c0' r0 ×ˢ ball c1 r
Tactic:
apply Set.prod_mono
Proof state after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c0' (min r0 (r / 2)) ⊆ ball c0' r0

case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c1 (r / 2) ⊆ ball c1 r
Theorem: to_uneven
Proof state before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c0' (min r0 (r / 2)) ⊆ ball c0' r0

case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c1 (r / 2) ⊆ ball c1 r
Tactic:
apply Metric.ball_subset_ball'
Proof state after:
case hs.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ min r0 (r / 2) + dist c0' c0' ≤ r0

case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c1 (r / 2) ⊆ ball c1 r
Theorem: to_uneven
Proof state before:
case hs.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ min r0 (r / 2) + dist c0' c0' ≤ r0

case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c1 (r / 2) ⊆ ball c1 r
Tactic:
simp only [dist_self, add_zero, min_le_iff, le_refl, true_or_iff]
Proof state after:
case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c1 (r / 2) ⊆ ball c1 r
Theorem: to_uneven
Proof state before:
case ht
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ ball c1 (r / 2) ⊆ ball c1 r
Tactic:
apply Metric.ball_subset_ball
Proof state after:
case ht.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ r / 2 ≤ r
Theorem: to_uneven
Proof state before:
case ht.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
⊢ r / 2 ≤ r
Tactic:
linarith
Proof state after:
no goals
Theorem: to_uneven
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
⊢ min r0 (r / 2) > 0
Tactic:
bound
Proof state after:
no goals
Theorem: to_uneven
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0'✝ c1 z0 z1 w0 w1 : ℂ
r r0✝ r1 b e : ℝ
h : Har f (closedBall (c0, c1) r)
rp : r > 0
r4p : r / 4 > 0
c0' : ℂ
r0 : ℝ
r0p : r0 > 0
a : AnalyticOn ℂ f (ball c0' r0 ×ˢ ball c1 r)
m : dist c0' c0 ≤ r / 4
sub : closedBall c0' (r / 2) ⊆ closedBall c0 r
r01 : min r0 (r / 2) ≤ r / 2
c0m : c0 ∈ ball c0' (r / 2)
h' : Har f (closedBall (c0', c1) (r / 2))
a' : AnalyticOn ℂ f (ball c0' (min r0 (r / 2)) ×ˢ ball c1 (r / 2))
⊢ r / 2 > 0
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_apply
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
z1 : ℂ
n : ℕ
⊢ ((unevenSeries' u r z1 n) fun x => 1) = unevenTerm' u r z1 n
Tactic:
simp only [unevenSeries', ContinuousMultilinearMap.mkPiRing_apply, Finset.prod_const_one,
  one_smul]
Proof state after:
no goals
Theorem: uneven_is_cauchy
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
⊢ unevenSeries' u r z1 = cauchyPowerSeries (fun z0 => f (z0, z1)) c0 r
Tactic:
funext
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = cauchyPowerSeries (fun z0 => f (z0, z1)) c0 r x✝
Theorem: uneven_is_cauchy
Proof state before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ unevenSeries' u r z1 x✝ = cauchyPowerSeries (fun z0 => f (z0, z1)) c0 r x✝
Tactic:
rw [unevenSeries', cauchyPowerSeries]
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝) (unevenTerm' u r z1 x✝) =
    ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝)
      ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r), (z - c0)⁻¹ ^ x✝ • (z - c0)⁻¹ • f (z, z1))
Theorem: uneven_is_cauchy
Proof state before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
x✝ : ℕ
⊢ ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝) (unevenTerm' u r z1 x✝) =
    ContinuousMultilinearMap.mkPiRing ℂ (Fin x✝)
      ((2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c0, r), (z - c0)⁻¹ ^ x✝ • (z - c0)⁻¹ • f (z, z1))
Tactic:
rfl
Proof state after:
no goals
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
set sn := s.toNNReal
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
have sns : s = sn := by simp only [Real.coe_toNNReal', sp.le, max_eq_left, sn]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
have snp : sn > 0 := Real.toNNReal_pos.mpr sp
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (unevenSeries' u s z1) c0 (ENNReal.ofReal s)
Tactic:
rw [uneven_is_cauchy]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 s) c0 (ENNReal.ofReal s)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 s) c0 (ENNReal.ofReal s)
Tactic:
rw [sns, ← ENNReal.coe_nnreal_eq]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 ↑sn) c0 ↑sn
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ HasFPowerSeriesOnBall (fun z0 => f (z0, z1)) (cauchyPowerSeries (fun z0 => f (z0, z1)) c0 ↑sn) c0 ↑sn
Tactic:
refine DifferentiableOn.hasFPowerSeriesOnBall ?_ snp
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 ↑sn)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 ↑sn)
Tactic:
rw [← sns]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 s)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 s)
Tactic:
refine DifferentiableOn.mono ?_ (Metric.closedBall_subset_closedBall sr1)
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 r1)
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
sns : s = ↑sn
snp : sn > 0
⊢ DifferentiableOn ℂ (fun z0 => f (z0, z1)) (closedBall c0 r1)
Tactic:
exact AnalyticOn.differentiableOn (u.h.on0 z1s)
Proof state after:
no goals
Theorem: Uneven.has_series
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s✝ : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sp : s > 0
sr1 : s ≤ r1
z1s : z1 ∈ closedBall c1 r1
sn : ℝ≥0 := s.toNNReal
⊢ s = ↑sn
Tactic:
simp only [Real.coe_toNNReal', sp.le, max_eq_left, sn]
Proof state after:
no goals
Theorem: unevenTerm_eq
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
⊢ z1 ∈ closedBall c1 r1 → unevenTerm' u r z1 = unevenTerm u z1
Tactic:
intro z1s
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenTerm' u r z1 = unevenTerm u z1
Theorem: unevenTerm_eq
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
⊢ unevenTerm' u r z1 = unevenTerm u z1
Tactic:
funext x
Proof state after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
r : ℝ
rp : r > 0
rr1 : r ≤ r1
z1 : ℂ
z1s : z1 ∈ closedBall c1 r1
x : ℕ
⊢ unevenTerm' u r z1 x = unevenTerm u z1 x