Theorem: HarmonicOn.sub (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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
⊢ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → (f - g) c = ⨍ (t : ℝ) in itau, (f - g) (circleMap c r t)
Tactic:
intro c r rp cs
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (f - g) c = ⨍ (t : ℝ) in itau, (f - g) (circleMap c r 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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (f - g) c = ⨍ (t : ℝ) in itau, (f - g) (circleMap c r t)
Tactic:
simp [fh.mean c r rp cs, gh.mean c r rp cs]
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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (⨍ (t : ℝ) in itau, f (circleMap c r t)) - ⨍ (t : ℝ) in itau, g (circleMap c r t) =
    ⨍ (t : ℝ) in itau, f (circleMap c r t) - g (circleMap c r 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 g : ℂ → E
s : Set ℂ
fh : HarmonicOn f s
gh : HarmonicOn g s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ (⨍ (t : ℝ) in itau, f (circleMap c r t)) - ⨍ (t : ℝ) in itau, g (circleMap c r t) =
    ⨍ (t : ℝ) in itau, f (circleMap c r t) - g (circleMap c r t)
Tactic:
rw [Average.sub ((fh.cont.mono cs).integrableOn_sphere rp)
  ((gh.cont.mono cs).integrableOn_sphere rp)]
State after:
no goals