theorem
WithLp.analyticOn_ofLp
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField π]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace π E]
[NormedSpace π F]
(p : ENNReal)
[Fact (1 β€ p)]
(s : Set (WithLp p (E Γ F)))
:
AnalyticOn π ofLp s
theorem
WithLp.analyticOn_toLp
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField π]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedSpace π E]
[NormedSpace π F]
(p : ENNReal)
[Fact (1 β€ p)]
(s : Set (E Γ F))
:
AnalyticOn π (toLp p) s
theorem
PiLp.analyticOn_ofLp
{π : Type u_1}
{ΞΉ : Type u_2}
[Fintype ΞΉ]
{E : ΞΉ β Type u_3}
[NontriviallyNormedField π]
[(i : ΞΉ) β NormedAddCommGroup (E i)]
[(i : ΞΉ) β NormedSpace π (E i)]
(p : ENNReal)
[Fact (1 β€ p)]
(s : Set (PiLp p E))
:
AnalyticOn π WithLp.ofLp s
theorem
PiLp.analyticOn_toLp
{π : Type u_1}
{ΞΉ : Type u_2}
[Fintype ΞΉ]
{E : ΞΉ β Type u_3}
[NontriviallyNormedField π]
[(i : ΞΉ) β NormedAddCommGroup (E i)]
[(i : ΞΉ) β NormedSpace π (E i)]
(p : ENNReal)
[Fact (1 β€ p)]
(s : Set ((i : ΞΉ) β E i))
:
AnalyticOn π (WithLp.toLp p) s