Theorem: SubharmonicOn.max (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 : ℂ → ℝ
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
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

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
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

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]
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))

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
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))

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
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))

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 ?_)
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

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
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)

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
State after:
no goals

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
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

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]
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

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]
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)

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 ≤ (ContinuousLinearMap.fst ℝ ℝ ℝ) (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume)
Tactic:
rw [← average_linear_comm pi]
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, (ContinuousLinearMap.fst ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))

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, (ContinuousLinearMap.fst ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))
Tactic:
simp only [ContinuousLinearMap.fst, ContinuousLinearMap.coe_mk', LinearMap.fst_apply]
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)

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)
Tactic:
exact (fs.mono cs).submean rp
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 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
p : ℝ × ℝ
⊢ p.1 = (ContinuousLinearMap.fst ℝ ℝ ℝ) p
Tactic:
simp only [ContinuousLinearMap.fst, ContinuousLinearMap.coe_mk', LinearMap.fst_apply]
State after:
no goals

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
⊢ g c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).2
Tactic:
have e : ∀ p : ℝ × ℝ, p.snd = ContinuousLinearMap.snd ℝ ℝ ℝ p := fun p ↦ by
  simp only [ContinuousLinearMap.snd, ContinuousLinearMap.coe_mk', LinearMap.snd_apply]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).2

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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume).2
Tactic:
rw [e]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ (ContinuousLinearMap.snd ℝ ℝ ℝ) (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume)

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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ (ContinuousLinearMap.snd ℝ ℝ ℝ) (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume)
Tactic:
rw [← average_linear_comm pi]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, (ContinuousLinearMap.snd ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))

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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, (ContinuousLinearMap.snd ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))
Tactic:
simp only [ContinuousLinearMap.snd, ContinuousLinearMap.coe_mk', LinearMap.snd_apply]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, g (circleMap c r x)

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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, g (circleMap c r x)
Tactic:
exact (gs.mono cs).submean rp
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 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
p : ℝ × ℝ
⊢ p.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
Tactic:
simp only [ContinuousLinearMap.snd, ContinuousLinearMap.coe_mk', LinearMap.snd_apply]
State after:
no goals

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 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
Tactic:
simp only [Ne, Measure.restrict_eq_zero]
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 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

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 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
Tactic:
exact NiceVolume.itau.ne_zero
State after:
no goals

State before:
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 ≠ ⊤
Tactic:
exact NiceVolume.itau.ne_top
State after:
no goals

State before:
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
Tactic:
simp only [Set.mem_univ, Filter.eventually_true]
State after:
no goals

State before:
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
Tactic:
exact (mc.mono cs).integrableOn_sphere rp
State after:
no goals