internlm/Lean-Github huggingface dataset:
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - k] z' ∈ approx i.z ∧ (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - k] z') ^ 2)
Tactic:
rw [ie, Function.iterate_succ_apply, hw']
Proof state after:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
    (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
Theorem: iterate'_correct
Proof state before:
case neg
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
ie : i.n - k = i.n - (k + 1) + 1
⊢ (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
    (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
Tactic:
exact h.2
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ k ≤ i.n
Tactic:
omega
Proof state after:
no goals
Theorem: iterate'_correct
Proof state before:
c : Box
rs : Floating
c' : ℂ
rs' : ℝ
cm : c' ∈ approx c
rsn : rs ≠ nan
rsm : rs' ≤ rs.val
n : ℕ
z : Box
z' : ℂ
zm : z' ∈ approx z
k : ℕ
zr2 : Interval
hzr2 : z.re.sqr = zr2
zi2 : Interval
hzi2 : z.im.sqr = zi2
z2 : Floating
hz2 : zr2.lo.add zi2.lo false = z2
w : Box
hw : { re := zr2 - zi2, im := (z.re * z.im).scaleB 1 } + c = w
we : w = z.sqr + c
w' : ℂ
hw' : f' 2 c' z' = w'
wa : w' ∈ approx w
z2n : ¬z2 = nan
rz : ¬rs.val < z2.val
i : Iter
hi : iterate' c w rs (k + 1) n = i
h :
  k + 1 ≤ i.n ∧
    (f' 2 c')^[i.n - (k + 1)] w' ∈ approx i.z ∧
      (i.exit = Exit.large → rs' < Complex.abs ((f' 2 c')^[i.n - (k + 1)] w') ^ 2)
⊢ i.n - k = i.n - (k + 1) + 1
Tactic:
omega
Proof state after:
no goals
Theorem: mem_approx_iterate
Proof state before:
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
⊢ (f' 2 c')^[(iterate c z rs n).n] z' ∈ approx (iterate c z rs n).z
Tactic:
rw [iterate]
Proof state after:
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z
Theorem: mem_approx_iterate
Proof state before:
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z
Tactic:
by_cases rsn : rs = nan
Proof state after:
case pos
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : rs = nan
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z

case neg
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : ¬rs = nan
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z
Theorem: mem_approx_iterate
Proof state before:
case pos
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : rs = nan
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z
Tactic:
simpa only [rsn, ite_true, Function.iterate_zero, id_eq]
Proof state after:
no goals
Theorem: mem_approx_iterate
Proof state before:
case neg
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : ¬rs = nan
⊢ (f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z' ∈
    approx (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).z
Tactic:
simp only [rsn, ite_false]
Proof state after:
case neg
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : ¬rs = nan
⊢ (f' 2 c')^[(iterate' c z rs 0 n).n] z' ∈ approx (iterate' c z rs 0 n).z
Theorem: mem_approx_iterate
Proof state before:
case neg
c z : Box
rs : Floating
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
rsn : ¬rs = nan
⊢ (f' 2 c')^[(iterate' c z rs 0 n).n] z' ∈ approx (iterate' c z rs 0 n).z
Tactic:
exact (iterate'_correct cm zm rsn (le_refl _) 0 n).2.1
Proof state after:
no goals
Theorem: iterate_large
Proof state before:
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (iterate c z rs n).exit = Exit.large
⊢ rs.val < Complex.abs ((f' 2 c')^[(iterate c z rs n).n] z') ^ 2
Tactic:
rw [iterate] at l ⊢
Proof state after:
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Theorem: iterate_large
Proof state before:
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Tactic:
by_cases rsn : rs = nan
Proof state after:
case pos
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2

case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : ¬rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Theorem: iterate_large
Proof state before:
case pos
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Tactic:
simp only [rsn, ↓reduceIte] at l
Proof state after:
no goals
Theorem: iterate_large
Proof state before:
case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
l : (if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).exit = Exit.large
rsn : ¬rs = nan
⊢ rs.val <
    Complex.abs ((f' 2 c')^[(if rs = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z rs 0 n).n] z') ^ 2
Tactic:
simp only [rsn, ite_false] at l ⊢
Proof state after:
case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
rsn : ¬rs = nan
l : (iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val < Complex.abs ((f' 2 c')^[(iterate' c z rs 0 n).n] z') ^ 2
Theorem: iterate_large
Proof state before:
case neg
c z : Box
rs : Floating
n : ℕ
c' z' : ℂ
cm : c' ∈ approx c
zm : z' ∈ approx z
rsn : ¬rs = nan
l : (iterate' c z rs 0 n).exit = Exit.large
⊢ rs.val < Complex.abs ((f' 2 c')^[(iterate' c z rs 0 n).n] z') ^ 2
Tactic:
simpa only [not_lt, Nat.sub_zero] using (iterate'_correct cm zm rsn (le_refl _) 0 n).2.2 l
Proof state after:
no goals
Theorem: iterate_nan
Proof state before:
c z : Box
n : ℕ
⊢ (iterate c z nan n).exit = Exit.nan
Tactic:
rw [iterate]
Proof state after:
c z : Box
n : ℕ
⊢ (if nan = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z nan 0 n).exit = Exit.nan
Theorem: iterate_nan
Proof state before:
c z : Box
n : ℕ
⊢ (if nan = nan then { z := z, n := 0, exit := Exit.nan } else iterate' c z nan 0 n).exit = Exit.nan
Tactic:
simp only [ite_true, Function.iterate_zero]
Proof state after:
no goals
Theorem: ne_nan_of_iterate
Proof state before:
c z : Box
rs : Floating
n : ℕ
e : (iterate c z rs n).exit ≠ Exit.nan
⊢ rs ≠ nan
Tactic:
contrapose e
Proof state after:
c z : Box
rs : Floating
n : ℕ
e : ¬rs ≠ nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan
Theorem: ne_nan_of_iterate
Proof state before:
c z : Box
rs : Floating
n : ℕ
e : ¬rs ≠ nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan
Tactic:
simp only [ne_eq, not_not] at e
Proof state after:
c z : Box
rs : Floating
n : ℕ
e : rs = nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan
Theorem: ne_nan_of_iterate
Proof state before:
c z : Box
rs : Floating
n : ℕ
e : rs = nan
⊢ ¬(iterate c z rs n).exit ≠ Exit.nan
Tactic:
simp only [e, iterate_nan, ne_eq, not_true_eq_false, not_false_eq_true]
Proof state after:
no goals
Theorem: HarmonicOn.convex
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
⊢ ∀ c ∈ interior s, ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f c) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap c s t))
Tactic:
intro z zs
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Theorem: HarmonicOn.convex
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 : ℂ → E
s : Set ℂ
g : E → ℝ
fh : HarmonicOn f s
c : Continuous g
gc : ConvexOn ℝ univ g
z : ℂ
zs : z ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior z zs with ⟨r, rp, rh⟩
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 : ℂ → 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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Theorem: HarmonicOn.convex
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 : ℂ → 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
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Tactic:
exists r, rp
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 : ℂ → 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
⊢ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Theorem: HarmonicOn.convex
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 : ℂ → 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
⊢ ∀ (s : ℝ), 0 < s → s < r → g (f z) ≤ ⨍ (t : ℝ) in itau, g (f (circleMap z s t))
Tactic:
intro t tp tr
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 : ℂ → 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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Theorem: HarmonicOn.convex
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 : ℂ → 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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
have cs : closedBall z t ⊆ s :=
  _root_.trans (Metric.closedBall_subset_ball tr) (_root_.trans rh interior_subset)
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 : ℂ → 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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Theorem: HarmonicOn.convex
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 : ℂ → 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
⊢ g (f z) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
simp only [fh.mean z t tp cs]
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 : ℂ → 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
⊢ g (⨍ (t_1 : ℝ) in itau, f (circleMap z t t_1)) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Theorem: HarmonicOn.convex
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 : ℂ → 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
⊢ g (⨍ (t_1 : ℝ) in itau, f (circleMap z t t_1)) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))
Tactic:
have n := NiceVolume.itau
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 : ℂ → 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
⊢ g (⨍ (t_1 : ℝ) in itau, f (circleMap z t t_1)) ≤ ⨍ (t_1 : ℝ) in itau, g (f (circleMap z t t_1))