internlm/Lean-Github huggingface dataset:
Theorem: fourierExtend'
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
⊢ ∀ (t : Real.Angle), (fourier (-↑n)) t = (starRingEnd ℂ) (((↑r)⁻¹ * (c + ↑r * ↑(AddCircle.toCircle t) - c)) ^ n)
Tactic:
intro t
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
t : Real.Angle
⊢ (fourier (-↑n)) t = (starRingEnd ℂ) (((↑r)⁻¹ * (c + ↑r * ↑(AddCircle.toCircle t) - c)) ^ n)
Theorem: fourierExtend'
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
t : Real.Angle
⊢ (fourier (-↑n)) t = (starRingEnd ℂ) (((↑r)⁻¹ * (c + ↑r * ↑(AddCircle.toCircle t) - c)) ^ n)
Tactic:
rw [rir rp]
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
t : Real.Angle
⊢ (fourier (-↑n)) t = (starRingEnd ℂ) (↑(AddCircle.toCircle t) ^ n)
Theorem: fourierExtend'
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
t : Real.Angle
⊢ (fourier (-↑n)) t = (starRingEnd ℂ) (↑(AddCircle.toCircle t) ^ n)
Tactic:
apply Eq.trans fourier_apply
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
t : Real.Angle
⊢ ↑(-↑n • t).toCircle = (starRingEnd ℂ) (↑(AddCircle.toCircle t) ^ n)
Theorem: fourierExtend'
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
c : ℂ
r : ℝ
rp : r > 0
mh : ∀ (n : ℕ), HarmonicOn (fun z => ((↑r)⁻¹ * (z - c)) ^ n) (closedBall c r)
n : ℕ
t : Real.Angle
⊢ ↑(-↑n • t).toCircle = (starRingEnd ℂ) (↑(AddCircle.toCircle t) ^ n)
Tactic:
simp only [neg_smul, natCast_zsmul, toCircle_neg, toCircle_smul, coe_inv_unitSphere,
  SubmonoidClass.coe_pow, Complex.inv_def, map_pow, normSq_eq_of_mem_circle, one_pow,
  inv_one, Complex.ofReal_one, mul_one]
Proof state after:
no goals
Theorem: fourierExtend
Proof 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
Proof 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
Theorem: fourierExtend
Proof 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
Proof 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
Theorem: fourierExtend
Proof 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⟩
Proof 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
Theorem: fourierExtend
Proof 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]
Proof 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
Theorem: fourierExtend
Proof 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 _
Proof state after:
no goals
Theorem: fourierExtend
Proof 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
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
c : ℂ
r : ℝ
f : C(Real.Angle, ℂ)
rp : r > 0
s : f ∈ Submodule.span ℂ (Set.range fourier)
⊢ HasExtension 0 (fun x => 0) c r
Theorem: fourierExtend
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
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] }
Proof state after:
no goals
Theorem: fourierExtend
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
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]
Proof state after:
no goals
Theorem: fourierExtend
Proof 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
Proof 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
Theorem: fourierExtend
Proof 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⟩
Proof 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
Theorem: fourierExtend
Proof 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⟩
Proof 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
Theorem: fourierExtend
Proof 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
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
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
Theorem: fourierExtend
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
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] }
Proof state after:
no goals
Theorem: fourierExtend
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
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]
Proof state after:
no goals