internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.submean_disk
Proof 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]
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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]
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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]
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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)
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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
Theorem: SubharmonicOn.submean_disk
Proof 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']
Proof state after:
no goals
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof state after:
no goals
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof state after:
no goals
Theorem: SubharmonicOn.submean_disk
Proof 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']
Proof state after:
no goals
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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
Theorem: SubharmonicOn.submean_disk
Proof 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
Proof 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