internlm/Lean-Github huggingface dataset:
Theorem: HarmonicOn.const_mul
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 : ℂ → S
s : Set ℂ
fh : HarmonicOn f s
a : S
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ a * f c = ⨍ (t : ℝ) in itau, a * f (circleMap c r t)
Tactic:
rw [average_eq]
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 : ℂ → S
s : Set ℂ
fh : HarmonicOn f s
a : S
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ a * f c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, a * f (circleMap c r x)
Theorem: HarmonicOn.const_mul
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 : ℂ → S
s : Set ℂ
fh : HarmonicOn f s
a : S
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ a * f c = (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, a * f (circleMap c r x)
Tactic:
simp_rw [← smul_eq_mul, integral_smul, smul_comm _ a, ← average_eq, ← fh.mean c r rp cs]
Proof state after:
no goals
Theorem: SubharmonicOn.constMul
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
⊢ ∀ c ∈ interior s, ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
intro c cs
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Theorem: SubharmonicOn.constMul
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
rcases fs.submean' c cs with ⟨r, rp, rm⟩
Proof state after:
case intro.intro
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Theorem: SubharmonicOn.constMul
Proof state before:
case intro.intro
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
use r, rp
Proof state after:
case right
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Theorem: SubharmonicOn.constMul
Proof state before:
case right
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 : ℂ → ℝ
s : Set ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
intro s sp sr
Proof state after:
case right
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
s : ℝ
sp : 0 < s
sr : s < r
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Theorem: SubharmonicOn.constMul
Proof state before:
case right
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
s : ℝ
sp : 0 < s
sr : s < r
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
specialize rm s sp sr
Proof state after:
case right
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Theorem: SubharmonicOn.constMul
Proof state before:
case right
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  smul_eq_mul] at rm ⊢
Proof state after:
case right
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, a * f (circleMap c s t)
Theorem: SubharmonicOn.constMul
Proof state before:
case right
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
calc a * f c
  _ ≤ a * ((volume itau).toReal⁻¹ * ∫ t in itau, f (circleMap c s t)) := by bound
  _ = (volume itau).toReal⁻¹ * (a * ∫ t in itau, f (circleMap c s t)) := by ring
  _ = (volume itau).toReal⁻¹ * ∫ t in itau, a * f (circleMap c s t) := by
    rw [integral_mul_left]
Proof state after:
no goals
Theorem: SubharmonicOn.constMul
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ a * ((↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t))
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.constMul
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * ((↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)) =
    (↑volume itau).toReal⁻¹ * (a * ∫ (t : ℝ) in itau, f (circleMap c s t))
Tactic:
ring
Proof state after:
no goals
Theorem: SubharmonicOn.constMul
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 : ℂ → ℝ
s✝ : Set ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ (↑volume itau).toReal⁻¹ * (a * ∫ (t : ℝ) in itau, f (circleMap c s t)) =
    (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
rw [integral_mul_left]
Proof state after:
no goals
Theorem: AnalyticOn.circle_mean_eq
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 : ℂ → 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 ?_
Proof 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
Theorem: AnalyticOn.circle_mean_eq
Proof 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
Proof 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
Theorem: AnalyticOn.circle_mean_eq
Proof 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
Proof 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
Theorem: AnalyticOn.circle_mean_eq
Proof 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
Proof 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
Theorem: AnalyticOn.circle_mean_eq
Proof 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
Proof 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