internlm/Lean-Github huggingface dataset:
Theorem: HarmonicOn.convex
Proof state before:
case intro.intro.hfi
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ IntegrableOn (fun x => f (circleMap z t x)) itau volume

case intro.intro.hgi
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ IntegrableOn (g ∘ fun x => f (circleMap z t x)) itau volume
Tactic:
exact (fh.cont.mono cs).integrableOn_sphere tp
Proof state after:
case intro.intro.hgi
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ IntegrableOn (g ∘ fun x => f (circleMap z t x)) itau volume
Theorem: HarmonicOn.convex
Proof state before:
case intro.intro.hgi
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
r : ℝ
rp : r > 0
rh : ball z r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
cs : closedBall z t ⊆ s
n : NiceVolume itau
⊢ IntegrableOn (g ∘ fun x => f (circleMap z t x)) itau volume
Tactic:
exact ((c.comp_continuousOn fh.cont).mono cs).integrableOn_sphere tp
Proof state after:
no goals
Theorem: HarmonicOn.subharmonicOn
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 ℂ
h : HarmonicOn f s
⊢ SubharmonicOn (fun z => f z) s
Tactic:
have e : (fun z ↦ f z) = fun z ↦ (fun x ↦ x) (f z) := rfl
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 : ℂ → ℝ
s : Set ℂ
h : HarmonicOn f s
e : (fun z => f z) = fun z => (fun x => x) (f z)
⊢ SubharmonicOn (fun z => f z) s
Theorem: HarmonicOn.subharmonicOn
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 ℂ
h : HarmonicOn f s
e : (fun z => f z) = fun z => (fun x => x) (f z)
⊢ SubharmonicOn (fun z => f z) s
Tactic:
rw [e]
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 : ℂ → ℝ
s : Set ℂ
h : HarmonicOn f s
e : (fun z => f z) = fun z => (fun x => x) (f z)
⊢ SubharmonicOn (fun z => (fun x => x) (f z)) s
Theorem: HarmonicOn.subharmonicOn
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 ℂ
h : HarmonicOn f s
e : (fun z => f z) = fun z => (fun x => x) (f z)
⊢ SubharmonicOn (fun z => (fun x => x) (f z)) s
Tactic:
exact h.convex continuous_id (convexOn_id convex_univ)
Proof state after:
no goals
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
⊢ ∀ c ∈ interior s, ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Tactic:
intro c 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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Theorem: SubharmonicOn.congr
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
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior c cs with ⟨r0, r0p, r0s⟩
Proof state after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Tactic:
rcases fs.submean' c cs with ⟨r1, r1p, sm⟩
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Tactic:
have r01p : min r0 r1 > 0 := by bound
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Tactic:
exists min r0 r1, r01p
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
⊢ ∀ (s : ℝ), 0 < s → s < min r0 r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
⊢ ∀ (s : ℝ), 0 < s → s < min r0 r1 → g c ≤ ⨍ (t : ℝ) in itau, g (circleMap c s t)
Tactic:
intro t tp tr
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
⊢ g c ≤ ⨍ (t_1 : ℝ) in itau, g (circleMap c t t_1)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
sm : ∀ (s : ℝ), 0 < s → s < r1 → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
⊢ g c ≤ ⨍ (t_1 : ℝ) in itau, g (circleMap c t t_1)
Tactic:
specialize sm t tp (lt_of_lt_of_le tr (by bound))
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ g c ≤ ⨍ (t_1 : ℝ) in itau, g (circleMap c t t_1)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
⊢ g c ≤ ⨍ (t_1 : ℝ) in itau, g (circleMap c t t_1)
Tactic:
have hs : (fun u ↦ f (circleMap c t u)) =ᵐ[volume.restrict itau]
    fun u ↦ g (circleMap c t u) := by
  rw [Filter.EventuallyEq]; rw [ae_restrict_iff' measurableSet_itau]
  apply Filter.eventually_of_forall
  intro u _; apply h.symm
  apply _root_.trans r0s interior_subset
  simp only [Metric.mem_ball, Complex.dist_eq, circleMap_sub_center, abs_circleMap_zero,
    abs_of_pos tp]
  exact lt_of_lt_of_le tr (by bound)
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
hs : (volume.restrict itau).ae.EventuallyEq (fun u => f (circleMap c t u)) fun u => g (circleMap c t u)
⊢ g c ≤ ⨍ (t_1 : ℝ) in itau, g (circleMap c t t_1)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
hs : (volume.restrict itau).ae.EventuallyEq (fun u => f (circleMap c t u)) fun u => g (circleMap c t u)
⊢ g c ≤ ⨍ (t_1 : ℝ) in itau, g (circleMap c t t_1)
Tactic:
rw [average_eq] at sm ⊢
Proof state after:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
hs : (volume.restrict itau).ae.EventuallyEq (fun u => f (circleMap c t u)) fun u => g (circleMap c t u)
⊢ g c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, g (circleMap c t x)
Theorem: SubharmonicOn.congr
Proof state before:
case intro.intro.intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f g : ℂ → ℝ
s : Set ℂ
fs : SubharmonicOn f s
h : Set.EqOn g f s
c : ℂ
cs : c ∈ interior s
r0 : ℝ
r0p : r0 > 0
r0s : ball c r0 ⊆ interior s
r1 : ℝ
r1p : 0 < r1
r01p : min r0 r1 > 0
t : ℝ
tp : 0 < t
tr : t < min r0 r1
sm : f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
hs : (volume.restrict itau).ae.EventuallyEq (fun u => f (circleMap c t u)) fun u => g (circleMap c t u)
⊢ g c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, g (circleMap c t x)
Tactic:
rwa [← h.symm (interior_subset cs), ← integral_congr_ae hs]
Proof state after:
no goals