Subsum condition for the odd case

def OddCase.redEmb1 {n : ℕ} : Fin 3 ↪ Fin (n + 5)

The embedding for the first subsum block reduction.

Equations

• OddCase.redEmb1 = { toFun := fun (i : Fin 3) => Fin.natAdd n (Fin.natAdd 2 i), inj' := ⋯ }

@[simp]

theorem OddCase.redEmb1_apply {n : ℕ} (i : Fin 3) : redEmb1 i = Fin.natAdd n (Fin.natAdd 2 i)

theorem OddCase.sum_redEmb1_compl {n : ℕ} {F : Finset ℕ} {x : ℤ} : ∑ i ∈ (Finset.map redEmb1 Finset.univ)ᶜ, (tup n F x i).natAbs = (VW n F).v + (VW n F).w + ∑ i ∈ Finset.range n, primeChain (max 8 (F.sup id)) i

theorem OddCase.sum_redEmb1_compl_lt {n : ℕ} {F : Finset ℕ} {x : ℤ} : ∑ i ∈ (Finset.map redEmb1 Finset.univ)ᶜ, (tup n F x i).natAbs < Y n F

theorem OddCase.b₂_upper_bound {x : ℤ} (hx : 2 ≤ x.natAbs) : (10 * (x ^ 2 + 1) ^ 2).natAbs ≤ 20 * x.natAbs ^ 4

theorem OddCase.b₁_lower_bound {x : ℤ} (hx : 26 ≤ x.natAbs) : 21 * x.natAbs ^ 4 ≤ ((x - 1) ^ 5).natAbs

theorem OddCase.b₃_lower_bound {x : ℤ} (hx : 26 ≤ x.natAbs) : 21 * x.natAbs ^ 4 ≤ ((x + 1) ^ 5).natAbs

theorem OddCase.natAbs_pow_le_redEmb1 {x : ℤ} {b₁ b₂ b₃ : SignType} (h : b₃ < b₁) (hx : 26 ≤ x.natAbs) : x.natAbs ^ 4 ≤ (↑b₁ * (x - 1) ^ 5 + ↑b₂ * (10 * (x ^ 2 + 1) ^ 2) + ↑b₃ * -(x + 1) ^ 5).natAbs

theorem OddCase.natAbs_le_redEmb1_reduced {x : ℤ} {b₁ b₂ : SignType} (h : b₁ ≠ b₂) (hx : 8 ≤ x.natAbs) : x.natAbs ≤ ((↑b₂ - ↑b₁) * (10 * (x ^ 2 + 1) ^ 2) + ↑b₁ * 8).natAbs

theorem OddCase.Y_le_natAbs_redEmb1 {n : ℕ} {F : Finset ℕ} {x : ℤ} {b₁ b₂ b₃ : SignType} (h : b₁ ≠ b₂ ∨ b₁ ≠ b₃) (hx : Y n F ≤ x.natAbs) : Y n F ≤ (↑b₁ * (x - 1) ^ 5 + ↑b₂ * (10 * (x ^ 2 + 1) ^ 2) + ↑b₃ * -(x + 1) ^ 5).natAbs

theorem OddCase.isSubsumBlock_redEmb1 {n : ℕ} {F : Finset ℕ} {x : ℤ} (hx : Y n F ≤ x.natAbs) : IsSubsumBlock (tup n F x) (Finset.map redEmb1 Finset.univ)

theorem OddCase.tupReduce_tup {n : ℕ} {F : Finset ℕ} {x : ℤ} {c₁ : n + 2 = n + 5 - (Finset.map redEmb1 Finset.univ).card} : tupReduce (tup n F x) (Finset.map redEmb1 Finset.univ) c₁ = vwTup (VW n F)

theorem OddCase.strongSSC_tup {n : ℕ} {F : Finset ℕ} {x : ℤ} (hx : Y n F ≤ x.natAbs) : StrongSSC (tup n F x)

theorem OddCase.maxAbs_tup {n : ℕ} {F : Finset ℕ} {x : ℕ} (hx : Y n F ≤ x) : maxAbs (tup n F ↑x) = (x + 1) ^ 5

When Y n F ≤ x, the maximum absolute value is (x + 1) ^ 5.