internlm/Lean-Github huggingface dataset:
Theorem: SubharmonicOn.hartogs
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb✝ : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
n : ℕ
fb : f n z ≤ b - d.toReal
⊢ g n z = ENNReal.ofReal (b - f n z)
Tactic:
simp only [← hg, ← hf', neg_sub]
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb✝ : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
n : ℕ
fb : f n z ≤ b - d.toReal
⊢ ENNReal.ofReal (b - f n z) ≥ ENNReal.ofReal (b - (b - d.toReal))
Tactic:
bound
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb✝ : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
n : ℕ
fb : f n z ≤ b - d.toReal
⊢ ENNReal.ofReal (b - (b - d.toReal)) = ENNReal.ofReal d.toReal
Tactic:
ring_nf
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb✝ : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
z : ℂ
zs : z ∈ interior s
fc : ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
d : ℝ≥0∞
dc : d < ENNReal.ofReal (b - c)
df : d ≠ ⊤
dc' : b - d.toReal > c
n : ℕ
fb : f n z ≤ b - d.toReal
⊢ ENNReal.ofReal d.toReal = d
Tactic:
rw [ENNReal.ofReal_toReal df]
Proof state after:
no goals
Theorem: SubharmonicOn.hartogs
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
⊢ ENNReal.ofReal (b - d) < ENNReal.ofReal (b - c)
Tactic:
rw [ENNReal.ofReal_lt_ofReal_iff (sub_pos.mpr bc)]
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
⊢ b - d < b - c
Theorem: SubharmonicOn.hartogs
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 k : Set ℂ
c b : ℝ
fs : ∀ (n : ℕ), SubharmonicOn (f n) s
fb : ∀ (n : ℕ), ∀ z ∈ s, f n z ≤ b
fc : ∀ z ∈ s, ∀ d > c, ∀ᶠ (n : ℕ) in atTop, f n z ≤ d
ck : IsCompact k
ks : k ⊆ interior s
bc : c < b
f' : ℕ → ℂ → ℝ
hf' : (fun n z => f n z - b) = f'
g : ℕ → ℂ → ℝ≥0∞
hg : (fun n z => ENNReal.ofReal (-f' n z)) = g
fs' : ∀ (n : ℕ), SubharmonicOn (f' n) s
fn' : ∀ (n : ℕ), ∀ z ∈ interior s, f' n z ≤ 0
gs : ∀ (n : ℕ), SuperharmonicOn (g n) (interior s)
gc : ∀ z ∈ interior s, liminf (fun n => g n z) atTop ≥ ENNReal.ofReal (b - c)
ks' : k ⊆ interior (interior s)
h : ∀ d < ENNReal.ofReal (b - c), ∀ᶠ (n : ℕ) in atTop, ∀ z ∈ k, g n z ≥ d
d : ℝ
dc : d > c
⊢ b - d < b - c
Tactic:
simpa only [sub_lt_sub_iff_left]
Proof state after:
no goals
Theorem: max_exp_pos
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ 0 < max b.exp x
Tactic:
bound
Proof state after:
no goals
Theorem: le_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ b ≤ maxLog b x
Tactic:
rw [maxLog, Real.le_log_iff_exp_le max_exp_pos]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ b.exp ≤ max b.exp x
Theorem: le_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ b.exp ≤ max b.exp x
Tactic:
bound
Proof state after:
no goals
Theorem: maxLog_eq_b
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
h : x ≤ b.exp
⊢ maxLog b x = b
Tactic:
simp [maxLog, max_eq_left h]
Proof state after:
no goals
Theorem: maxLog_eq_log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
h : b.exp ≤ x
⊢ maxLog b x = x.log
Tactic:
simp [maxLog, max_eq_right h]
Proof state after:
no goals
Theorem: maxLog_le
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ maxLog b x ≤ y
Tactic:
rw [maxLog, Real.log_le_iff_le_exp max_exp_pos]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ max b.exp x ≤ y.exp
Theorem: maxLog_le
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ max b.exp x ≤ y.exp
Tactic:
apply max_le
Proof state after:
case h₁
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ b.exp ≤ y.exp

case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp
Theorem: maxLog_le
Proof state before:
case h₁
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ b.exp ≤ y.exp

case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp
Tactic:
apply Real.exp_le_exp.mpr yb
Proof state after:
case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp
Theorem: maxLog_le
Proof state before:
case h₂
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b ≤ y
xy : x ≤ y.exp
⊢ x ≤ y.exp
Tactic:
exact xy
Proof state after:
no goals
Theorem: le_exp_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ x ≤ (maxLog b x).exp
Tactic:
rw [maxLog, Real.exp_log max_exp_pos]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ x ≤ max b.exp x
Theorem: le_exp_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ x ≤ max b.exp x
Tactic:
bound
Proof state after:
no goals
Theorem: le_of_maxLog_le
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
m : maxLog b x ≤ y
⊢ x ≤ y.exp
Tactic:
rw [maxLog, Real.log_le_iff_le_exp max_exp_pos] at m
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
m : max b.exp x ≤ y.exp
⊢ x ≤ y.exp
Theorem: le_of_maxLog_le
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
m : max b.exp x ≤ y.exp
⊢ x ≤ y.exp
Tactic:
exact le_of_max_le_right m
Proof state after:
no goals
Theorem: monotone_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Monotone fun x => maxLog b x
Tactic:
simp_rw [maxLog]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Monotone fun x => (max b.exp x).log
Theorem: monotone_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Monotone fun x => (max b.exp x).log
Tactic:
intro x y xy
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (fun x => (max b.exp x).log) x ≤ (fun x => (max b.exp x).log) y
Theorem: monotone_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (fun x => (max b.exp x).log) x ≤ (fun x => (max b.exp x).log) y
Tactic:
simp only [ge_iff_le]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (max b.exp x).log ≤ (max b.exp y).log
Theorem: monotone_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ (max b.exp x).log ≤ (max b.exp y).log
Tactic:
rw [Real.log_le_log_iff max_exp_pos max_exp_pos]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ max b.exp x ≤ max b.exp y
Theorem: monotone_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
xy : x ≤ y
⊢ max b.exp x ≤ max b.exp y
Tactic:
apply max_le_max (le_refl _) xy
Proof state after:
no goals
Theorem: continuous_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Continuous fun x => maxLog b x
Tactic:
simp_rw [maxLog]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Continuous fun x => (max b.exp x).log
Theorem: continuous_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ Continuous fun x => (max b.exp x).log
Tactic:
rw [continuous_iff_continuousAt]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun x => (max b.exp x).log) x
Theorem: continuous_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun x => (max b.exp x).log) x
Tactic:
intro x
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => (max b.exp x).log) x
Theorem: continuous_maxLog
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => (max b.exp x).log) x
Tactic:
refine (ContinuousAt.log ?_ max_exp_pos.ne').comp ?_
Proof state after:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (max b.exp) x

case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => x) x
Theorem: continuous_maxLog
Proof state before:
case refine_1
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (max b.exp) x
Tactic:
apply Continuous.continuousAt
Proof state after:
case refine_1.h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous (max b.exp)
Theorem: continuous_maxLog
Proof state before:
case refine_1.h
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous (max b.exp)
Tactic:
apply Continuous.max
Proof state after:
case refine_1.h.hf
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b_1 => b.exp

case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b
Theorem: continuous_maxLog
Proof state before:
case refine_1.h.hf
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b_1 => b.exp

case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b
Tactic:
exact continuous_const
Proof state after:
case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b
Theorem: continuous_maxLog
Proof state before:
case refine_1.h.hg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ Continuous fun b => b
Tactic:
exact continuous_id
Proof state after:
no goals
Theorem: continuous_maxLog
Proof state before:
case refine_2
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x : ℝ
⊢ ContinuousAt (fun x => x) x
Tactic:
exact continuousAt_id
Proof state after:
no goals
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ LipschitzOnWith (-b).exp.toNNReal Real.log (Ici b.exp)
Tactic:
rw [lipschitzOnWith_iff_dist_le_mul]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Tactic:
have half : ∀ x y : ℝ, b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y| := by
  intro x y yb xy
  have yp : y > 0 := lt_of_lt_of_le (Real.exp_pos _) yb
  have xp : x > 0 := lt_of_lt_of_le yp xy
  have yi : y⁻¹ ≤ (-b).exp := by rw [Real.exp_neg]; bound
  rw [abs_of_nonneg (sub_nonneg.mpr xy)]
  rw [abs_of_nonneg (sub_nonneg.mpr ((Real.log_le_log_iff yp xp).mpr xy))]
  rw [← Real.log_div xp.ne' yp.ne']
  rw [Real.log_le_iff_le_exp (div_pos xp yp)]
  trans (y⁻¹ * (x - y)).exp; swap; bound
  have e : y⁻¹ * (x - y) = x / y - 1 := by field_simp [yp.ne']
  rw [e]
  have e1 := Real.add_one_le_exp (x / y - 1)
  simp at e1; exact e1
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
⊢ ∀ x ∈ Ici b.exp, ∀ y ∈ Ici b.exp, dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Tactic:
intro x xs y ys
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x : ℝ
xs : x ∈ Ici b.exp
y : ℝ
ys : y ∈ Ici b.exp
⊢ dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x : ℝ
xs : x ∈ Ici b.exp
y : ℝ
ys : y ∈ Ici b.exp
⊢ dist x.log y.log ≤ ↑(-b).exp.toNNReal * dist x y
Tactic:
simp at xs ys ⊢
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ max (-b).exp 0 * dist x y
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ max (-b).exp 0 * dist x y
Tactic:
rw [max_eq_left (Real.exp_pos _).le]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ (-b).exp * dist x y
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ dist x.log y.log ≤ (-b).exp * dist x y
Tactic:
simp_rw [Real.dist_eq]
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
by_cases xy : x ≥ y
Proof state after:
case pos
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|

case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : ¬x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Theorem: LipschitzOnWith.log
Proof state before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : ¬x ≥ y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
simp at xy
Proof state after:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Theorem: LipschitzOnWith.log
Proof state before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
rw [← neg_sub y x, abs_neg]
Proof state after:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |y - x|
Theorem: LipschitzOnWith.log
Proof state before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |x.log - y.log| ≤ (-b).exp * |y - x|
Tactic:
rw [← neg_sub y.log x.log, abs_neg]
Proof state after:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |y.log - x.log| ≤ (-b).exp * |y - x|
Theorem: LipschitzOnWith.log
Proof state before:
case neg
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
half : ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
x y : ℝ
xs : b.exp ≤ x
ys : b.exp ≤ y
xy : x < y
⊢ |y.log - x.log| ≤ (-b).exp * |y - x|
Tactic:
exact half y x xs xy.le
Proof state after:
no goals
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b : ℝ
⊢ ∀ (x y : ℝ), b.exp ≤ y → y ≤ x → |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
intro x y yb xy
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Theorem: LipschitzOnWith.log
Proof state before:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|
Tactic:
have yp : y > 0 := lt_of_lt_of_le (Real.exp_pos _) yb
Proof state after:
E : Type
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
b x y : ℝ
yb : b.exp ≤ y
xy : y ≤ x
yp : y > 0
⊢ |x.log - y.log| ≤ (-b).exp * |x - y|