Theorem: AnalyticOn.circle_mean_eq (Ray/Hartogs/Subharmonic.lean)

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c
Tactic:
have h := Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
  Set.countable_empty (Metric.mem_ball_self rp) fa.continuousOn ?_
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c

case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
⊢ ∀ x ∈ ball c r \ ∅, DifferentiableAt ℂ f x

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • f z) = (2 * ↑π * I) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c
Tactic:
simp_rw [circleIntegral, deriv_circleMap, circleMap_sub_center, smul_smul, mul_comm _ I] at h
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (θ : ℝ) in 0 ..2 * π, (I * circleMap 0 r θ * (circleMap 0 r θ)⁻¹) • f (circleMap c r θ) = (I * (2 * ↑π)) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (θ : ℝ) in 0 ..2 * π, (I * circleMap 0 r θ * (circleMap 0 r θ)⁻¹) • f (circleMap c r θ) = (I * (2 * ↑π)) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c
Tactic:
field_simp [circleMap_ne_center rp.ne'] at h
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : I • ∫ (x : ℝ) in 0 ..2 * π, f (circleMap c r x) = (I * (2 * ↑π)) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : I • ∫ (x : ℝ) in 0 ..2 * π, f (circleMap c r x) = (I * (2 * ↑π)) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c
Tactic:
rw [← smul_smul, IsUnit.smul_left_cancel (Ne.isUnit Complex.I_ne_zero)] at h
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in 0 ..2 * π, f (circleMap c r x) = (2 * ↑π) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in 0 ..2 * π, f (circleMap c r x) = (2 * ↑π) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c
Tactic:
rw [intervalIntegral.integral_of_le Real.two_pi_pos.le] at h
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ ⨍ (t : ℝ) in itau, f (circleMap c r t) = f c
Tactic:
rw [average_eq, itau, h]
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (↑(volume.restrict (Ioc 0 (2 * π))) univ).toReal⁻¹ • (2 * ↑π) • f c = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (↑(volume.restrict (Ioc 0 (2 * π))) univ).toReal⁻¹ • (2 * ↑π) • f c = f c
Tactic:
simp only [gt_iff_lt, zero_lt_two, mul_pos_iff_of_pos_left, not_lt, ge_iff_le, MeasurableSet.univ,
  Measure.restrict_apply, Set.univ_inter, Real.volume_Ioc, sub_zero, mul_nonneg_iff_of_pos_left]
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (ENNReal.ofReal (2 * π)).toReal⁻¹ • (2 * ↑π) • f c = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (ENNReal.ofReal (2 * π)).toReal⁻¹ • (2 * ↑π) • f c = f c
Tactic:
rw [ENNReal.toReal_ofReal Real.two_pi_pos.le]
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (2 * π)⁻¹ • (2 * ↑π) • f c = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (2 * π)⁻¹ • (2 * ↑π) • f c = f c
Tactic:
rw [← smul_assoc, Complex.real_smul]
State after:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (↑(2 * π)⁻¹ * (2 * ↑π)) • f c = f c

State before:
case refine_2
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
h : ∫ (x : ℝ) in Ioc 0 (2 * π), f (circleMap c r x) ∂volume = (2 * ↑π) • f c
⊢ (↑(2 * π)⁻¹ * (2 * ↑π)) • f c = f c
Tactic:
field_simp [Real.pi_ne_zero]
State after:
no goals

State before:
case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
⊢ ∀ x ∈ ball c r \ ∅, DifferentiableAt ℂ f x
Tactic:
intro z zs
State after:
case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
z : ℂ
zs : z ∈ ball c r \ ∅
⊢ DifferentiableAt ℂ f z

State before:
case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
z : ℂ
zs : z ∈ ball c r \ ∅
⊢ DifferentiableAt ℂ f z
Tactic:
rw [Set.diff_empty] at zs
State after:
case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
z : ℂ
zs : z ∈ ball c r
⊢ DifferentiableAt ℂ f z

State before:
case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → H
c : ℂ
r : ℝ
fa : AnalyticOn ℂ f (closedBall c r)
rp : r > 0
z : ℂ
zs : z ∈ ball c r
⊢ DifferentiableAt ℂ f z
Tactic:
exact (fa z (Metric.ball_subset_closedBall zs)).differentiableAt
State after:
no goals