internlm/Lean-Github huggingface dataset:
Theorem: unevenSeries_analytic
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
⊢ ↑‖(0, w1 - z1)‖₊ < r
Tactic:
simp only [EMetric.mem_ball, edist_dist, Complex.dist_eq] at w1s
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ↑‖(0, w1 - z1)‖₊ < r
Theorem: unevenSeries_analytic
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ↑‖(0, w1 - z1)‖₊ < r
Tactic:
simp only [Prod.nnnorm_def', nnnorm_zero, max_eq_right, zero_le', ← edist_eq_coe_nnnorm,
  edist_dist, Complex.dist_eq, sub_zero]
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ENNReal.ofReal (Complex.abs (w1 - z1)) < r
Theorem: unevenSeries_analytic
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
w1s : ENNReal.ofReal (Complex.abs (w1 - z1)) < s
⊢ ENNReal.ofReal (Complex.abs (w1 - z1)) < r
Tactic:
exact lt_of_lt_of_le w1s sr
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof state before:
case h.e'_9.h.h.e'_1.h.e'_4
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
x✝ : ℂ
⊢ w1 = (c0, z1).2 + (0, w1 - z1).2
Tactic:
simp only [add_sub_cancel]
Proof state after:
no goals
Theorem: unevenSeries_analytic
Proof state before:
case h.e'_11
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
n : ℕ
z1 : ℂ
z1s : z1 ∈ ball c1 r1
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p (c0, z1) r
g : ℂ → ℂ × ℂ := fun w1 => (0, w1 - z1)
ta : AnalyticAt ℂ (fun x => p.changeOrigin (g x) n) z1
s' : ℝ := r1 - dist z1 c1
s : ℝ≥0∞ := min r (ENNReal.ofReal s')
s'p : s' > 0
sp : s > 0
sr : s ≤ r
sb : EMetric.ball z1 s ⊆ ball c1 r1
w1 : ℂ
w1s : w1 ∈ EMetric.ball z1 s
p0 : HasFPowerSeriesAt (fun z0 => f (z0, w1)) (unevenSeries u w1) c0
wz : ↑‖(0, w1 - z1)‖₊ < r
⊢ c0 = (c0, z1).1 + (0, w1 - z1).1
Tactic:
simp only [add_sub_cancel, add_zero]
Proof state after:
no goals
Theorem: unevenTerm.analytic
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
n : ℕ
⊢ AnalyticOn ℂ (fun z1 => unevenTerm u z1 n) (ball c1 r1)
Tactic:
have e : ∀ z1, unevenTerm u z1 n =
    (cmmapApplyCmap ℂ (fun _ : Fin n ↦ ℂ) E fun _ ↦ 1) (unevenSeries u z1 n) := by
  intro z1; simp [unevenTerm, ←unevenSeries_apply, cmmapApplyCmap, unevenSeries,
    ContinuousLinearMap.coe_mk', LinearMap.coe_mk]
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
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => unevenTerm u z1 n) (ball c1 r1)
Theorem: unevenTerm.analytic
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
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => unevenTerm u z1 n) (ball c1 r1)
Tactic:
simp_rw [e]
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
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)) (ball c1 r1)
Theorem: unevenTerm.analytic
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
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)) (ball c1 r1)
Tactic:
exact ContinuousLinearMap.comp_analyticOn _ (unevenSeries_analytic u n)
Proof state after:
no goals
Theorem: unevenTerm.analytic
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
n : ℕ
⊢ ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
Tactic:
intro z1
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
n : ℕ
z1 : ℂ
⊢ unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
Theorem: unevenTerm.analytic
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
n : ℕ
z1 : ℂ
⊢ unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
Tactic:
simp [unevenTerm, ←unevenSeries_apply, cmmapApplyCmap, unevenSeries,
ContinuousLinearMap.coe_mk', LinearMap.coe_mk]
Proof state after:
no goals
Theorem: unevenLog_uniform_bound
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 : ℝ
sr : s < r1
⊢ ∃ b, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ b
Tactic:
rcases unevenSeries_uniform_bound u sr with ⟨c, a, _, ap, h⟩
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 (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∃ b, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ b
Theorem: unevenLog_uniform_bound
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 (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∃ b, ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ b
Tactic:
use maxLog 0 (r1 * (max 1 c * a))
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
⊢ ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, unevenLog u n z1 ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
intro n z zs
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
h : ∀ (n : ℕ), ∀ z1 ∈ closedBall c1 s, ‖unevenSeries u z1 n‖ ≤ c * a ^ n
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
specialize h n z zs
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenSeries u z n‖ ≤ c * a ^ n
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenSeries u z n‖ ≤ c * a ^ n
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
simp_rw [unevenSeries_norm] at h
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
⊢ unevenLog u n z ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
rw [unevenLog]
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
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
s : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
by_cases n0 : n = 0
Proof state after:
case pos
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : n = 0
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))

case neg
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
Proof state before:
case neg
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
have np : n ≥ 1 := Nat.one_le_of_lt (Nat.pos_of_ne_zero n0)
Proof state after:
case neg
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
Proof state before:
case neg
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ (↑n)⁻¹ * maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ maxLog 0 (r1 * (max 1 c * a))
Tactic:
rw [inv_mul_le_iff (Nat.cast_pos.mpr (Nat.pos_of_ne_zero n0) : 0 < (n : ℝ))]
Proof state after:
case neg
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))
Theorem: unevenLog_uniform_bound
Proof state before:
case neg
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ maxLog (-1) ‖r1 ^ n • unevenTerm u z n‖ ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))
Tactic:
apply maxLog_le
Proof state after:
case neg.yb
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ -1 ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Theorem: unevenLog_uniform_bound
Proof state before:
case neg.yb
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ -1 ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp
Tactic:
trans (0 : ℝ)
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ -1 ≤ 0

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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ 0 ≤ ↑n * maxLog 0 (r1 * (max 1 c * a))

case neg.xy
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 : ℝ
sr : s < r1
c a : ℝ
left✝ : c > 0
ap : a > 0
n : ℕ
z : ℂ
zs : z ∈ closedBall c1 s
h : ‖unevenTerm u z n‖ ≤ c * a ^ n
n0 : ¬n = 0
np : n ≥ 1
⊢ ‖r1 ^ n • unevenTerm u z n‖ ≤ (↑n * maxLog 0 (r1 * (max 1 c * a))).exp