Theorem: fourierExtend (Ray/Hartogs/Subharmonic.lean)

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ Extendable f c r
Tactic:
apply Submodule.span_induction (p := fun f ↦ Extendable f c r) s
State after:
case mem
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ x ∈ Set.range fourier, Extendable x c r

case zero
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ Extendable 0 c r

case add
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ (x y : C(Real.Angle, ℂ)), Extendable x c r → Extendable y c r → Extendable (x + y) c r

case smul
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ (a : ℂ) (x : C(Real.Angle, ℂ)), Extendable x c r → Extendable (a • x) c r

State before:
case mem
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ x ∈ Set.range fourier, Extendable x c r
Tactic:
intro g gs
State after:
case mem
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
gs : g ∈ Set.range fourier
⊢ Extendable g c r

State before:
case mem
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
gs : g ∈ Set.range fourier
⊢ Extendable g c r
Tactic:
simp only [Set.mem_range] at gs
State after:
case mem
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
gs : ∃ y, fourier y = g
⊢ Extendable g c r

State before:
case mem
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
gs : ∃ y, fourier y = g
⊢ Extendable g c r
Tactic:
rcases gs with ⟨n, ng⟩
State after:
case mem.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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
n : ℤ
ng : fourier n = g
⊢ Extendable g c r

State before:
case mem.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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
n : ℤ
ng : fourier n = g
⊢ Extendable g c r
Tactic:
rw [← ng]
State after:
case mem.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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
n : ℤ
ng : fourier n = g
⊢ Extendable (fourier n) c r

State before:
case mem.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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
g : C(Real.Angle, ℂ)
n : ℤ
ng : fourier n = g
⊢ Extendable (fourier n) c r
Tactic:
exact fourierExtend' rp _
State after:
no goals

State before:
case zero
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ Extendable 0 c r
Tactic:
use fun _ ↦ 0
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ HasExtension 0 (fun x => 0) c r

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ HasExtension 0 (fun x => 0) c r
Tactic:
exact
  { gh := HarmonicOn.const _
    b := by simp only [ContinuousMap.coe_zero, Pi.zero_apply, forall_const] }
State after:
no goals

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ (t : Real.Angle), 0 t = 0
Tactic:
simp only [ContinuousMap.coe_zero, Pi.zero_apply, forall_const]
State after:
no goals

State before:
case add
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ (x y : C(Real.Angle, ℂ)), Extendable x c r → Extendable y c r → Extendable (x + y) c r
Tactic:
intro x y xe ye
State after:
case add
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
xe : Extendable x c r
ye : Extendable y c r
⊢ Extendable (x + y) c r

State before:
case add
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
xe : Extendable x c r
ye : Extendable y c r
⊢ Extendable (x + y) c r
Tactic:
rcases xe with ⟨x', xh, xb⟩
State after:
case add.intro.mk
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
ye : Extendable y c r
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ Extendable (x + y) c r

State before:
case add.intro.mk
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
ye : Extendable y c r
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ Extendable (x + y) c r
Tactic:
rcases ye with ⟨y', yh, yb⟩
State after:
case add.intro.mk.intro.mk
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
y' : ℂ → ℂ
yh : HarmonicOn y' (closedBall c r)
yb : ∀ (t : Real.Angle), y t = y' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ Extendable (x + y) c r

State before:
case add.intro.mk.intro.mk
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
y' : ℂ → ℂ
yh : HarmonicOn y' (closedBall c r)
yb : ∀ (t : Real.Angle), y t = y' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ Extendable (x + y) c r
Tactic:
use fun z ↦ x' z + y' z
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
y' : ℂ → ℂ
yh : HarmonicOn y' (closedBall c r)
yb : ∀ (t : Real.Angle), y t = y' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ HasExtension (x + y) (fun z => x' z + y' z) c r

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
y' : ℂ → ℂ
yh : HarmonicOn y' (closedBall c r)
yb : ∀ (t : Real.Angle), y t = y' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ HasExtension (x + y) (fun z => x' z + y' z) c r
Tactic:
exact
  { gh := xh.add yh
    b := by
      simp only [xb, yb, ContinuousMap.coe_add, Pi.add_apply, eq_self_iff_true, forall_const] }
State after:
no goals

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
x y : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
y' : ℂ → ℂ
yh : HarmonicOn y' (closedBall c r)
yb : ∀ (t : Real.Angle), y t = y' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ ∀ (t : Real.Angle), (x + y) t = x' (c + ↑r * ↑(AddCircle.toCircle t)) + y' (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
simp only [xb, yb, ContinuousMap.coe_add, Pi.add_apply, eq_self_iff_true, forall_const]
State after:
no goals

State before:
case smul
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ ∀ (a : ℂ) (x : C(Real.Angle, ℂ)), Extendable x c r → Extendable (a • x) c r
Tactic:
intro a x xe
State after:
case smul
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
xe : Extendable x c r
⊢ Extendable (a • x) c r

State before:
case smul
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
xe : Extendable x c r
⊢ Extendable (a • x) c r
Tactic:
rcases xe with ⟨x', xh, xb⟩
State after:
case smul.intro.mk
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ Extendable (a • x) c r

State before:
case smul.intro.mk
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ Extendable (a • x) c r
Tactic:
use fun z ↦ a * x' z
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ HasExtension (a • x) (fun z => a * x' z) c r

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ HasExtension (a • x) (fun z => a * x' z) c r
Tactic:
exact
  { gh := xh.const_mul _
    b := by
      simp only [xb, ContinuousMap.coe_smul, Pi.smul_apply, Algebra.id.smul_eq_mul,
        eq_self_iff_true, forall_const] }
State after:
no goals

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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
a : ℂ
x : C(Real.Angle, ℂ)
x' : ℂ → ℂ
xh : HarmonicOn x' (closedBall c r)
xb : ∀ (t : Real.Angle), x t = x' (c + ↑r * ↑(AddCircle.toCircle t))
⊢ ∀ (t : Real.Angle), (a • x) t = a * x' (c + ↑r * ↑(AddCircle.toCircle t))
Tactic:
simp only [xb, ContinuousMap.coe_smul, Pi.smul_apply, Algebra.id.smul_eq_mul,
  eq_self_iff_true, forall_const]
State after:
no goals