internlm/Lean-Github huggingface dataset:
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
e : ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
⊢ AnalyticAt 𝕜 (fun x => p (_root_.fderiv 𝕜 (uncurry f) x)) c
Tactic:
exact (p.analyticAt _).comp fa.fderiv
Proof state after:
no goals
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ ∀ᶠ (x : E × 𝕜) in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
Tactic:
refine fa.eventually_analyticAt.mp (eventually_of_forall ?_)
Proof state after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ ∀ (x : E × 𝕜), AnalyticAt 𝕜 (uncurry f) x → _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
⊢ ∀ (x : E × 𝕜), AnalyticAt 𝕜 (uncurry f) x → _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x)
Tactic:
intro ⟨x, y⟩ fa
Proof state after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ _root_.deriv (f (x, y).1) (x, y).2 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ _root_.deriv (f (x, y).1) (x, y).2 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
simp only [← fderiv_deriv]
Proof state after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
have e : f x = uncurry f ∘ fun y ↦ (x, y) := rfl
Proof state after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (f x) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
rw [e]
Proof state after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (uncurry f ∘ fun y => (x, y)) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ (_root_.fderiv 𝕜 (uncurry f ∘ fun y => (x, y)) y) 1 = p (_root_.fderiv 𝕜 (uncurry f) (x, y))
Tactic:
rw [fderiv.comp]
Proof state after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ ((_root_.fderiv 𝕜 (uncurry f) (x, y)).comp (_root_.fderiv 𝕜 (fun y => (x, y)) y)) 1 =
    p (_root_.fderiv 𝕜 (uncurry f) (x, y))

case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)

case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y
Theorem: AnalyticAt.deriv2
Proof state before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ _root_.fderiv 𝕜 (fun y => (x, y)) y = ContinuousLinearMap.inr 𝕜 E 𝕜
Tactic:
apply HasFDerivAt.fderiv
Proof state after:
case h
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ HasFDerivAt (fun y => (x, y)) (ContinuousLinearMap.inr 𝕜 E 𝕜) y
Theorem: AnalyticAt.deriv2
Proof state before:
case h
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ HasFDerivAt (fun y => (x, y)) (ContinuousLinearMap.inr 𝕜 E 𝕜) y
Tactic:
apply hasFDerivAt_prod_mk_right
Proof state after:
no goals
Theorem: AnalyticAt.deriv2
Proof state before:
case hg
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (uncurry f) (x, y)
Tactic:
exact fa.differentiableAt
Proof state after:
no goals
Theorem: AnalyticAt.deriv2
Proof state before:
case hf
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
inst✝ : CompleteSpace 𝕜
f : E → 𝕜 → 𝕜
c : E × 𝕜
fa✝ : AnalyticAt 𝕜 (uncurry f) c
p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := (ContinuousLinearMap.apply 𝕜 𝕜) (0, 1)
x : E
y : 𝕜
fa : AnalyticAt 𝕜 (uncurry f) (x, y)
e : f x = uncurry f ∘ fun y => (x, y)
⊢ DifferentiableAt 𝕜 (fun y => (x, y)) y
Tactic:
exact (differentiableAt_const _).prod differentiableAt_id
Proof state after:
no goals
Theorem: HasFPowerSeriesAt.const_smul
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ HasFPowerSeriesAt (fun z => a • f z) (fun n => a • p n) c
Tactic:
rw [hasFPowerSeriesAt_iff] at fp ⊢
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))
Theorem: HasFPowerSeriesAt.const_smul
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))
Tactic:
refine fp.mp (eventually_of_forall fun z h ↦ ?_)
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))
Theorem: HasFPowerSeriesAt.const_smul
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => z ^ n • FormalMultilinearSeries.coeff (fun n => a • p n) n) (a • f (c + z))
Tactic:
simp only [FormalMultilinearSeries.coeff, ContinuousMultilinearMap.smul_apply, smul_comm _ a]
Proof state after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => a • z ^ n • (p n) 1) (a • f (c + z))
Theorem: HasFPowerSeriesAt.const_smul
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
z : 𝕜
h : HasSum (fun n => z ^ n • p.coeff n) (f (c + z))
⊢ HasSum (fun n => a • z ^ n • (p n) 1) (a • f (c + z))
Tactic:
exact h.const_smul a
Proof state after:
no goals
Theorem: analyticAt_iff_const_smul
Proof state before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
⊢ AnalyticAt 𝕜 (fun z => a • f z) c ↔ AnalyticAt 𝕜 f c
Tactic:
constructor
Proof state after:
case mp
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
⊢ AnalyticAt 𝕜 (fun z => a • f z) c → AnalyticAt 𝕜 f c

case mpr
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
⊢ AnalyticAt 𝕜 f c → AnalyticAt 𝕜 (fun z => a • f z) c
Theorem: analyticAt_iff_const_smul
Proof state before:
case mp
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
⊢ AnalyticAt 𝕜 (fun z => a • f z) c → AnalyticAt 𝕜 f c
Tactic:
intro ⟨p, fp⟩
Proof state after:
case mp
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt (fun z => a • f z) p c
⊢ AnalyticAt 𝕜 f c
Theorem: analyticAt_iff_const_smul
Proof state before:
case mp
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt (fun z => a • f z) p c
⊢ AnalyticAt 𝕜 f c
Tactic:
have e : f = fun z ↦ a⁻¹ • a • f z := by
  funext; simp only [← smul_assoc, smul_eq_mul, inv_mul_cancel a0, one_smul]
Proof state after:
case mp
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt (fun z => a • f z) p c
e : f = fun z => a⁻¹ • a • f z
⊢ AnalyticAt 𝕜 f c