mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ ∃ s ∈ 𝓝 t₀, EqOn f g s

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ ∃ s ∈ 𝓝 t₀, EqOn f g s
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β ≤ (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ ∀ (x_1 : ↑(Icc tmin tmax)),
    dist ((toContinuousMap ((next hf hx)^[n] α)) x_1) ((toContinuousMap ((next hf hx)^[n] β)) x_1) ≤
      (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ ∀ (x_1 : ↑(Icc tmin tmax)),
    dist ((toContinuousMap ((next hf hx)^[n] α)) x_1) ((toContinuousMap ((next hf hx)^[n] β)) x_1) ≤
      (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
⊢ 0 ≤ (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ n / ↑n ! * dist α β
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ∑ i ∈ insert p.natDegree (range p.natDegree), p.coeff i * a ^ i = 0
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ∑ i ∈ insert p.natDegree (range p.natDegree), p.coeff i * a ^ i = 0
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x ↦ eval x P) atTop atTop
this : 0 < P.degree ∧ 0 < P.leadingCoeff
⊢ 0 < P.degree ∧ 0 ≤ P.leadingCoeff
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : P.degree ≤ 0 ∧ P.leadingCoeff = c
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x ↦ eval x P) atTop (𝓝 c)
this : P.degree ≤ 0 ∧ P.leadingCoeff = c
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = (-x✝) ^ (P.comp (-X)).natDegree * (-1) ^ P.natDegree * P.leadingCoeff

Tactic:
]

Goal state after:
case e'_6
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
x✝ : 𝕜
⊢ P.leadingCoeff * x✝ ^ P.natDegree = (-x✝) ^ (P.comp (-X)).natDegree * (-1) ^ P.natDegree * P.leadingCoeff
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
]

Goal state after:
case inr.inr
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : 1 < ‖a‖₊
⊢ ‖a‖₊ < p.cauchyBound
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 (?neg✝ * 0))

pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ 𝕜

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 (?neg✝ * 0))

case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ 𝕜
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
this : Nonempty ↑(Icc tmin tmax)
⊢ ⨆ x_1, ‖(toContinuousMap (next hf hx α) - toContinuousMap (next hf hy α)) x_1‖ = dist x y

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x y : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
hy : y ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
this : Nonempty ↑(Icc tmin tmax)
⊢ ⨆ x_1, ‖(toContinuousMap (next hf hx α) - toContinuousMap (next hf hy α)) x_1‖ = dist x y
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case pos.inl
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree

Tactic:
]

Goal state after:
case pos.inl
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    (∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨ ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨ ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    ∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[n] α) ≤
    ∑ i ∈ Finset.range n, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg.inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ 0 = 0
⊢ P.degree < Q.degree

Tactic:
]

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ 0 = 0
⊢ P.degree < Q.degree
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑Q.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun x ↦ P.leadingCoeff / Q.leadingCoeff * x ^ (↑Q.natDegree - ↑Q.natDegree)) atTop
    (𝓝 (P.leadingCoeff / Q.leadingCoeff))
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: p : ℂ[X]
this :
  ∑ b ∈ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support, ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1

pp: case eq_zero
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
⊢ ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 = 0

Tactic:
]

Goal state after:
p : ℂ[X]
this :
  ∑ b ∈ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support, ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
⊢ ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun θ ↦ ‖eval θ p‖ ^ 2) 0 1

case eq_zero
p : ℂ[X]
this :
  ∑' (i : ℤ), ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑↑((ContinuousMap.toLp 2 haarAddCircle ℂ) (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
⊢ ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ ^ 2 = 0
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop atTop

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop atTop
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i] (next hf hx α)) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[i] α) ((next hf hx)^[i] (next hf hx α)) ≤
    (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i ! * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop atBot

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atTop atBot
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range n, ↑C ^ i) *
      dist α (next hf hx α)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ((∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ∑ i ∈ Finset.range n, ↑C ^ i) *
      dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖a‖₊ ^ p.natDegree = ‖a‖₊ ^ p.natDegree

pp: case ha
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖p.leadingCoeff‖₊ ≠ 0

Tactic:
]

Goal state after:
case ha
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
⊢ ‖p.leadingCoeff‖₊ ≠ 0
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ∑ i ∈ Finset.range n,
      (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n : ℕ
⊢ dist ((next hf hx)^[0] α) ((next hf hx)^[m]^[n] α) ≤
    ∑ i ∈ Finset.range n,
      (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.CauchyBound

Goal state before:
pp: case h₁
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
x : ℕ
a✝ : x ∈ range p.natDegree
⊢ ‖p.coeff x‖₊ ≤ ‖p.leadingCoeff‖₊ * (((range p.natDegree).sup fun x ↦ ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊)

Tactic:
]

Goal state after:
case h₁
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree ≤ ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
pld : ‖p.leadingCoeff‖₊ ≠ 0
x : ℕ
a✝ : x ∈ range p.natDegree
⊢ ‖p.coeff x‖₊ ≤ ‖p.leadingCoeff‖₊ * (((range p.natDegree).sup fun x ↦ ‖p.coeff x‖₊) / ‖p.leadingCoeff‖₊)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i] ((next hf hx)^[m] α)) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist ((next hf hx)^[m]^[i] α) ((next hf hx)^[m]^[i] ((next hf hx)^[m] α)) ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * ↑C ^ i * dist α (next hf hx α)
Module: Mathlib.Analysis.Polynomial.Fourier

Goal state before:
pp: p : ℂ[X]
this :
  ∑ x ∈ p.support, ‖p.coeff x‖ ^ 2 =
    ∫ (t : AddCircle (2 * π)), ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle
t : AddCircle (2 * π)
ht : ↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t = (toAddCircle p) t
⊢ ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 =
    ‖↑(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : (P.comp (-X)).degree < (Q.comp (-X)).degree
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : (P.comp (-X)).degree < (Q.comp (-X)).degree
⊢ Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * ↑C ^ i ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α) * ↑C ^ i

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α : FunSpace t₀ x₀ r L
m : ℕ
C : ℝ≥0
hm : LipschitzWith C (next hf hx)^[m]
n i : ℕ
hi : i < n
⊢ dist α ((next hf hx)^[m] α) * ↑C ^ i ≤
    (∑ i ∈ Finset.range m, (↑K * max (tmax - ↑t₀) (↑t₀ - tmin)) ^ i / ↑i !) * dist α (next hf hx α) * ↑C ^ i
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x ↦ eval x P / eval x Q) atBot (𝓝 0)
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree