Theorem: Along0.analyticAt (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 : ℝ
n : ℕ
⊢ ∀ {p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E}, AnalyticAt ℂ (fun p => p.along0) p
Tactic:
intro p
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ AnalyticAt ℂ (fun p => p.along0) p

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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ AnalyticAt ℂ (fun p => p.along0) p
Tactic:
have e : (fun p : ContinuousMultilinearMap ℂ (fun _ : Fin n ↦ ℂ × ℂ) E => p.along0) =ᶠ[𝓝 p]
    (Along0.continuousLinearMap n : (ContinuousMultilinearMap ℂ (fun _ : Fin n ↦ ℂ × ℂ) E →
      ContinuousMultilinearMap ℂ (fun _ : Fin n ↦ ℂ) E)) := by
  apply eventually_of_forall; intro _; rfl
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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (fun p => p.along0) p

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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (fun p => p.along0) p
Tactic:
rw [analyticAt_congr 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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (⇑(continuousLinearMap n)) p

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✝ : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
e : (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
⊢ AnalyticAt ℂ (⇑(continuousLinearMap n)) p
Tactic:
apply ContinuousLinearMap.analyticAt
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ (𝓝 p).EventuallyEq (fun p => p.along0) ⇑(continuousLinearMap n)
Tactic:
apply eventually_of_forall
State after:
case hp
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ ∀ (x : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E), (fun p => p.along0) x = (continuousLinearMap n) x

State before:
case hp
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 : ℝ
n : ℕ
p : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ ∀ (x : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E), (fun p => p.along0) x = (continuousLinearMap n) x
Tactic:
intro _
State after:
case hp
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 : ℝ
n : ℕ
p x✝ : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ (fun p => p.along0) x✝ = (continuousLinearMap n) x✝

State before:
case hp
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 : ℝ
n : ℕ
p x✝ : ContinuousMultilinearMap ℂ (fun x => ℂ × ℂ) E
⊢ (fun p => p.along0) x✝ = (continuousLinearMap n) x✝
Tactic:
rfl
State after:
no goals