Analyticity on WithLp

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