Theorem: continuousExtend (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, ℂ)
c : ℂ
rp : r > 0
⊢ Extendable f c r
Tactic:
set s : Submodule ℂ C(Real.Angle, ℂ) := Submodule.span ℂ (Set.range (@fourier (2 * π)))
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

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
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

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
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

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
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

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
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

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
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

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]
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 ∈ ↑⊤

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
State after:
no goals