internlm/Lean-Github huggingface dataset:
Theorem: Weight.pair_swap_le
Proof state before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a j * w i + a i * w j ≤ a j * w j + a i * w i
Tactic:
rw [add_comm (a j * w i), add_comm (a j * w j)]
Proof state after:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a i * w j + a j * w i ≤ a i * w i + a j * w j
Theorem: Weight.pair_swap_le
Proof state before:
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a i * w j + a j * w i ≤ a i * w i + a j * w j
Tactic:
exact mul_add_mul_le_mul_add_mul ha hw
Proof state after:
no goals
Theorem: Weight.pair_swap_le
Proof state before:
case haij
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
k : Fin (Nat.succ n)
hk : k ∈ erase (erase univ j) i
⊢ Weight.comp a (Equiv.swap i j) k = a k
Tactic:
rw [comp_apply,
    Equiv.swap_apply_of_ne_of_ne (ne_of_mem_erase hk)
                                 (ne_of_mem_erase (mem_of_mem_erase hk))]
Proof state after:
no goals
Theorem: Weight.pair_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) (Weight.comp a σ) = pair w a
Tactic:
simp only [Weight.comp, pair, Function.comp_apply]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ x : Fin (Nat.succ n), a (σ x) * w (σ x) = ∑ j : Fin (Nat.succ n), a j * w j
Theorem: Weight.pair_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ ∑ x : Fin (Nat.succ n), a (σ x) * w (σ x) = ∑ j : Fin (Nat.succ n), a j * w j
Tactic:
exact Fintype.sum_bijective σ (Equiv.bijective _) _ _ (fun k ↦ rfl)
Proof state after:
no goals
Theorem: Weight.pair_perm'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) a = pair w (Weight.comp a σ⁻¹)
Tactic:
rw [← pair_perm w _ σ]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) a = pair (Weight.comp w σ) (Weight.comp (Weight.comp a σ⁻¹) σ)
Theorem: Weight.pair_perm'
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ pair (Weight.comp w σ) a = pair (Weight.comp w σ) (Weight.comp (Weight.comp a σ⁻¹) σ)
Tactic:
simp only [comp_comp, mul_left_inv, comp_one]
Proof state after:
no goals
Theorem: Weight.pair_swap_eq
Proof state before:
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
⊢ pair w (Weight.comp a (Equiv.swap i j)) = pair (Weight.comp w (Equiv.swap i j)) a
Tactic:
convert (pair_perm' w a _).symm
Proof state after:
case h.e'_2.h.e'_4.h.e'_4
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
⊢ Equiv.swap i j = (Equiv.swap i j)⁻¹
Theorem: Weight.pair_swap_eq
Proof state before:
case h.e'_2.h.e'_4.h.e'_4
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
⊢ Equiv.swap i j = (Equiv.swap i j)⁻¹
Tactic:
simp only [Equiv.swap_inv]
Proof state after:
no goals
Theorem: Weight.pair_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ pair (k • 1) ↑a = k * d
Tactic:
simp only [pair, smul_apply, one_apply, mul_one]
Proof state after:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), ↑a x * k = k * d
Theorem: Weight.pair_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), ↑a x * k = k * d
Tactic:
rw [mul_comm k, ← Finset.sum_mul]
Proof state after:
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ (∑ i : Fin (Nat.succ n), ↑a i) * k = d * k
Theorem: Weight.tv_finset
Proof state before:
n d : ℕ
inst✝ : NeZero d
⊢ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) = testvecs n d
Tactic:
simp only [testvecs]
Proof state after:
n d : ℕ
inst✝ : NeZero d
⊢ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) = {w | Weight.sum w = d}
Theorem: Weight.tv_finset
Proof state before:
n d : ℕ
inst✝ : NeZero d
⊢ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) = {w | Weight.sum w = d}
Tactic:
ext a
Proof state after:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ a ∈ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) ↔ a ∈ {w | Weight.sum w = d}
Theorem: Weight.tv_finset
Proof state before:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ a ∈ ↑(Finset.Nat.antidiagonalTuple (Nat.succ n) d) ↔ a ∈ {w | Weight.sum w = d}
Tactic:
simp only [Finset.Nat.mem_antidiagonalTuple, Finset.mem_coe, Finset.mem_mk, Weight.sum]
Proof state after:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ ∑ i : Fin (Nat.succ n), a i = d ↔ a ∈ {w | ∑ j : Fin (Nat.succ n), w j = d}
Theorem: Weight.tv_finset
Proof state before:
case h
n d : ℕ
inst✝ : NeZero d
a : Fin (Nat.succ n) → ℕ
⊢ ∑ i : Fin (Nat.succ n), a i = d ↔ a ∈ {w | ∑ j : Fin (Nat.succ n), w j = d}
Tactic:
rfl
Proof state after:
no goals
Theorem: Weight.testvecs_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
a : Weight n d
ha : a ∈ testvecs n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ Weight.comp a σ ∈ testvecs n d
Tactic:
simpa only [testvecs, sum_perm, Set.mem_setOf_eq]
Proof state after:
no goals
Theorem: Weight.tw'_sum
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
k : Fin (Nat.succ n)
⊢ Weight.sum (tw' n d k) = d
Tactic:
simp only [Weight.sum, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply, mul_ite,
  mul_one, mul_zero, Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, ite_true]
Proof state after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
k : Fin (Nat.succ n)
⊢ d - 1 + 1 = d
Theorem: Weight.tw'_sum
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
k : Fin (Nat.succ n)
⊢ d - 1 + 1 = d
Tactic:
exact Nat.sub_add_cancel (Nat.one_le_of_lt (NeZero.pos d))
Proof state after:
no goals
Theorem: Weight.tw_inj
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
⊢ Function.Injective (tw n d)
Tactic:
intro j k h
Proof state after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : tw n d j = tw n d k
⊢ j = k
Theorem: Weight.tw_inj
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : tw n d j = tw n d k
⊢ j = k
Tactic:
simp only [tw, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Subtype.mk.injEq] at h
Proof state after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1 =
    (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1
⊢ j = k
Theorem: Weight.tw_inj
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1 =
    (fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1
⊢ j = k
Tactic:
replace h := congr_fun h k
Proof state after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1) k =
    ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1) k
⊢ j = k
Theorem: Weight.tw_inj
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h :
  ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 j 1) k =
    ((fun x => d - 1) * Function.update 0 0 1 + Function.update 0 k 1) k
⊢ j = k
Tactic:
simp only [ge_iff_le, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply,
  mul_ite, mul_one, mul_zero, Function.update_same, add_right_inj, ite_eq_left_iff, if_true] at h
Proof state after:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : ¬k = j → False
⊢ j = k
Theorem: Weight.tw_inj
Proof state before:
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : ¬k = j → False
⊢ j = k
Tactic:
exact (of_not_not h).symm
Proof state after:
no goals
Theorem: Weight.pair_tw
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : Fin (Nat.succ n)
⊢ pair w ↑(tw n d k) = (d - 1) * w 0 + w k
Tactic:
simp only [pair, tw, tw', ge_iff_le, nsmul_eq_mul, Pi.coe_nat, Nat.cast_tsub, Nat.cast_id,
  Nat.cast_one, Pi.add_apply, Pi.mul_apply, ne_eq, Function.update_apply, zero_apply, mul_ite,
  mul_one, mul_zero, add_mul, ite_mul, zero_mul, one_mul, Finset.sum_add_distrib,
  Finset.sum_ite_eq', Finset.mem_univ, ite_true]
Proof state after:
no goals
Theorem: Weight.one_le_E
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ 1 ≤ E w
Tactic:
simp only [E, le_add_iff_nonneg_left, zero_le']
Proof state after:
no goals
Theorem: Weight.E_perm
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
σ : Equiv.Perm (Fin (Nat.succ n))
⊢ E (Weight.comp w σ) = E w
Tactic:
simp only [E, sum_perm]
Proof state after:
no goals
Theorem: Weight.E_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ E (w + k • 1) = E w + k * d
Tactic:
simp only [E, Weight.sum, Nat.succ_eq_add_one, add_apply, smul_apply, one_apply, mul_one,
  Finset.sum_add_distrib, Finset.sum_const, Finset.card_fin, smul_eq_mul]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x + (n + 1) * k) * d / (n + 1) + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d
Theorem: Weight.E_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x + (n + 1) * k) * d / (n + 1) + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d
Tactic:
rw [add_mul, mul_assoc, Nat.add_mul_div_left _ _ (Nat.succ_pos n)]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x) * d / Nat.succ n + k * d + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d
Theorem: Weight.E_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ (∑ x : Fin (n + 1), w x) * d / Nat.succ n + k * d + 1 = (∑ x : Fin (n + 1), w x) * d / (n + 1) + 1 + k * d
Tactic:
abel
Proof state after:
no goals
Theorem: Weight.eval_f_tw
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : Fin (Nat.succ n)
⊢ f w (tw n d k) = E w - (d - 1) * w 0 - w k
Tactic:
simp only [f, pair, ge_iff_le, tsub_le_iff_right, Nat.sub_sub]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : Fin (Nat.succ n)
⊢ E w - ∑ j : Fin (Nat.succ n), ↑(tw n d k) j * w j = E w - ((d - 1) * w 0 + w k)
Theorem: Weight.f_eq_on_shift
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ f (w + k • 1) = f w
Tactic:
ext a
Proof state after:
case h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : ↑(testvecs n d)
⊢ f (w + k • 1) a = f w a
Theorem: Weight.f_eq_on_shift
Proof state before:
case h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : ↑(testvecs n d)
⊢ f (w + k • 1) a = f w a
Tactic:
simp only [f_apply, E_shift, pair_add_left, pair_shift, add_tsub_add_eq_tsub_right]
Proof state after:
no goals
Theorem: Weight.f_le_mul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ f w ≤ f (Nat.succ k • w)
Tactic:
simp only [E, f_le_iff, f_apply, sum_smul, pair_smul_left, SetCoe.forall, Subtype.coe_mk]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∀ x ∈ testvecs n d,
    Weight.sum w * d / (n + 1) + 1 - pair w x ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w x
Theorem: Weight.f_le_mul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∀ x ∈ testvecs n d,
    Weight.sum w * d / (n + 1) + 1 - pair w x ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w x
Tactic:
intro a _
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
Theorem: Weight.f_le_mul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
Tactic:
have H : w.sum * d / (n + 1) + 1 - w.pair a
           ≤ k.succ * (w.sum * d / (n + 1)) + 1 - k.succ * w.pair a
Proof state after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a

n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
Theorem: Weight.f_le_mul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
Tactic:
refine H.trans <| Nat.sub_le_sub_right (add_le_add_right ?_ _) _
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * Weight.sum w * d / (n + 1)
Theorem: Weight.f_le_mul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * Weight.sum w * d / (n + 1)
Tactic:
rw [mul_assoc]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * (Weight.sum w * d) / (n + 1)
Theorem: Weight.f_le_mul
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * (Weight.sum w * d) / (n + 1)
Tactic:
exact Nat.mul_div_le_mul_div_assoc ..
Proof state after:
no goals
Theorem: Weight.f_le_mul
Proof state before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
Tactic:
set m := w.sum * d / (n + 1)
Proof state after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
⊢ m + 1 - pair w a ≤ Nat.succ k * m + 1 - Nat.succ k * pair w a
Theorem: Weight.f_le_mul
Proof state before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
⊢ m + 1 - pair w a ≤ Nat.succ k * m + 1 - Nat.succ k * pair w a
Tactic:
set l := w.pair a
Proof state after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Theorem: Weight.f_le_mul
Proof state before:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
cases' lt_or_le m l with hlt hle
Proof state after:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l

case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Theorem: Weight.f_le_mul
Proof state before:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
rw [Nat.sub_eq_zero_of_le hlt]
Proof state after:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ 0 ≤ Nat.succ k * m + 1 - Nat.succ k * l
Theorem: Weight.f_le_mul
Proof state before:
case H.inl
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hlt : m < l
⊢ 0 ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Weight.f_le_mul
Proof state before:
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
Tactic:
rw [← tsub_add_eq_add_tsub hle, ← tsub_add_eq_add_tsub (mul_le_mul' le_rfl hle),
    ← Nat.mul_sub_left_distrib]
Proof state after:
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m - l + 1 ≤ Nat.succ k * (m - l) + 1
Theorem: Weight.f_le_mul
Proof state before:
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m - l + 1 ≤ Nat.succ k * (m - l) + 1
Tactic:
exact add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) 1
Proof state after:
no goals
Theorem: Weight.pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ pair' w (v a) = ↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)
Tactic:
simp [v, pair, pair', Weight.sum, Finset.mul_sum, Finset.sum_sub_distrib, sub_mul, mul_assoc]
Proof state after:
no goals
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : pair' w (v a) < 0
⊢ f w a = 0
Tactic:
simp only [pair'_v, sub_neg] at h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ f w a = 0
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ f w a = 0
Tactic:
simp only [f_apply, E, tsub_eq_zero_iff_le]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ Weight.sum w * d / (n + 1) + 1 ≤ pair w ↑a
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ Weight.sum w * d / (n + 1) + 1 ≤ pair w ↑a
Tactic:
zify
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 ≤ ↑(pair w ↑a)
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 ≤ ↑(pair w ↑a)
Tactic:
change ((Weight.sum w) * ↑d / (↑n + 1) : ℤ) < ↑(pair w ↑a)
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) < ↑(pair w ↑a)
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) < ↑(pair w ↑a)
Tactic:
apply Int.ediv_lt_of_lt_mul (by linarith)
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d < ↑(pair w ↑a) * (↑n + 1)
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ ↑(Weight.sum w) * ↑d < ↑(pair w ↑a) * (↑n + 1)
Tactic:
simp only [mul_comm, h]
Proof state after:
no goals
Theorem: Weight.f_apply_eq_zero_of_neg_pair'_v
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ 0 < ↑n + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : 0 ≤ pair' w (v a)
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
Tactic:
simp only [pair'_v, sub_nonneg] at h
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
Tactic:
have H : pair w a ≤ w.sum * d / (n + 1) + 1
Proof state after:
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1

n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
Tactic:
simp only [f_apply, E, ge_iff_le, pair'_v]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w * d / (n + 1) + 1 - pair w ↑a) = (↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)) / (↑n + 1) + 1
Theorem: Weight.f_apply_eq_pair'_v_of_nonneg
Proof state before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w * d / (n + 1) + 1 - pair w ↑a) = (↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)) / (↑n + 1) + 1
Tactic:
zify [H]
Proof state after:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1 - ↑(pair w ↑a) = (↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)) / (↑n + 1) + 1