internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.submean_disk
Proof state before:
case refine_2.hf
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Set.MapsTo (fun a => circleMap c a.1 a.2) (Icc (0, 0) (r, 2 * π)) (closedBall c r)
Tactic:
intro (a,b) ts
Proof state after:
case refine_2.hf
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (a, b) ∈ Icc (0, 0) (r, 2 * π)
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r
Theorem: SubharmonicOn.submean_disk
Proof state before:
case refine_2.hf
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (a, b) ∈ Icc (0, 0) (r, 2 * π)
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r
Tactic:
simp only [ge_iff_le, Prod.mk_le_mk, gt_iff_lt, zero_lt_two, mul_nonneg_iff_of_pos_left,
  not_and, not_le, Prod.mk_lt_mk, Set.mem_Icc] at ts
Proof state after:
case refine_2.hf
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (0 ≤ a ∧ 0 ≤ b) ∧ a ≤ r ∧ b ≤ 2 * π
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r
Theorem: SubharmonicOn.submean_disk
Proof state before:
case refine_2.hf
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
c : ℂ
r : ℝ
fs : SubharmonicOn f (closedBall c r)
rp : r > 0
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
a b : ℝ
ts : (0 ≤ a ∧ 0 ≤ b) ∧ a ≤ r ∧ b ≤ 2 * π
⊢ (fun a => circleMap c a.1 a.2) (a, b) ∈ closedBall c r
Tactic:
simp only [Metric.mem_closedBall, Complex.dist_eq, circleMap_sub_center, abs_circleMap_zero,
  abs_of_nonneg ts.1.1, ts.2.1]
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
m :
  (volume.restrict (Ioc 0 r)).ae.EventuallyLE (fun s => (2 * π * s) • f c) fun s =>
    s • ∫ (t : ℝ) in Ioc 0 (2 * π), f (circleMap c s t)
⊢ Continuous fun a => circleMap c a.1 a.2
Tactic:
continuity
Proof state after:
no goals
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
⊢ SubharmonicOn (fun z => Max.max (f z) (g z)) s
Tactic:
have pc : ContinuousOn (fun z ↦ (f z, g z)) s := fs.cont.prod gs.cont
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
⊢ SubharmonicOn (fun z => Max.max (f z) (g z)) s
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
⊢ SubharmonicOn (fun z => Max.max (f z) (g z)) s
Tactic:
have mc : ContinuousOn (fun z ↦ Max.max (f z) (g z)) s := continuous_max.comp_continuousOn pc
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
⊢ SubharmonicOn (fun z => Max.max (f z) (g z)) s
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
⊢ SubharmonicOn (fun z => Max.max (f z) (g z)) s
Tactic:
rw [subharmonicOn_iff_submean mc]
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
⊢ ∀ (c : ℂ),
    ∀ r > 0,
      closedBall c r ⊆ s → Max.max (f c) (g c) ≤ ⨍ (t : ℝ) in itau, Max.max (f (circleMap c r t)) (g (circleMap c r t))
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
⊢ ∀ (c : ℂ),
    ∀ r > 0,
      closedBall c r ⊆ s → Max.max (f c) (g c) ≤ ⨍ (t : ℝ) in itau, Max.max (f (circleMap c r t)) (g (circleMap c r t))
Tactic:
intro c r rp 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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ Max.max (f c) (g c) ≤ ⨍ (t : ℝ) in itau, Max.max (f (circleMap c r t)) (g (circleMap c r t))
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ Max.max (f c) (g c) ≤ ⨍ (t : ℝ) in itau, Max.max (f (circleMap c r t)) (g (circleMap c r t))
Tactic:
have pi : IntegrableOn (fun t ↦ (f (circleMap c r t), g (circleMap c r t))) itau := by
  refine ContinuousOn.integrableOn_sphere (f := fun z ↦ (f z, g z)) ?_ rp
  exact pc.mono 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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
⊢ Max.max (f c) (g c) ≤ ⨍ (t : ℝ) in itau, Max.max (f (circleMap c r t)) (g (circleMap c r t))
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
Tactic:
refine ContinuousOn.integrableOn_sphere (f := fun z ↦ (f z, g z)) ?_ rp
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ContinuousOn (fun z => (f z, g z)) (closedBall c r)
Theorem: SubharmonicOn.max
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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ ContinuousOn (fun z => (f z, g z)) (closedBall c r)
Tactic:
exact pc.mono cs
Proof state after:
no goals
Theorem: SubharmonicOn.max
Proof state before:
case refine_1
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
⊢ Max.max (f c) (g c) ≤
    Max.max (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).1
      (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).2
Tactic:
apply max_le_max
Proof state after:
case refine_1.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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
⊢ f c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).1

case refine_1.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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
⊢ g c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).2
Theorem: SubharmonicOn.max
Proof state before:
case refine_1.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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
⊢ f c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).1
Tactic:
have e : ∀ p : ℝ × ℝ, p.fst = ContinuousLinearMap.fst ℝ ℝ ℝ p := fun p ↦ by
  simp only [ContinuousLinearMap.fst, ContinuousLinearMap.coe_mk', LinearMap.fst_apply]
Proof state after:
case refine_1.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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
e : ∀ (p : ℝ × ℝ), p.1 = (ContinuousLinearMap.fst ℝ ℝ ℝ) p
⊢ f c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).1
Theorem: SubharmonicOn.max
Proof state before:
case refine_1.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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
e : ∀ (p : ℝ × ℝ), p.1 = (ContinuousLinearMap.fst ℝ ℝ ℝ) p
⊢ f c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).1
Tactic:
rw [e]
Proof state after:
case refine_1.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 g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
gs : SubharmonicOn g s
pc : ContinuousOn (fun z => (f z, g z)) s
mc : ContinuousOn (fun z => Max.max (f z) (g z)) s
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
pi : IntegrableOn (fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume
e : ∀ (p : ℝ × ℝ), p.1 = (ContinuousLinearMap.fst ℝ ℝ ℝ) p
⊢ f c ≤ (ContinuousLinearMap.fst ℝ ℝ ℝ) (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume)