internlm/Lean-Github huggingface dataset:
Theorem: uneven_bounded
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
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ Complex.abs (z.1 - c0) ^ n * ‖unevenSeries u z.2 n‖ ≤ s ^ n * (c * t⁻¹ ^ n)
Tactic:
bound [ch n _ z1t]
Proof state after:
no goals
Theorem: uneven_bounded
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
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ s ^ n * (c * t⁻¹ ^ n) = c * (s ^ n * t⁻¹ ^ n)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: uneven_bounded
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
sr : s < r1
t : ℝ
ts : s < t
tr : t < r1
tp : t > 0
c : ℝ
cp : c ≥ 0
ch : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 t, ‖unevenSeries u z1 n‖ ≤ c * t⁻¹ ^ n
z : ℂ × ℂ
zs : dist z.1 c0 < s ∧ dist z.2 c1 < s
z1t : z.2 ∈ closedBall c1 t
z1r : z.2 ∈ closedBall c1 r1
ds' : z.1 - c0 ∈ EMetric.ball 0 (ENNReal.ofReal s)
hs : HasSum (fun n => (z.1 - c0) ^ n • (unevenSeries u z.2).coeff n) (f z)
g : ℕ → ℝ := fun n => c * (s / t) ^ n
gs : HasSum g (c * (1 - s / t)⁻¹)
n : ℕ
ds : Complex.abs (z.1 - c0) < s
⊢ c * (s ^ n * t⁻¹ ^ n) = c * (s / t) ^ n
Tactic:
rw [← mul_pow, ← div_eq_mul_inv]
Proof state after:
no goals
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
⊢ AnalyticOn ℂ f s
Tactic:
have h : Har f s := ⟨fa0, fa1⟩
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
⊢ AnalyticOn ℂ f s
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
⊢ AnalyticOn ℂ f s
Tactic:
intro c cs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases Metric.isOpen_iff.mp so c cs with ⟨r, rp, rs⟩
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases exists_between rp with ⟨t, tp, tr⟩
Proof state after:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ AnalyticAt ℂ f c
Tactic:
have bs : closedBall (c.1, c.2) t ⊆ s := by
  refine _root_.trans ?_ rs; simp only [fst_snd_eq]; exact Metric.closedBall_subset_ball tr
Proof state after:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
⊢ AnalyticAt ℂ f c
Tactic:
rcases to_uneven (h.mono bs) tp with ⟨c0', r0, r1, us, c0s, u⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
⊢ AnalyticAt ℂ f c
Tactic:
have cr : abs (c.1 - c0') < r1 := by
  simp only [Complex.dist_eq, Metric.mem_ball] at c0s; exact c0s
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
⊢ AnalyticAt ℂ f c
Tactic:
rcases exists_between cr with ⟨v, vc, vr⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
⊢ AnalyticAt ℂ f c
Tactic:
rcases uneven_bounded u (lt_of_le_of_lt (Complex.abs.nonneg _) vc) vr with ⟨b, _, fb⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ AnalyticAt ℂ f c
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ AnalyticAt ℂ f c
Tactic:
have fa := of_bounded (h.mono ?_) Metric.isOpen_ball fb
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ AnalyticAt ℂ f c

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
⊢ ball (c0', c.2) v ⊆ s
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall (c.1, c.2) t ⊆ s
Tactic:
refine _root_.trans ?_ rs
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall (c.1, c.2) t ⊆ ball c r
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall (c.1, c.2) t ⊆ ball c r
Tactic:
simp only [fst_snd_eq]
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall c t ⊆ ball c r
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
⊢ closedBall c t ⊆ ball c r
Tactic:
exact Metric.closedBall_subset_ball tr
Proof state after:
no goals
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
⊢ Complex.abs (c.1 - c0') < r1
Tactic:
simp only [Complex.dist_eq, Metric.mem_ball] at c0s
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
u : Uneven f c0' c.2 r0 r1
c0s : Complex.abs (c.1 - c0') < r1
⊢ Complex.abs (c.1 - c0') < r1
Theorem: Pair.hartogs
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
u : Uneven f c0' c.2 r0 r1
c0s : Complex.abs (c.1 - c0') < r1
⊢ Complex.abs (c.1 - c0') < r1
Tactic:
exact c0s
Proof state after:
no goals
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ AnalyticAt ℂ f c
Tactic:
apply fa
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ c ∈ ball (c0', c.2) v
Theorem: Pair.hartogs
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
so : IsOpen s
fa0 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z0 => f (z0, c1)) c0
fa1 : ∀ (c0 c1 : ℂ), (c0, c1) ∈ s → AnalyticAt ℂ (fun z1 => f (c0, z1)) c1
h : Har f s
c : ℂ × ℂ
cs : c ∈ s
r : ℝ
rp : r > 0
rs : ball c r ⊆ s
t : ℝ
tp : 0 < t
tr : t < r
bs : closedBall (c.1, c.2) t ⊆ s
c0' : ℂ
r0 r1 : ℝ
us : ball c0' r1 ⊆ closedBall c.1 t
c0s : c.1 ∈ ball c0' r1
u : Uneven f c0' c.2 r0 r1
cr : Complex.abs (c.1 - c0') < r1
v : ℝ
vc : Complex.abs (c.1 - c0') < v
vr : v < r1
b : ℝ
left✝ : b ≥ 0
fb : ∀ z ∈ ball (c0', c.2) v, ‖f z‖ ≤ b
fa : AnalyticOn ℂ f (ball (c0', c.2) v)
⊢ c ∈ ball (c0', c.2) v
Tactic:
simp only [Metric.mem_ball, Prod.dist_eq, Complex.dist_eq, dist_self, ge_iff_le, apply_nonneg,
  max_eq_left, vc]
Proof state after:
no goals