internlm/Lean-Github huggingface dataset:
Theorem: continuous_to_harmonic_complex
Proof state before:
case right.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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
rr : c + ↑r * ↑t.toCircle = z
⊢ f z = { toFun := f', continuous_toFun := fc' } t
Tactic:
simp only [← hf', rr, ContinuousMap.coe_mk]
Proof state after:
no goals
Theorem: continuous_to_harmonic_complex
Proof state before:
case pos
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
use f
Proof state after:
case h
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ HarmonicOn f (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = f z
Theorem: continuous_to_harmonic_complex
Proof state before:
case h
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ HarmonicOn f (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = f z
Tactic:
use HarmonicOn.subsingleton (Metric.subsingleton_closedBall _ rp)
Proof state after:
case right
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∀ z ∈ sphere c r, f z = f z
Theorem: continuous_to_harmonic_complex
Proof state before:
case right
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
⊢ ∀ z ∈ sphere c r, f z = f z
Tactic:
intros
Proof state after:
case right
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
z✝ : ℂ
a✝ : z✝ ∈ sphere c r
⊢ f z✝ = f z✝
Theorem: continuous_to_harmonic_complex
Proof state before:
case right
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : r ≤ 0
z✝ : ℂ
a✝ : z✝ ∈ sphere c r
⊢ f z✝ = f z✝
Tactic:
rfl
Proof state after:
no goals
Theorem: continuous_to_harmonic_complex
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous f'
Tactic:
rw [← hf']
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => f (c + ↑r * ↑(AddCircle.toCircle t))
Theorem: continuous_to_harmonic_complex
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => f (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
apply fc.comp_continuous
Proof state after:
case hf
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => c + ↑r * ↑(AddCircle.toCircle t)

case hs
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ ∀ (x : Real.Angle), c + ↑r * ↑(AddCircle.toCircle x) ∈ sphere c r
Theorem: continuous_to_harmonic_complex
Proof state before:
case hf
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Continuous fun t => c + ↑r * ↑(AddCircle.toCircle t)
Tactic:
exact continuous_const.add
  (continuous_const.mul (continuous_subtype_val.comp AddCircle.continuous_toCircle))
Proof state after:
no goals
Theorem: continuous_to_harmonic_complex
Proof state before:
case hs
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ ∀ (x : Real.Angle), c + ↑r * ↑(AddCircle.toCircle x) ∈ sphere c r
Tactic:
simp only [mem_sphere_iff_norm, add_sub_cancel_left, Complex.norm_eq_abs,
  AbsoluteValue.map_mul, Complex.abs_ofReal, abs_coe_circle, mul_one, abs_eq_self]
Proof state after:
case hs
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Real.Angle → 0 ≤ r
Theorem: continuous_to_harmonic_complex
Proof state before:
case hs
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
⊢ Real.Angle → 0 ≤ r
Tactic:
intro _
Proof state after:
case hs
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
x✝ : Real.Angle
⊢ 0 ≤ r
Theorem: continuous_to_harmonic_complex
Proof state before:
case hs
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
x✝ : Real.Angle
⊢ 0 ≤ r
Tactic:
bound
Proof state after:
no goals
Theorem: continuous_to_harmonic_complex
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
⊢ Complex.abs z' = 1
Tactic:
simp only [mem_sphere_iff_norm, Complex.norm_eq_abs] at 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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
zs : Complex.abs (z - c) = r
⊢ Complex.abs z' = 1
Theorem: continuous_to_harmonic_complex
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
zs : Complex.abs (z - c) = r
⊢ Complex.abs z' = 1
Tactic:
simp only [zs, abs_of_pos rp, inv_mul_cancel rp.ne', AbsoluteValue.map_mul, map_inv₀,
  Complex.abs_ofReal, ← hz']
Proof state after:
no goals
Theorem: continuous_to_harmonic_complex
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ c + ↑r * ↑t.toCircle = z
Tactic:
rw [← tz, ← hz']
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ c + ↑r * ((↑r)⁻¹ * (z - c)) = z
Theorem: continuous_to_harmonic_complex
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 : ℂ → ℂ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
rp : 0 < r
f' : Real.Angle → ℂ
hf' : (fun t => f (c + ↑r * ↑(AddCircle.toCircle t))) = f'
fc' : Continuous f'
g : ℂ → ℂ
e : HasExtension { toFun := f', continuous_toFun := fc' } g c r
z : ℂ
zs : z ∈ sphere c r
z' : ℂ
hz' : (↑r)⁻¹ * (z - c) = z'
za' : Complex.abs z' = 1
t : AddCircle (2 * π)
tz : z' = ↑t.toCircle
⊢ c + ↑r * ((↑r)⁻¹ * (z - c)) = z
Tactic:
exact rri rp _
Proof state after:
no goals
Theorem: continuous_to_harmonic_real
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
generalize hf' : (fun z ↦ (f z : ℂ)) = f'
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Theorem: continuous_to_harmonic_real
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
have fc' : ContinuousOn f' (sphere c r) := by
  rw [← hf']; exact Complex.continuous_ofReal.comp_continuousOn fc
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Theorem: continuous_to_harmonic_real
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z
Tactic:
rcases continuous_to_harmonic_complex fc' with ⟨g, gh, b⟩
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 : ℂ → ℝ
c : ℂ
r : ℝ
fc : ContinuousOn f (sphere c r)
f' : ℂ → ℂ
hf' : (fun z => ↑(f z)) = f'
fc' : ContinuousOn f' (sphere c r)
g : ℂ → ℂ
gh : HarmonicOn g (closedBall c r)
b : ∀ z ∈ sphere c r, f' z = g z
⊢ ∃ g, HarmonicOn g (closedBall c r) ∧ ∀ z ∈ sphere c r, f z = g z