internlm/Lean-Github huggingface dataset:
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 ≤ (ContinuousLinearMap.fst ℝ ℝ ℝ) (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume)
Tactic:
rw [← average_linear_comm pi]
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, (ContinuousLinearMap.fst ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))
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, (ContinuousLinearMap.fst ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))
Tactic:
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)
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)
Tactic:
exact (fs.mono cs).submean rp
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
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]
Proof state after:
no goals
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
⊢ 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]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ 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
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]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ (ContinuousLinearMap.snd ℝ ℝ ℝ) (⨍ (x : ℝ) in itau, (f (circleMap c r x), g (circleMap c r x)) ∂volume)
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.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]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, (ContinuousLinearMap.snd ℝ ℝ ℝ) (f (circleMap c r x), g (circleMap c r x))
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.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]
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, g (circleMap c r x)
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.2 = (ContinuousLinearMap.snd ℝ ℝ ℝ) p
⊢ g c ≤ ⨍ (x : ℝ) in itau, g (circleMap c r x)
Tactic:
exact (gs.mono cs).submean rp
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
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]
Proof state after:
no goals
Theorem: SubharmonicOn.max
Proof 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]
Proof 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
Theorem: SubharmonicOn.max
Proof 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
Proof state after:
no goals
Theorem: SubharmonicOn.max
Proof 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
Proof state after:
no goals
Theorem: SubharmonicOn.max
Proof 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]
Proof state after:
no goals
Theorem: SubharmonicOn.max
Proof 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
Proof state after:
no goals
Theorem: SubharmonicOn.partialSups
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
n : ℕ
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n) s
Tactic:
induction' n with n h
Proof state after:
case zero
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) 0) s

case succ
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 : ℕ → ℂ → ℝ
s : Set ℂ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
n : ℕ
h : SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) n) s
⊢ SubharmonicOn (fun z => (_root_.partialSups fun k => f k z) (n + 1)) s