Theorem: unevenTerm.analytic (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ AnalyticOn ℂ (fun z1 => unevenTerm u z1 n) (ball c1 r1)
Tactic:
have e : ∀ z1, unevenTerm u z1 n =
    (cmmapApplyCmap ℂ (fun _ : Fin n ↦ ℂ) E fun _ ↦ 1) (unevenSeries u z1 n) := by
  intro z1; simp [unevenTerm, ←unevenSeries_apply, cmmapApplyCmap, unevenSeries,
    ContinuousLinearMap.coe_mk', LinearMap.coe_mk]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => unevenTerm u z1 n) (ball c1 r1)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => unevenTerm u z1 n) (ball c1 r1)
Tactic:
simp_rw [e]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)) (ball c1 r1)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e✝ : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
e : ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
⊢ AnalyticOn ℂ (fun z1 => (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)) (ball c1 r1)
Tactic:
exact ContinuousLinearMap.comp_analyticOn _ (unevenSeries_analytic u n)
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
⊢ ∀ (z1 : ℂ), unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
Tactic:
intro z1
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
⊢ unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1✝ w0 w1 : ℂ
r r0 r1 b e : ℝ
u : Uneven f c0 c1 r0 r1
n : ℕ
z1 : ℂ
⊢ unevenTerm u z1 n = (cmmapApplyCmap ℂ (fun x => ℂ) E fun x => 1) (unevenSeries u z1 n)
Tactic:
simp [unevenTerm, ←unevenSeries_apply, cmmapApplyCmap, unevenSeries,
ContinuousLinearMap.coe_mk', LinearMap.coe_mk]
State after:
no goals