internlm/Lean-Github huggingface dataset:
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
⊢ ∀ (n : ℕ), ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Tactic:
intro n
Proof state after:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Tactic:
specialize th n
Proof state after:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Tactic:
rw [unevenSeries_eq u u.r1p (le_refl _) z1s] at th
Proof state after:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
⊢ ‖unevenSeries u z1 n‖ ≤ max 1 c * s⁻¹ ^ n
Tactic:
generalize hy : ‖unevenSeries u z1 n‖ = y
Proof state after:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
y : ℝ
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
th : ‖unevenSeries u z1 n‖ * ↑t ^ n ≤ c
y : ℝ
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n
Tactic:
rw [hy] at th
Proof state after:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
⊢ y ≤ max 1 c * s⁻¹ ^ n
Tactic:
have tnz : (t : ℝ) ^ n ≠ 0 := pow_ne_zero _ (lt_trans sp st').ne'
Proof state after:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y ≤ max 1 c * s⁻¹ ^ n
Theorem: unevenSeries_nonuniform_bound
Proof state before:
case right
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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y ≤ max 1 c * s⁻¹ ^ n
Tactic:
calc
  y = y * (↑t ^ n * (↑t ^ n)⁻¹) := by simp only [mul_inv_cancel tnz, mul_one]
  _ = y * ↑t ^ n * (↑t ^ n)⁻¹ := by ring
  _ ≤ c * (↑t ^ n)⁻¹ := by bound
  _ ≤ c * (s ^ n)⁻¹ := by bound
  _ = c * s⁻¹ ^ n := by simp only [inv_pow]
  _ ≤ max 1 c * s⁻¹ ^ n := by bound
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
⊢ s < ↑t
Tactic:
rw [← ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_lt_ofReal_iff_of_nonneg sp.le] at st
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : s < ↑t
⊢ s < ↑t
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : s < ↑t
⊢ s < ↑t
Tactic:
exact st
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
⊢ ‖unevenSeries' u r1 z1 0‖ * ↑t ^ 0 ≥ 0
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
th : ∀ (n : ℕ), ‖unevenSeries' u r1 z1 n‖ * ↑t ^ n ≤ c
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y = y * (↑t ^ n * (↑t ^ n)⁻¹)
Tactic:
simp only [mul_inv_cancel tnz, mul_one]
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y * (↑t ^ n * (↑t ^ n)⁻¹) = y * ↑t ^ n * (↑t ^ n)⁻¹
Tactic:
ring
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ y * ↑t ^ n * (↑t ^ n)⁻¹ ≤ c * (↑t ^ n)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ c * (↑t ^ n)⁻¹ ≤ c * (s ^ n)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ c * (s ^ n)⁻¹ = c * s⁻¹ ^ n
Tactic:
simp only [inv_pow]
Proof state after:
no goals
Theorem: unevenSeries_nonuniform_bound
Proof 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
s : ℝ
sp : s > 0
sr1 : s < r1
z1s : z1 ∈ closedBall c1 r1
sr : ¬ENNReal.ofReal r1 ≤ ENNReal.ofReal s
t : ℝ≥0
c : ℝ
st : ENNReal.ofReal s < ↑t
st' : s < ↑t
cp : c ≥ 0
n : ℕ
y : ℝ
th : y * ↑t ^ n ≤ c
hy : ‖unevenSeries u z1 n‖ = y
tnz : ↑t ^ n ≠ 0
⊢ c * s⁻¹ ^ n ≤ max 1 c * s⁻¹ ^ n
Tactic:
bound
Proof state after:
no goals
Theorem: Along0.norm
Proof 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.along0‖ ≤ ‖p‖
Tactic:
have pp : 0 ≤ ‖p‖ := by bound
Proof 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
pp : 0 ≤ ‖p‖
⊢ ‖p.along0‖ ≤ ‖p‖
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
⊢ ‖p.along0‖ ≤ ‖p‖
Tactic:
apply p.along0.opNorm_le_bound pp
Proof 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
pp : 0 ≤ ‖p‖
⊢ ∀ (m : Fin n → ℂ), ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
⊢ ∀ (m : Fin n → ℂ), ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖
Tactic:
intro m
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p.along0 m‖ ≤ ‖p‖ * Finset.univ.prod fun i => ‖m i‖
Tactic:
simp only [ContinuousMultilinearMap.along0,
  ContinuousMultilinearMap.compContinuousLinearMap_apply, Complex.norm_eq_abs]
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)
Tactic:
have e : ∀ i : Fin n, abs (m i) = ‖idZeroLm (m i)‖ := by
  intro i
  simp only [idZeroLm, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
    ContinuousLinearMap.zero_apply, Prod.norm_def, Complex.norm_eq_abs, norm_zero, ge_iff_le,
    apply_nonneg, max_eq_left]
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => Complex.abs (m x)
Tactic:
simp_rw [e]
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => ‖idZeroLm (m x)‖
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
e : ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
⊢ ‖p fun i => idZeroLm (m i)‖ ≤ ‖p‖ * Finset.univ.prod fun x => ‖idZeroLm (m x)‖
Tactic:
exact ContinuousMultilinearMap.le_opNorm p _
Proof state after:
no goals
Theorem: Along0.norm
Proof 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
⊢ 0 ≤ ‖p‖
Tactic:
bound
Proof state after:
no goals
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
⊢ ∀ (i : Fin n), Complex.abs (m i) = ‖idZeroLm (m i)‖
Tactic:
intro i
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
i : Fin n
⊢ Complex.abs (m i) = ‖idZeroLm (m i)‖
Theorem: Along0.norm
Proof 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
pp : 0 ≤ ‖p‖
m : Fin n → ℂ
i : Fin n
⊢ Complex.abs (m i) = ‖idZeroLm (m i)‖
Tactic:
simp only [idZeroLm, ContinuousLinearMap.prod_apply, ContinuousLinearMap.coe_id', id_eq,
  ContinuousLinearMap.zero_apply, Prod.norm_def, Complex.norm_eq_abs, norm_zero, ge_iff_le,
  apply_nonneg, max_eq_left]
Proof state after:
no goals
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
⊢ p.radius ≤ p.along0.radius
Tactic:
simp_rw [FormalMultilinearSeries.radius]
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_mono ?_
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
⊢ ∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ C), ↑i ≤ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑i ^ n ≤ C), ↑i
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
⊢ ∀ (i : ℝ≥0), ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ C), ↑i ≤ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑i ^ n ≤ C), ↑i
Tactic:
intro r
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
⊢ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r
Theorem: Along0.radius
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
⊢ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_mono ?_
Proof 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 : ℝ
p : FormalMultilinearSeries ℂ (ℂ × ℂ) E
r : ℝ≥0
⊢ ∀ (i : ℝ), ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.along0 n‖ * ↑r ^ n ≤ i), ↑r