Theorem: SubharmonicOn.submean (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 ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
rcases continuous_to_harmonic_real (fs.cont.mono Metric.sphere_subset_closedBall) with ⟨g, gh, fg⟩
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
generalize hd : (fun z ↦ f z - g z) = d
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have ds : SubharmonicOn d (closedBall c r) := by rw [← hd]; apply fs.add gh.neg.subharmonicOn
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have dz : ∀ z, z ∈ sphere c r → d z = 0 := by intro z zs; rw [← hd]; simp only [fg z zs, sub_self]
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have dz' : ∀ᵐ t, t ∈ itau → d (circleMap c r t) = 0 := by
  apply ae_of_all; intro t _; apply dz
  simp only [mem_sphere_iff_norm, circleMap_sub_center, Complex.norm_eq_abs, abs_circleMap_zero,
    abs_eq_self]
  linarith
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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
rcases ds.maximum_principle (isCompact_closedBall _ _) ⟨c, Metric.mem_closedBall_self rp.le⟩
  with ⟨w, wf, wm⟩
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ frontier (closedBall c r)
wm : IsMaxOn d (closedBall c r) w
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ frontier (closedBall c r)
wm : IsMaxOn d (closedBall c r) w
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
rw [frontier_closedBall _ rp.ne'] at wf
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have fd : f = fun z ↦ d z + g z := by funext z; rw [← hd]; simp only [sub_add_cancel]
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
simp_rw [fd, Average.add (ds.cont.integrableOn_sphere rp) (gh.cont.integrableOn_sphere rp)]
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c + g c ≤ (⨍ (z : ℝ) in itau, d (circleMap c r z)) + ⨍ (z : ℝ) in itau, g (circleMap c r z)

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c + g c ≤ (⨍ (z : ℝ) in itau, d (circleMap c r z)) + ⨍ (z : ℝ) in itau, g (circleMap c r z)
Tactic:
simp only [← gh.mean c r rp (subset_refl _), add_le_add_iff_right]
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c ≤ ⨍ (z : ℝ) in itau, d (circleMap c r z)

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c ≤ ⨍ (z : ℝ) in itau, d (circleMap c r z)
Tactic:
simp only [average_congr_on NiceVolume.itau dz', average_zero]
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c ≤ 0

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c ≤ 0
Tactic:
rw [← dz w wf]
State after:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c ≤ d w

State before:
case intro.intro.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 : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
fd : f = fun z => d z + g z
⊢ d c ≤ d w
Tactic:
apply wm (Metric.mem_closedBall_self rp.le)
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
⊢ SubharmonicOn d (closedBall c r)
Tactic:
rw [← hd]
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
⊢ SubharmonicOn (fun z => f z - g z) (closedBall c 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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
⊢ SubharmonicOn (fun z => f z - g z) (closedBall c r)
Tactic:
apply fs.add gh.neg.subharmonicOn
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
⊢ ∀ z ∈ sphere c r, d z = 0
Tactic:
intro z zs
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
z : ℂ
zs : z ∈ sphere c r
⊢ d z = 0

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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
z : ℂ
zs : z ∈ sphere c r
⊢ d z = 0
Tactic:
rw [← hd]
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
z : ℂ
zs : z ∈ sphere c r
⊢ (fun z => f z - g z) z = 0

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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
z : ℂ
zs : z ∈ sphere c r
⊢ (fun z => f z - g z) z = 0
Tactic:
simp only [fg z zs, sub_self]
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
⊢ ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
⊢ ∀ a ∈ itau, d (circleMap c r a) = 0

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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
⊢ ∀ a ∈ itau, d (circleMap c r a) = 0
Tactic:
intro t _
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
t : ℝ
a✝ : t ∈ itau
⊢ d (circleMap c r t) = 0

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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
t : ℝ
a✝ : t ∈ itau
⊢ d (circleMap c r t) = 0
Tactic:
apply dz
State after:
case a.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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
t : ℝ
a✝ : t ∈ itau
⊢ circleMap c r t ∈ sphere c r

State before:
case a.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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
t : ℝ
a✝ : t ∈ itau
⊢ circleMap c r t ∈ sphere c r
Tactic:
simp only [mem_sphere_iff_norm, circleMap_sub_center, Complex.norm_eq_abs, abs_circleMap_zero,
  abs_eq_self]
State after:
case a.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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
t : ℝ
a✝ : t ∈ itau
⊢ 0 ≤ r

State before:
case a.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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
t : ℝ
a✝ : t ∈ itau
⊢ 0 ≤ r
Tactic:
linarith
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
⊢ f = fun z => d z + g z
Tactic:
funext z
State after:
case h
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = d z + g z

State before:
case h
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = d z + g z
Tactic:
rw [← hd]
State after:
case h
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = (fun z => f z - g z) z + g z

State before:
case h
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
g : ℂ → ℝ
gh : HarmonicOn g (closedBall c r)
fg : ∀ z ∈ sphere c r, f z = g z
d : ℂ → ℝ
hd : (fun z => f z - g z) = d
ds : SubharmonicOn d (closedBall c r)
dz : ∀ z ∈ sphere c r, d z = 0
dz' : ∀ᵐ (t : ℝ), t ∈ itau → d (circleMap c r t) = 0
w : ℂ
wf : w ∈ sphere c r
wm : IsMaxOn d (closedBall c r) w
z : ℂ
⊢ f z = (fun z => f z - g z) z + g z
Tactic:
simp only [sub_add_cancel]
State after:
no goals