Theorem: LO.FirstOrder.Arith.Model.Nuon.polyI_hash_self_polybounded (Arithmetization/OmegaOne/Nuon.lean)

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (polyI A # polyI A) ((√‖A‖ + 1) ^ 2) = polyI A # polyI A
Tactic:
simpa [sq, len_polyI pos] using bexp_eq_hash (polyI A) (polyI A)
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (√‖A‖ + 1) ^ 2 < ‖polyI A # polyI A‖
Tactic:
simp [length_hash, lt_succ_iff_le, ←sq, len_polyI pos]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (2 * √‖A‖) ^ 2 < ‖(2 * A) # (2 * A)‖
Tactic:
simp [length_hash, lt_succ_iff_le, ←sq, len_polyI pos, length_two_mul_of_pos pos]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (√‖A‖ + 1) ^ 2 ≤ (2 * √‖A‖) ^ 2
Tactic:
simp [two_mul, ←pos_iff_one_le, pos]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp ((2 * A) # (2 * A)) ((2 * √‖A‖) ^ 2) ≤ bexp ((2 * A) # (2 * A)) (4 * (√‖A‖) ^ 2)
Tactic:
simp [mul_pow, two_pow_two_eq_four]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ 4 * (√‖A‖) ^ 2 < ‖(2 * A) # (2 * A)‖
Tactic:
simp [length_hash, lt_succ_iff_le, ←sq, len_polyI pos, length_two_mul_of_pos pos, ←two_pow_two_eq_four, ←mul_pow]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (√‖A‖) ^ 2 < ‖A # 1‖
Tactic:
simp [length_hash, lt_succ_iff_le]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (A # 1) ((√‖A‖) ^ 2) ^ 4 ≤ bexp (A # 1) ‖A‖ ^ 4
Tactic:
simp
State after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (A # 1) ((√‖A‖) ^ 2) ≤ bexp (A # 1) ‖A‖

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (A # 1) ((√‖A‖) ^ 2) ≤ bexp (A # 1) ‖A‖
Tactic:
exact (bexp_monotone_le (by simp [length_hash, lt_succ_iff_le]) (by simp [length_hash, lt_succ_iff_le])).mpr (by simp)
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ ‖A‖ < ‖A # 1‖
Tactic:
simp [length_hash, lt_succ_iff_le]
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (√‖A‖) ^ 2 ≤ ‖A‖
Tactic:
simp
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (A # 1) ‖A‖ ^ 4 = (A # 1) ^ 4
Tactic:
congr 1
State after:
case e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (A # 1) ‖A‖ = A # 1

State before:
case e_a
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ bexp (A # 1) ‖A‖ = A # 1
Tactic:
simpa using bexp_eq_hash A 1
State after:
no goals

State before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
pos : 0 < A
⊢ (A # 1) ^ 4 ≤ (2 * A + 1) ^ 4
Tactic:
simp
State after:
no goals