internlm/Lean-Github huggingface dataset:
Theorem: fourierExtend
Proof 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
Proof 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
Theorem: fourierExtend
Proof 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⟩
Proof 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
Theorem: fourierExtend
Proof 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
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)
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
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)
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] }
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)
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]
Proof state after:
no goals
Theorem: continuousExtend
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, ℂ)
c : ℂ
rp : r > 0
⊢ Extendable f c r
Tactic:
set s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range (@fourier (2 * π)))
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 : ℝ
f : C(Real.Angle, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
⊢ Extendable f c r
Theorem: continuousExtend
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
⊢ Extendable f c r
Tactic:
have se : ∀ f, f ∈ s.carrier → Extendable f c r := fun f fs ↦ fourierExtend rp fs
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 : ℝ
f : C(Real.Angle, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
⊢ Extendable f c r
Theorem: continuousExtend
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
⊢ Extendable f c r
Tactic:
have ce : ∀ f, f ∈ closure s.carrier → Extendable f c r := IsClosed.extendable se 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 : ℝ
f : C(Real.Angle, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ closure s.carrier, Extendable f c r
⊢ Extendable f c r
Theorem: continuousExtend
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ closure s.carrier, Extendable f c r
⊢ Extendable f c r
Tactic:
have e : closure s.carrier = s.topologicalClosure.carrier := rfl
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 : ℝ
f : C(Real.Angle, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ closure s.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ Extendable f c r
Theorem: continuousExtend
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ closure s.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ Extendable f c r
Tactic:
rw [e, @span_fourier_closure_eq_top _ (fact_iff.mpr Real.two_pi_pos)] at ce
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 : ℝ
f : C(Real.Angle, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ ⊤.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ Extendable f c r
Theorem: continuousExtend
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ ⊤.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ Extendable f c r
Tactic:
apply ce
Proof state after:
case a
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ ⊤.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ f ∈ ⊤.carrier
Theorem: continuousExtend
Proof state before:
case a
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ ⊤.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ f ∈ ⊤.carrier
Tactic:
simp only [Submodule.mem_carrier]
Proof state after:
case a
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ ⊤.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ f ∈ ↑⊤
Theorem: continuousExtend
Proof state before:
case a
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, ℂ)
c : ℂ
rp : r > 0
s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range fourier)
se : ∀ f ∈ s.carrier, Extendable f c r
ce : ∀ f ∈ ⊤.carrier, Extendable f c r
e : closure s.carrier = s.topologicalClosure.carrier
⊢ f ∈ ↑⊤
Tactic:
trivial
Proof state after:
no goals
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
⊢ ∀ (c : ℂ), ∀ r > 0, closedBall c r ⊆ s → f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
intro c r rp cs
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have cm : c ∈ s := cs (Metric.mem_closedBall_self (by linarith))
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have rm : c + r ∈ s := cs (by
  simp only [abs_of_pos rp, Metric.mem_closedBall, dist_self_add_left,
    Complex.norm_eq_abs, Complex.abs_ofReal, le_refl])
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
rm : c + ↑r ∈ s
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Theorem: HarmonicOn.subsingleton
Proof state before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
rm : c + ↑r ∈ s
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)
Tactic:
have e : c = c + r := ss cm rm
Proof state after:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → S
s : Set ℂ
ss : s.Subsingleton
c : ℂ
r : ℝ
rp : r > 0
cs : closedBall c r ⊆ s
cm : c ∈ s
rm : c + ↑r ∈ s
e : c = c + ↑r
⊢ f c = ⨍ (t : ℝ) in itau, f (circleMap c r t)