internlm/Lean-Github huggingface dataset:
Theorem: FormalMultilinearSeries.unshift_radius'
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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r = ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
apply le_antisymm
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup₂_le ?_
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro r k
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_le ?_
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro h
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine le_trans ?_ (le_iSup₂ r (k * ↑r⁻¹))
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
have h := fun n ↦ mul_le_mul_of_nonneg_right (h (n + 1)) (NNReal.coe_nonneg r⁻¹)
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
by_cases r0 : r = 0
Proof state after:
case pos
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r

case neg
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : ¬r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case neg
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : ¬r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
simp only [pow_succ, ←mul_assoc _ _ (r:ℝ), mul_assoc _ (r:ℝ) _,
  mul_inv_cancel (NNReal.coe_ne_zero.mpr r0), NNReal.coe_inv, mul_one, p.unshift_norm'] at h
Proof state after:
case neg
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case neg
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
simp only [NNReal.coe_inv]
Proof state after:
case neg
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case neg
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹), ↑r
Tactic:
convert le_iSup _ h
Proof state after:
case h.e'_3
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r = ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case h.e'_3
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r = ↑r
Tactic:
rfl
Proof state after:
no goals
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case pos
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
simp only [r0, ENNReal.coe_zero, ENNReal.iSup_zero_eq_zero, le_zero_iff]
Proof state after:
no goals
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup₂_le ?_
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro r k
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_le ?_
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro h
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Theorem: FormalMultilinearSeries.unshift_radius'
Proof state before:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine le_trans ?_ (le_iSup₂ r (max ‖c‖ (k * ↑r)))
Proof state after:
case a
𝕜 : 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
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)), ↑r