Theorem: SubharmonicOn.submean_disk (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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ ⨍ (z : ℂ) in closedBall c r, f z
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul]
State after:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (↑volume (closedBall c r)).toReal⁻¹ * ∫ (z : ℂ) in closedBall c r, f z

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (↑volume (closedBall c r)).toReal⁻¹ * ∫ (z : ℂ) in closedBall c r, f z
Tactic:
rw [Complex.volume_closedBall' rp.le, fubini_ball fs.cont]
State after:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have m : (fun s ↦ (2 * π * s) • f c) ≤ᵐ[volume.restrict (Ioc 0 r)] fun s ↦
    s • ∫ t : ℝ in Set.Ioc 0 (2 * π), f (circleMap c s t) := by
  rw [Filter.EventuallyLE]; rw [ae_restrict_iff' measurableSet_Ioc]; apply ae_of_all; intro s sr
  simp only [Set.mem_Ioc] at sr
  have e := (fs.mono (Metric.closedBall_subset_closedBall sr.2)).submean sr.1
  rw [smul_eq_mul, ← itau]
  simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
    itau_real_volume, smul_eq_mul] at e
  generalize hi : ∫ t in itau, f (circleMap c s t) = i
  rw [hi] at e
  calc 2 * π * s * f c
    _ ≤ 2 * π * s * ((2 * π)⁻¹ * i) := by bound
    _ = s * (2 * π * (2 * π)⁻¹) * i := by ring_nf
    _ ≤ s * i := by field_simp [Real.two_pi_pos.ne']
State after:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have im := integral_mono_ae ?_ ?_ m
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ ∫ (a : ℝ) in Ioc 0 r, a • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c a t)
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Integrable (fun s => (2 * π * s) • f c) (volume.restrict (Ioc 0 r))

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Integrable (fun s => s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)) (volume.restrict (Ioc 0 r))

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [Filter.EventuallyLE]
State after:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc 0 r), (2 * π * x) • f c ≤ x • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c x t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict (Ioc 0 r), (2 * π * x) • f c ≤ x • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c x t)
Tactic:
rw [ae_restrict_iff' measurableSet_Ioc]
State after:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 r → (2 * π * x) • f c ≤ x • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c x t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc 0 r → (2 * π * x) • f c ≤ x • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c x t)
Tactic:
apply ae_of_all
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ ∀ a ∈ Ioc 0 r, (2 * π * a) • f c ≤ a • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c a t)

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
⊢ ∀ a ∈ Ioc 0 r, (2 * π * a) • f c ≤ a • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c a t)
Tactic:
intro s sr
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : s ∈ Ioc 0 r
⊢ (2 * π * s) • f c ≤ s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : s ∈ Ioc 0 r
⊢ (2 * π * s) • f c ≤ s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
simp only [Set.mem_Ioc] at sr
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
⊢ (2 * π * s) • f c ≤ s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
⊢ (2 * π * s) • f c ≤ s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
have e := (fs.mono (Metric.closedBall_subset_closedBall sr.2)).submean sr.1
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ (2 * π * s) • f c ≤ s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ (2 * π * s) • f c ≤ s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
rw [smul_eq_mul, ← itau]
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ 2 * π * s * f c ≤ s • ∫ (t : ℝ) in itau, f (circleMap c s t)

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ 2 * π * s * f c ≤ s • ∫ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  itau_real_volume, smul_eq_mul] at e
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ (2 * π)⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ 2 * π * s * f c ≤ s • ∫ (t : ℝ) in itau, f (circleMap c s t)

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ (2 * π)⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ 2 * π * s * f c ≤ s • ∫ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
generalize hi : ∫ t in itau, f (circleMap c s t) = i
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ (2 * π)⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
i : ℝ
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ 2 * π * s * f c ≤ s • i

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
e : f c ≤ (2 * π)⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
i : ℝ
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ 2 * π * s * f c ≤ s • i
Tactic:
rw [hi] at e
State after:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
i : ℝ
e : f c ≤ (2 * π)⁻¹ * i
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ 2 * π * s * f c ≤ s • i

State before:
case a
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
i : ℝ
e : f c ≤ (2 * π)⁻¹ * i
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ 2 * π * s * f c ≤ s • i
Tactic:
calc 2 * π * s * f c
  _ ≤ 2 * π * s * ((2 * π)⁻¹ * i) := by bound
  _ = s * (2 * π * (2 * π)⁻¹) * i := by ring_nf
  _ ≤ s * i := by field_simp [Real.two_pi_pos.ne']
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
i : ℝ
e : f c ≤ (2 * π)⁻¹ * i
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ 2 * π * s * f c ≤ 2 * π * s * ((2 * π)⁻¹ * i)
Tactic:
bound
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
i : ℝ
e : f c ≤ (2 * π)⁻¹ * i
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ 2 * π * s * ((2 * π)⁻¹ * i) = s * (2 * π * (2 * π)⁻¹) * i
Tactic:
ring_nf
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
s : ℝ
sr : 0 < s ∧ s ≤ r
i : ℝ
e : f c ≤ (2 * π)⁻¹ * i
hi : ∫ (t : ℝ) in itau, f (circleMap c s t) = i
⊢ s * (2 * π * (2 * π)⁻¹) * i ≤ s * i
Tactic:
field_simp [Real.two_pi_pos.ne']
State after:
no goals

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ ∫ (a : ℝ) in Ioc 0 r, a • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c a t)
⊢ f c ≤ (π * r ^ 2)⁻¹ * ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
Tactic:
generalize hi : ∫ s in Ioc 0 r, s • ∫ t in Ioc 0 (2 * π), f (circleMap c s t) = i
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ ∫ (a : ℝ) in Ioc 0 r, a • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c a t)
i : ℝ
hi : ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t) = i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ ∫ (a : ℝ) in Ioc 0 r, a • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c a t)
i : ℝ
hi : ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t) = i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i
Tactic:
rw [hi] at im
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
i : ℝ
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ i
hi : ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t) = i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
i : ℝ
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ i
hi : ∫ (s : ℝ) in Ioc 0 r, s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t) = i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i
Tactic:
clear hi m
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : ∫ (a : ℝ) in Ioc 0 r, (2 * π * a) • f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i
Tactic:
simp only [← intervalIntegral.integral_of_le rp.le, Algebra.id.smul_eq_mul,
  intervalIntegral.integral_mul_const, intervalIntegral.integral_const_mul, integral_id,
  zero_pow, Ne, bit0_eq_zero, Nat.one_ne_zero, not_false_iff, tsub_zero] at im
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : (∫ (x : ℝ) in 0 ..r, 2 * π * x) * f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : (∫ (x : ℝ) in 0 ..r, 2 * π * x) * f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i
Tactic:
rw [intervalIntegral.integral_const_mul] at im
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : (2 * π * ∫ (x : ℝ) in 0 ..r, x) * f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : (2 * π * ∫ (x : ℝ) in 0 ..r, x) * f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i
Tactic:
simp only [integral_id, ne_eq, zero_pow, sub_zero] at im
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : 2 * π * ((r ^ 2 - 0 ^ 2) / 2) * f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : 2 * π * ((r ^ 2 - 0 ^ 2) / 2) * f c ≤ i
⊢ f c ≤ (π * r ^ 2)⁻¹ * i
Tactic:
ring_nf at im ⊢
State after:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : π * r ^ 2 * f c ≤ i
⊢ f c ≤ π⁻¹ * r⁻¹ ^ 2 * i

State before:
case refine_3
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : π * r ^ 2 * f c ≤ i
⊢ f c ≤ π⁻¹ * r⁻¹ ^ 2 * i
Tactic:
calc f c
  _ = π⁻¹ * r⁻¹^2 * (π * r^2 * f c) := by ring_nf; field_simp [rp.ne', Real.pi_pos.ne']
  _ ≤ π⁻¹ * r⁻¹^2 * i := by bound
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : π * r ^ 2 * f c ≤ i
⊢ f c = π⁻¹ * r⁻¹ ^ 2 * (π * r ^ 2 * f c)
Tactic:
ring_nf
State after:
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : π * r ^ 2 * f c ≤ i
⊢ f c = π * π⁻¹ * r ^ 2 * r⁻¹ ^ 2 * f c

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : π * r ^ 2 * f c ≤ i
⊢ f c = π * π⁻¹ * r ^ 2 * r⁻¹ ^ 2 * f c
Tactic:
field_simp [rp.ne', Real.pi_pos.ne']
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
i : ℝ
im : π * r ^ 2 * f c ≤ i
⊢ π⁻¹ * r⁻¹ ^ 2 * (π * r ^ 2 * f c) ≤ π⁻¹ * r⁻¹ ^ 2 * i
Tactic:
bound
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Integrable (fun s => (2 * π * s) • f c) (volume.restrict (Ioc 0 r))
Tactic:
apply Continuous.integrableOn_Ioc
State after:
case refine_1.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Continuous fun s => (2 * π * s) • f c

State before:
case refine_1.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Continuous fun s => (2 * π * s) • f c
Tactic:
continuity
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Integrable (fun s => s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)) (volume.restrict (Ioc 0 r))
Tactic:
refine IntegrableOn.mono_set ?_ Set.Ioc_subset_Icc_self
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ IntegrableOn (fun s => s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)) (Icc 0 r) volume

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ IntegrableOn (fun s => s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)) (Icc 0 r) volume
Tactic:
apply ContinuousOn.integrableOn_Icc
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (fun s => s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)) (Icc 0 r)

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (fun s => s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)) (Icc 0 r)
Tactic:
apply ContinuousOn.smul continuousOn_id
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c x t)) (Icc 0 r)

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c x t)) (Icc 0 r)
Tactic:
simp_rw [← intervalIntegral.integral_of_le Real.two_pi_pos.le]
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in 0 ..2 * π, f (circleMap c x t)) (Icc 0 r)

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in 0 ..2 * π, f (circleMap c x t)) (Icc 0 r)
Tactic:
refine ContinuousOn.intervalIntegral ?_ isCompact_Icc Real.two_pi_pos.le
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (uncurry fun x t => f (circleMap c x t)) (Icc 0 r ×ˢ Icc 0 (2 * π))

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (uncurry fun x t => f (circleMap c x t)) (Icc 0 r ×ˢ Icc 0 (2 * π))
Tactic:
simp only [uncurry, Set.Icc_prod_Icc]
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (uncurry fun x t => f (circleMap c x t)) (Icc (0, 0) (r, 2 * π))

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ ContinuousOn (uncurry fun x t => f (circleMap c x t)) (Icc (0, 0) (r, 2 * π))
Tactic:
refine fs.cont.comp (Continuous.continuousOn (by continuity)) ?_
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Set.MapsTo (fun a => circleMap c a.1 a.2) (Icc (0, 0) (r, 2 * π)) (closedBall c r)

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Set.MapsTo (fun a => circleMap c a.1 a.2) (Icc (0, 0) (r, 2 * π)) (closedBall c r)
Tactic:
intro (a,b) ts
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (a, b) ∈ Icc (0, 0) (r, 2 * π)
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (a, b) ∈ Icc (0, 0) (r, 2 * π)
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r
Tactic:
simp only [ge_iff_le, Prod.mk_le_mk, gt_iff_lt, zero_lt_two, mul_nonneg_iff_of_pos_left,
  not_and, not_le, Prod.mk_lt_mk, Set.mem_Icc] at ts
State after:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (0 ≤ a ∧ 0 ≤ b) ∧ a ≤ r ∧ b ≤ 2 * π
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r

State before:
case refine_2.hf
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (0 ≤ a ∧ 0 ≤ b) ∧ a ≤ r ∧ b ≤ 2 * π
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r
Tactic:
simp only [Metric.mem_closedBall, Complex.dist_eq, circleMap_sub_center, abs_circleMap_zero,
  abs_of_nonneg ts.1.1, ts.2.1]
State after:
no goals

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Continuous fun a => circleMap c a.1 a.2
Tactic:
continuity
State after:
no goals