Theorem: analyticAt_iff_const_smul (Ray/Analytic/Analytic.lean)

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
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

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⟩
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

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]
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

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
e : f = fun z => a⁻¹ • a • f z
⊢ AnalyticAt 𝕜 f c
Tactic:
rw [e]
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 𝕜 (fun z => a⁻¹ • a • f z) c

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
e : f = fun z => a⁻¹ • a • f z
⊢ AnalyticAt 𝕜 (fun z => a⁻¹ • a • f z) c
Tactic:
exact ⟨_, fp.const_smul⟩
State after:
no goals

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
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt (fun z => a • f z) p c
⊢ f = fun z => a⁻¹ • a • f z
Tactic:
funext
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
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt (fun z => a • f z) p c
x✝ : 𝕜
⊢ f x✝ = a⁻¹ • a • f x✝

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
f : 𝕜 → E
c a : 𝕜
a0 : a ≠ 0
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt (fun z => a • f z) p c
x✝ : 𝕜
⊢ f x✝ = a⁻¹ • a • f x✝
Tactic:
simp only [← smul_assoc, smul_eq_mul, inv_mul_cancel a0, one_smul]
State after:
no goals

State before:
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
Tactic:
intro ⟨p, fp⟩
State after:
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
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ AnalyticAt 𝕜 (fun z => a • f z) c

State before:
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
p : FormalMultilinearSeries 𝕜 𝕜 E
fp : HasFPowerSeriesAt f p c
⊢ AnalyticAt 𝕜 (fun z => a • f z) c
Tactic:
exact ⟨_, fp.const_smul⟩
State after:
no goals