internlm/Lean-Github huggingface dataset:
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) Filter.atTop (nhds 0)
Tactic:
convert_to Filter.Tendsto (fun e : ℕ => ((e : ℝ) + 2)⁻¹ * ‖s.centroid ℝ id - x‖) Filter.atTop _
Proof state after:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) = fun e =>
    (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖

case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖) Filter.atTop (nhds 0)
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖) Filter.atTop (nhds 0)
Tactic:
suffices Filter.Tendsto (fun e : ℕ => (↑(e + 2) : ℝ)⁻¹) Filter.atTop (nhds 0) by
  simpa using this.mul_const _
Proof state after:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑(e + 2))⁻¹) Filter.atTop (nhds 0)
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => (↑(e + 2))⁻¹) Filter.atTop (nhds 0)
Tactic:
refine' tendsto_inv_atTop_zero.comp _
Proof state after:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ↑(e + 2)) Filter.atTop Filter.atTop
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => ↑(e + 2)) Filter.atTop Filter.atTop
Tactic:
rw [tendsto_natCast_atTop_iff]
Proof state after:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => e + 2) Filter.atTop Filter.atTop
Theorem: subset_closure_combiInterior
Proof state before:
case a.refine'_3.convert_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ Filter.Tendsto (fun e => e + 2) Filter.atTop Filter.atTop
Tactic:
apply Filter.tendsto_add_atTop_nat
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof state before:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
⊢ (fun e => ‖(↑e + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑e + 2)⁻¹) • x - x‖) = fun e =>
    (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖
Tactic:
ext n
Proof state after:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ‖(↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x - x‖ = (↑n + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖
Theorem: subset_closure_combiInterior
Proof state before:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ ‖(↑n + 2)⁻¹ • Finset.centroid ℝ s id + (1 - (↑n + 2)⁻¹) • x - x‖ = (↑n + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖
Tactic:
rw [add_sub_assoc, sub_smul, sub_right_comm, one_smul, sub_self, zero_sub, ← smul_neg, ←
  smul_add, norm_smul_of_nonneg, ← sub_eq_add_neg]
Proof state after:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ (↑n + 2)⁻¹
Theorem: subset_closure_combiInterior
Proof state before:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ (↑n + 2)⁻¹
Tactic:
rw [inv_nonneg]
Proof state after:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ ↑n + 2
Theorem: subset_closure_combiInterior
Proof state before:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ ↑n + 2
Tactic:
norm_cast
Proof state after:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ n + 2
Theorem: subset_closure_combiInterior
Proof state before:
case h.e'_3.h.ht
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
n : ℕ
⊢ 0 ≤ n + 2
Tactic:
apply Nat.zero_le
Proof state after:
no goals
Theorem: subset_closure_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s t : Finset E
hs : AffineIndependent ℝ Subtype.val
x : E
hx : x ∈ s
hsnonempty : s.Nonempty
centroid_weights : ∑ i ∈ s, Finset.centroidWeights ℝ s i = 1
this : Filter.Tendsto (fun e => (↑(e + 2))⁻¹) Filter.atTop (nhds 0)
⊢ Filter.Tendsto (fun e => (↑e + 2)⁻¹ * ‖Finset.centroid ℝ s id - x‖) Filter.atTop (nhds 0)
Tactic:
simpa using this.mul_const _
Proof state after:
no goals
Theorem: closure_combiInterior_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) = (convexHull ℝ) ↑s
Tactic:
refine'
  Set.Subset.antisymm _
    (convexHull_min (subset_closure_combiInterior hs) (convex_combiInterior hs).closure)
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑s
Theorem: closure_combiInterior_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑s
Tactic:
rw [s.isClosed_convexHull.closure_subset_iff]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ (convexHull ℝ) ↑s
Theorem: closure_combiInterior_eq_convexHull
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ (convexHull ℝ) ↑s
Tactic:
exact combiInterior_subset_convexHull
Proof state after:
no goals
Theorem: convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
Tactic:
rw [← closure_combiInterior_eq_convexHull hs]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t
Theorem: convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t
Tactic:
rw [← closure_combiInterior_eq_convexHull ht]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)
Theorem: convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)
Tactic:
intro h
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
h : combiInterior ℝ s ⊆ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)
Theorem: convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
ht : AffineIndependent ℝ Subtype.val
h : combiInterior ℝ s ⊆ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)
Tactic:
apply closure_mono h
Proof state after:
no goals
Theorem: Polynomial.discConv_single
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P : R[X]
r : R
s : S
⊢ discConv (fun₀ | r => s) P = s • P.comp (X + C r)
Tactic:
simp [discConv]
Proof state after:
no goals
Theorem: Polynomial.discConv_zero
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P : R[X]
w : R →₀ S
⊢ discConv w 0 = 0
Tactic:
simp [discConv]
Proof state after:
no goals
Theorem: Polynomial.discConv_add
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P Q : R[X]
⊢ discConv w (P + Q) = discConv w P + discConv w Q
Tactic:
simp [discConv]
Proof state after:
no goals
Theorem: Polynomial.discConv_sub
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P Q : R[X]
⊢ discConv w (P - Q) = discConv w P - discConv w Q
Tactic:
simp [discConv, smul_sub]
Proof state after:
no goals
Theorem: Polynomial.discConv_neg
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P : R[X]
⊢ discConv w (-P) = -discConv w P
Tactic:
simp [discConv]
Proof state after:
no goals
Theorem: Polynomial.discConv_sum
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
s : Finset ι
P : ι → R[X]
⊢ discConv w (∑ i ∈ s, P i) = ∑ i ∈ s, discConv w (P i)
Tactic:
simp [discConv, smul_sum, Finsupp.sum]
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
s : Finset ι
P : ι → R[X]
⊢ ∑ x ∈ w.support, ∑ x_1 ∈ s, w x • (P x_1).comp (X + C x) = ∑ x ∈ s, ∑ x_1 ∈ w.support, w x_1 • (P x).comp (X + C x_1)
Theorem: Polynomial.discConv_sum
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
s : Finset ι
P : ι → R[X]
⊢ ∑ x ∈ w.support, ∑ x_1 ∈ s, w x • (P x_1).comp (X + C x) = ∑ x ∈ s, ∑ x_1 ∈ w.support, w x_1 • (P x).comp (X + C x_1)
Tactic:
exact Finset.sum_comm
Proof state after:
no goals
Theorem: Polynomial.discConv_zero_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
⊢ discConv 0 P = 0
Tactic:
simp [discConv]
Proof state after:
no goals
Theorem: Polynomial.discConv_add_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : R →₀ S
P : R[X]
⊢ ∀ (a : R), 0 • P.comp (X + C a) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.discConv_add_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : R →₀ S
P : R[X]
⊢ ∀ (a : R) (b₁ b₂ : S), (b₁ + b₂) • P.comp (X + C a) = b₁ • P.comp (X + C a) + b₂ • P.comp (X + C a)
Tactic:
simp [add_smul]
Proof state after:
no goals
Theorem: Polynomial.discConv_sub_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : R →₀ S
P : R[X]
⊢ ∀ (a : R) (b₁ b₂ : S), (b₁ - b₂) • P.comp (X + C a) = b₁ • P.comp (X + C a) - b₂ • P.comp (X + C a)
Tactic:
simp [sub_smul]
Proof state after:
no goals
Theorem: Polynomial.discConv_neg_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P : R[X]
⊢ ∀ (a : R), 0 • P.comp (X + C a) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.discConv_neg_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P : R[X]
⊢ (w.sum fun a b => -b • P.comp (X + C a)) = -discConv w P
Tactic:
simp [discConv]
Proof state after:
no goals
Theorem: Polynomial.discConv_sum_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
s : Finset ι
w : ι → R →₀ S
P : R[X]
⊢ ∀ (i : R), 0 • P.comp (X + C i) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.discConv_sum_weight
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
s : Finset ι
w : ι → R →₀ S
P : R[X]
⊢ ∀ (i : R) (x y : S), (x + y) • P.comp (X + C i) = x • P.comp (X + C i) + y • P.comp (X + C i)
Tactic:
simp [add_smul]
Proof state after:
no goals
Theorem: Polynomial.eval_discConv
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P : R[X]
x : R
⊢ eval x (discConv w P) = w.sum fun r s => s • eval (x + r) P
Tactic:
simp [discConv, Finsupp.sum,eval_finset_sum]
Proof state after:
no goals
Theorem: Polynomial.eval_discForwardDiff
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
x : R
⊢ eval x P.discForwardDiff = eval (x + 1) P - eval x P
Tactic:
simp_rw [discForwardDiff, discConv_sub_weight, discConv_single]
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
x : R
⊢ eval x (1 • P.comp (X + C 1) - 1 • P.comp (X + C 0)) = eval (x + 1) P - eval x P
Theorem: Polynomial.eval_discForwardDiff
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
x : R
⊢ eval x (1 • P.comp (X + C 1) - 1 • P.comp (X + C 0)) = eval (x + 1) P - eval x P
Tactic:
simp
Proof state after:
no goals
Theorem: Polynomial.eval_discBackwardDiff
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
x : R
⊢ eval x P.discBackwardDiff = eval x P - eval (x - 1) P
Tactic:
simp_rw [discBackwardDiff, discConv_sub_weight, discConv_single]
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
x : R
⊢ eval x (1 • P.comp (X + C 0) - 1 • P.comp (X + C (-1))) = eval x P - eval (x - 1) P
Theorem: Polynomial.eval_discBackwardDiff
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w : R →₀ S
P✝ P : R[X]
x : R
⊢ eval x (1 • P.comp (X + C 0) - 1 • P.comp (X + C (-1))) = eval x P - eval (x - 1) P
Tactic:
simp [sub_eq_add_neg]
Proof state after:
no goals
Theorem: Polynomial.discConv_discConv
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : AddMonoidAlgebra S R
P : R[X]
⊢ discConv v (discConv w P) = discConv (v * w) P
Tactic:
simp [discConv]
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : AddMonoidAlgebra S R
P : R[X]
⊢ (Finsupp.sum v fun r s => s • (Finsupp.sum w fun r s => s • P.comp (X + C r)).comp (X + C r)) =
    Finsupp.sum (v * w) fun r s => s • P.comp (X + C r)
Theorem: Polynomial.discConv_discConv
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
v w : AddMonoidAlgebra S R
P : R[X]
⊢ (Finsupp.sum v fun r s => s • (Finsupp.sum w fun r s => s • P.comp (X + C r)).comp (X + C r)) =
    Finsupp.sum (v * w) fun r s => s • P.comp (X + C r)
Tactic:
sorry
Proof state after:
no goals
Theorem: Polynomial.coeff_discConv_natDegree
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra S R
w✝ : R →₀ S
P✝ : R[X]
w : R →₀ S
P : R[X]
⊢ (discConv w P).coeff P.natDegree = (w.sum fun x => id) • P.leadingCoeff
Tactic:
sorry
Proof state after:
no goals
Theorem: Polynomial.discForwardDiff_aux
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra S R
w : R →₀ S
P : R[X]
inst✝ : Nontrivial S
⊢ (((fun₀ | 1 => 1) - fun₀ | 0 => 1).sum fun x => id) = 0
Tactic:
classical simp [Finsupp.sum_sub_index, -Finsupp.single_neg]
Proof state after:
no goals
Theorem: Polynomial.discForwardDiff_aux
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra S R
w : R →₀ S
P : R[X]
inst✝ : Nontrivial S
⊢ (((fun₀ | 1 => 1) - fun₀ | 0 => 1).sum fun x => id) = 0
Tactic:
simp [Finsupp.sum_sub_index, -Finsupp.single_neg]
Proof state after:
no goals
Theorem: Polynomial.discBackwardDiff_aux
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra S R
w : R →₀ S
P : R[X]
inst✝ : Nontrivial S
⊢ (((fun₀ | 0 => 1) - fun₀ | -1 => 1).sum fun x => id) = 0
Tactic:
classical simp [Finsupp.sum_sub_index, -Finsupp.single_neg]
Proof state after:
no goals
Theorem: Polynomial.discBackwardDiff_aux
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra S R
w : R →₀ S
P : R[X]
inst✝ : Nontrivial S
⊢ (((fun₀ | 0 => 1) - fun₀ | -1 => 1).sum fun x => id) = 0
Tactic:
simp [Finsupp.sum_sub_index, -Finsupp.single_neg]
Proof state after:
no goals
Theorem: Polynomial.natDegree_discConv_le
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w P).natDegree ≤ P.natDegree
Tactic:
refine' (natDegree_sum_le _ _).trans $ Finset.sup_le fun r _ ↦ _
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (natDegree ∘ fun a => (fun r s => s • P.comp (X + C r)) a (w a)) r ≤ P.natDegree
Theorem: Polynomial.natDegree_discConv_le
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (natDegree ∘ fun a => (fun r s => s • P.comp (X + C r)) a (w a)) r ≤ P.natDegree
Tactic:
dsimp
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (w r • P.comp (X + C r)).natDegree ≤ P.natDegree
Theorem: Polynomial.natDegree_discConv_le
Proof state before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (w r • P.comp (X + C r)).natDegree ≤ P.natDegree
Tactic:
simp_rw [algebra_compatible_smul R (w r)]
Proof state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ ((algebraMap S R) (w r) • P.comp (X + C r)).natDegree ≤ P.natDegree