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
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))
Tactic:
refine _root_.trans ?_ (ConvexOn.map_set_average_le convexOn_max continuous_max.continuousOn
    isClosed_univ ?_ ?_ ?_ pi ?_)
Proof state after:
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

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 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
⊢ ↑volume itau ≠ 0

case refine_3
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f 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
⊢ ↑volume itau ≠ ⊤

case refine_4
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
⊢ ∀ᵐ (x : ℝ) ∂volume.restrict itau, (f (circleMap c r x), g (circleMap c r x)) ∈ univ

case refine_5
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
⊢ IntegrableOn ((fun p => Max.max p.1 p.2) ∘ fun t => (f (circleMap c r t), g (circleMap c r t))) itau volume