internlm/Lean-Github huggingface dataset:
Theorem: fubini_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in closedBall c r \ {c}, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [←Metric.closedBall_zero, ←annulus_oc]
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in annulus_oc c 0 r, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Theorem: fubini_ball
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ∫ (x : ℂ) in annulus_oc c 0 r, f x = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
apply fubini_annulus
Proof state after:
case fc
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ContinuousOn (fun z => f z) (annulus_cc c 0 r)

case r0p
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ 0 ≤ 0
Theorem: fubini_ball
Proof state before:
case fc
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ ContinuousOn (fun z => f z) (annulus_cc c 0 r)
Tactic:
simpa only [annulus_cc, Metric.ball_zero, diff_empty]
Proof state after:
no goals
Theorem: fubini_ball
Proof state before:
case r0p
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
fc : ContinuousOn f (closedBall c r)
⊢ 0 ≤ 0
Tactic:
rfl
Proof state after:
no goals
Theorem: Complex.volume_closedBall'
Proof state before:
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Tactic:
have c : ContinuousOn (fun _ : ℂ ↦ (1 : ℝ)) (closedBall c r) := continuousOn_const
Proof state after:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2
Theorem: Complex.volume_closedBall'
Proof state before:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2
Tactic:
have f := fubini_ball c
Proof state after:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
f : ∫ (z : ℂ) in closedBall c✝ r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2
Theorem: Complex.volume_closedBall'
Proof state before:
c✝ : ℂ
r : ℝ
rp : r ≥ 0
c : ContinuousOn (fun x => 1) (closedBall c✝ r)
f : ∫ (z : ℂ) in closedBall c✝ r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c✝ r)).toReal = π * r ^ 2
Tactic:
clear c
Proof state after:
c : ℂ
r : ℝ
rp : r ≥ 0
f : ∫ (z : ℂ) in closedBall c r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Theorem: Complex.volume_closedBall'
Proof state before:
c : ℂ
r : ℝ
rp : r ≥ 0
f : ∫ (z : ℂ) in closedBall c r, 1 = ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), 1
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Tactic:
simp only [ENNReal.toReal_ofReal Real.two_pi_pos.le, ←
  intervalIntegral.integral_of_le rp, integral_const, Measure.restrict_apply, MeasurableSet.univ,
  univ_inter, Algebra.id.smul_eq_mul, mul_one, Real.volume_Ioc, tsub_zero,
  intervalIntegral.integral_mul_const, integral_id, zero_pow, Ne, bit0_eq_zero,
  Nat.one_ne_zero, not_false_iff] at f
Proof state after:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 / 2 * (2 * π)
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Theorem: Complex.volume_closedBall'
Proof state before:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 / 2 * (2 * π)
⊢ (↑volume (closedBall c r)).toReal = π * r ^ 2
Tactic:
ring_nf at f ⊢
Proof state after:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 * π
⊢ (↑volume (closedBall c r)).toReal = r ^ 2 * π
Theorem: Complex.volume_closedBall'
Proof state before:
c : ℂ
r : ℝ
rp : r ≥ 0
f : (↑volume (closedBall c r)).toReal = r ^ 2 * π
⊢ (↑volume (closedBall c r)).toReal = r ^ 2 * π
Tactic:
exact f
Proof state after:
no goals
Theorem: NiceVolume.closedBall
Proof state before:
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (Metric.closedBall c r) < ⊤
Tactic:
simp only [Complex.volume_closedBall]
Proof state after:
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 * ↑NNReal.pi < ⊤
Theorem: NiceVolume.closedBall
Proof state before:
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 * ↑NNReal.pi < ⊤
Tactic:
apply ENNReal.mul_lt_top
Proof state after:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 ≠ ⊤

case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑NNReal.pi ≠ ⊤
Theorem: NiceVolume.closedBall
Proof state before:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ENNReal.ofReal r ^ 2 ≠ ⊤
Tactic:
simp only [ne_eq, ENNReal.pow_eq_top_iff, ENNReal.ofReal_ne_top, OfNat.ofNat_ne_zero,
  not_false_eq_true, and_true]
Proof state after:
no goals
Theorem: NiceVolume.closedBall
Proof state before:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑NNReal.pi ≠ ⊤
Tactic:
simp only [ne_eq, ENNReal.coe_ne_top, not_false_eq_true]
Proof state after:
no goals
Theorem: NiceVolume.closedBall
Proof state before:
c : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (Metric.closedBall c r) > 0
Tactic:
simp only [Complex.volume_closedBall, gt_iff_lt, CanonicallyOrderedCommSemiring.mul_pos,
  ENNReal.coe_pos, NNReal.pi_pos, and_true]
Proof state after:
c : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r ^ 2
Theorem: NiceVolume.closedBall
Proof state before:
c : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r ^ 2
Tactic:
apply ENNReal.pow_pos
Proof state after:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r
Theorem: NiceVolume.closedBall
Proof state before:
case a
c : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r
Tactic:
bound
Proof state after:
no goals
Theorem: LocalVolume.closedBall
Proof state before:
c : ℂ
r : ℝ
rp : r > 0
⊢ LocalVolumeSet (Metric.closedBall c r)
Tactic:
apply LocalVolume.closure_interior
Proof state after:
case bp
c : ℂ
r : ℝ
rp : r > 0
⊢ ∀ (x : ℂ), ∀ r > 0, ↑volume (ball x r) > 0

case ci
c : ℂ
r : ℝ
rp : r > 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))
Theorem: LocalVolume.closedBall
Proof state before:
case bp
c : ℂ
r : ℝ
rp : r > 0
⊢ ∀ (x : ℂ), ∀ r > 0, ↑volume (ball x r) > 0
Tactic:
intro x r rp
Proof state after:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (ball x r) > 0
Theorem: LocalVolume.closedBall
Proof state before:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ ↑volume (ball x r) > 0
Tactic:
simp only [Complex.volume_ball, gt_iff_lt, CanonicallyOrderedCommSemiring.mul_pos,
  ENNReal.coe_pos, NNReal.pi_pos, and_true]
Proof state after:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r ^ 2
Theorem: LocalVolume.closedBall
Proof state before:
case bp
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r ^ 2
Tactic:
apply ENNReal.pow_pos
Proof state after:
case bp.a
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r
Theorem: LocalVolume.closedBall
Proof state before:
case bp.a
c : ℂ
r✝ : ℝ
rp✝ : r✝ > 0
x : ℂ
r : ℝ
rp : r > 0
⊢ 0 < ENNReal.ofReal r
Tactic:
bound
Proof state after:
no goals
Theorem: LocalVolume.closedBall
Proof state before:
case ci
c : ℂ
r : ℝ
rp : r > 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))
Tactic:
have rz := rp.ne'
Proof state after:
case ci
c : ℂ
r : ℝ
rp : r > 0
rz : r ≠ 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))
Theorem: LocalVolume.closedBall
Proof state before:
case ci
c : ℂ
r : ℝ
rp : r > 0
rz : r ≠ 0
⊢ Metric.closedBall c r ⊆ closure (interior (Metric.closedBall c r))
Tactic:
simp only [interior_closedBall c rz, closure_ball c rz, subset_refl]
Proof state after:
no goals
Theorem: approx_bad_potential_image
Proof state before:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ potential_image ↑c ∈ approx (bad_potential_image n r c)
Tactic:
rw [potential_image, bad_potential_image]
Proof state after:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)
Theorem: approx_bad_potential_image
Proof state before:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)
Tactic:
have e : ∀ p : ℝ, p^16 = (((p^2)^2)^2)^2 := by intro p; rw [←pow_mul, ←pow_mul, ←pow_mul]
Proof state after:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)
Theorem: approx_bad_potential_image
Proof state before:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)
Tactic:
simp only [far', outside', clear', green', e]
Proof state after:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat).quantize
Theorem: approx_bad_potential_image
Proof state before:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat).quantize
Tactic:
apply Color.mem_approx_quantize
Proof state after:
case cm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat)
Theorem: approx_bad_potential_image
Proof state before:
case cm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat)
Tactic:
apply mem_approx_lerp
Proof state after:
case cm.tm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr

case cm.xm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑clear ∈ approx clear.ofRat

case cm.ym
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑outside ∈ approx outside.ofRat
Theorem: approx_bad_potential_image
Proof state before:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
Tactic:
intro p
Proof state after:
c : ℚ × ℚ
n : ℕ
r : Floating
p : ℝ
⊢ p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
Theorem: approx_bad_potential_image
Proof state before:
c : ℚ × ℚ
n : ℕ
r : Floating
p : ℝ
⊢ p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
Tactic:
rw [←pow_mul, ←pow_mul, ←pow_mul]
Proof state after:
no goals
Theorem: approx_bad_potential_image
Proof state before:
case cm.tm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr
Tactic:
apply Interval.mem_approx_sqr
Proof state after:
case cm.tm.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ((potential 2 ↑↑c ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr
Theorem: approx_bad_potential_image
Proof state before:
case cm.tm.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ((potential 2 ↑↑c ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr
Tactic:
apply Interval.mem_approx_sqr
Proof state after:
case cm.tm.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (potential 2 ↑↑c ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr
Theorem: approx_bad_potential_image
Proof state before:
case cm.tm.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (potential 2 ↑↑c ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr
Tactic:
apply Interval.mem_approx_sqr
Proof state after:
case cm.tm.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr
Theorem: approx_bad_potential_image
Proof state before:
case cm.tm.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr
Tactic:
apply Interval.mem_approx_sqr
Proof state after:
case cm.tm.ax.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1
Theorem: approx_bad_potential_image
Proof state before:
case cm.tm.ax.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1
Tactic:
mono
Proof state after:
no goals
Theorem: approx_bad_potential_image
Proof state before:
case cm.xm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑clear ∈ approx clear.ofRat
Tactic:
mono
Proof state after:
no goals
Theorem: approx_bad_potential_image
Proof state before:
case cm.ym
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑outside ∈ approx outside.ofRat
Tactic:
mono
Proof state after:
no goals
Theorem: nontrivial_local_of_global
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
⊢ NontrivialHolomorphicAt f z
Tactic:
have fh : HolomorphicOn I I f (closedBall z r) := fun _ m ↦ (fa _ m).holomorphicAt I I
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
⊢ NontrivialHolomorphicAt f z
Theorem: nontrivial_local_of_global
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
⊢ NontrivialHolomorphicAt f z
Tactic:
have zs : z ∈ closedBall z r := mem_closedBall_self rp.le
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ NontrivialHolomorphicAt f z
Theorem: nontrivial_local_of_global
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ NontrivialHolomorphicAt f z
Tactic:
use fh _ zs
Proof state after:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
Theorem: nontrivial_local_of_global
Proof state before:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
ef : ∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
⊢ ∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
Tactic:
contrapose ef
Proof state after:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
Theorem: nontrivial_local_of_global
Proof state before:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ¬∃ᶠ (w : ℂ) in 𝓝 z, f w ≠ f z
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
Tactic:
simp only [Filter.not_frequently, not_not] at ef
Proof state after:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
Theorem: nontrivial_local_of_global
Proof state before:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ¬∀ w ∈ sphere z r, e ≤ ‖f w - f z‖
Tactic:
simp only [not_forall, not_le]
Proof state after:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ∃ x, ∃ (_ : x ∈ sphere z r), ‖f x - f z‖ < e
Theorem: nontrivial_local_of_global
Proof state before:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
⊢ ∃ x, ∃ (_ : x ∈ sphere z r), ‖f x - f z‖ < e
Tactic:
have zrs : z + r ∈ sphere z r := by
  simp only [mem_sphere, Complex.dist_eq, add_sub_cancel_left, Complex.abs_ofReal, abs_of_pos rp]
Proof state after:
case nonconst
X : Type
inst✝⁶ : TopologicalSpace X
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝³ : TopologicalSpace T
inst✝² : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹ : TopologicalSpace U
inst✝ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f : ℂ → ℂ
z : ℂ
e r : ℝ
fa : AnalyticOn ℂ f (closedBall z r)
rp : 0 < r
ep : 0 < e
fh : HolomorphicOn 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) f (closedBall z r)
zs : z ∈ closedBall z r
ef : ∀ᶠ (x : ℂ) in 𝓝 z, f x = f z
zrs : z + ↑r ∈ sphere z r
⊢ ∃ x, ∃ (_ : x ∈ sphere z r), ‖f x - f z‖ < e