Algebra shared by the below-two and above-two residual identities

The weighted reversal, pairing and triangular-sum identities depend on the residual map and recurrence, independently of the coefficient regime.

noncomputable def V7.ResidualAlgebra.forwardC {d : ℕ} (n : ℕ) (u : ScalarSeq) (A : VectorSeq d) : VectorSeq d

Weighted reversal obtained by accumulating the residual increments.

Equations

• V7.ResidualAlgebra.forwardC n u A k = Nat.rec (u n • A n) (fun (j : ℕ) (previous : V7.Point d) => if j < n then previous + u (n - j - 1) • (A (n - j - 1) - A (n - j)) else previous) k

theorem V7.ResidualAlgebra.forwardC_zero {d : ℕ} (n : ℕ) (u : ScalarSeq) (A : VectorSeq d) : forwardC n u A 0 = u n • A n

theorem V7.ResidualAlgebra.forwardC_succ {d : ℕ} (n : ℕ) (u : ScalarSeq) (A : VectorSeq d) (k : ℕ) (hk : k < n) : forwardC n u A (k + 1) = forwardC n u A k + u (n - k - 1) • (A (n - k - 1) - A (n - k))

theorem V7.ResidualAlgebra.forward_map {d : ℕ} (n : ℕ) (u : ScalarSeq) (A B : VectorSeq d) : BelowResidualMap n u A B (forwardC n u A) fun (i : ℕ) => B (n - i)

noncomputable def V7.ResidualAlgebra.inverseRev {d : ℕ} (n : ℕ) (u : ScalarSeq) (C : VectorSeq d) : VectorSeq d

Reconstruct the reversed primal sequence from weighted residual increments.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.ResidualAlgebra.inverseRev_zero {d : ℕ} (n : ℕ) (u : ScalarSeq) (C : VectorSeq d) : inverseRev n u C 0 = (1 / u n) • C 0

theorem V7.ResidualAlgebra.inverseRev_succ {d : ℕ} (n : ℕ) (u : ScalarSeq) (C : VectorSeq d) (k : ℕ) (hk : k < n) : inverseRev n u C (k + 1) = inverseRev n u C k + (1 / u (n - k - 1)) • (C (k + 1) - C k)

noncomputable def V7.ResidualAlgebra.inverseA {d : ℕ} (n : ℕ) (u : ScalarSeq) (C : VectorSeq d) : VectorSeq d

Return the reconstructed primal sequence in its original index order.

Equations

• V7.ResidualAlgebra.inverseA n u C i = V7.ResidualAlgebra.inverseRev n u C (n - i)

theorem V7.ResidualAlgebra.map_determined_forward {d : ℕ} (n : ℕ) (u : ScalarSeq) (A B C D : VectorSeq d) (hmap : BelowResidualMap n u A B C D) : SameOnHorizon n C (forwardC n u A) ∧ SameOnHorizon n D fun (i : ℕ) => B (n - i)

theorem V7.ResidualAlgebra.pairing_smul_left {d : ℕ} (r : ℝ) (x y : Point d) : O3.pairing (r • x) y = r * O3.pairing x y

theorem V7.ResidualAlgebra.pairing_smul_right {d : ℕ} (r : ℝ) (x y : Point d) : O3.pairing x (r • y) = r * O3.pairing x y

theorem V7.ResidualAlgebra.pairing_add_left {d : ℕ} (x y z : Point d) : O3.pairing (x + y) z = O3.pairing x z + O3.pairing y z

theorem V7.ResidualAlgebra.pairing_sub_left {d : ℕ} (x y z : Point d) : O3.pairing (x - y) z = O3.pairing x z - O3.pairing y z

theorem V7.ResidualAlgebra.pairing_sub_right {d : ℕ} (x y z : Point d) : O3.pairing x (y - z) = O3.pairing x y - O3.pairing x z

theorem V7.ResidualAlgebra.pairing_weightedSum_left {d : ℕ} (m : ℕ) (a : ScalarSeq) (X : VectorSeq d) (y : Point d) : O3.pairing (weightedSum m a X) y = ∑ i ∈ Finset.range m, a i * O3.pairing (X i) y

theorem V7.ResidualAlgebra.pairing_weightedSum_right {d : ℕ} (m : ℕ) (a : ScalarSeq) (X : VectorSeq d) (y : Point d) : O3.pairing y (weightedSum m a X) = ∑ i ∈ Finset.range m, a i * O3.pairing y (X i)

theorem V7.ResidualAlgebra.pairing_abel {d : ℕ} (n : ℕ) (Y X : VectorSeq d) : ∑ k ∈ Finset.range (n + 1), O3.pairing (Y k - Y (k + 1)) (X k) = O3.pairing (Y 0) (X 0) + ∑ k ∈ Finset.range n, O3.pairing (Y (k + 1)) (X (k + 1) - X k) - O3.pairing (Y (n + 1)) (X n)

theorem V7.ResidualAlgebra.triangle_sum {E : Type u_1} [AddCommMonoid E] (f : ℕ → ℕ → E) (n : ℕ) : ∑ j ∈ Finset.range (n + 1), ∑ l ∈ Finset.range (n - j + 1), f (j + l) j = ∑ r ∈ Finset.range (n + 1), ∑ j ∈ Finset.range (r + 1), f r j

noncomputable def V7.ResidualAlgebra.dualP {d : ℕ} (n : ℕ) (u : ScalarSeq) (C : VectorSeq d) (k : ℕ) : Point d

Dual sequence expressed by the weighted summation-by-parts formula.

Equations

• V7.ResidualAlgebra.dualP n u C k = (1 / u (n - (k + 1))) • C (k + 1) - V7.weightedSum (k + 1) (fun (j : ℕ) => 1 / u (n - (j + 1)) - 1 / u (n - j)) C

theorem V7.ResidualAlgebra.dualP_succ {d : ℕ} (n : ℕ) (u : ScalarSeq) (C : VectorSeq d) (k : ℕ) : dualP n u C (k + 1) = dualP n u C k + (1 / u (n - (k + 2))) • (C (k + 2) - C (k + 1))

theorem V7.ResidualAlgebra.omega_block {d : ℕ} (n : ℕ) (Omega : Point d → ℝ) (heven : EvenIncrement Omega) (B D : VectorSeq d) (hD : ∀ i ≤ n, D i = B (n - i)) : ∑ k ∈ Finset.range n, Omega (B k - B (k + 1)) = ∑ k ∈ Finset.range n, Omega (D k - D (k + 1))

theorem V7.ResidualAlgebra.b_block {d : ℕ} (n : ℕ) (u : ScalarSeq) (b : ScalarMatrix) (A B C D X : VectorSeq d) (hb00 : b 0 0 = -1) (hAn : A (n + 1) = 0) (hX : BelowXRecurrence n b B X) (hmap : BelowResidualMap n u A B C D) : -∑ k ∈ Finset.range (n + 1), u k * O3.pairing (A k - A (k + 1)) (X k) = ∑ k ∈ Finset.range (n + 1), O3.pairing (weightedSum (k + 1) (fun (i : ℕ) => b (n - i) (n - k)) C) (D k)

theorem V7.ResidualAlgebra.sum_succ_sub {E : Type u_1} [AddCommGroup E] (n : ℕ) (f : ℕ → E) : ∑ k ∈ Finset.range n, (f (k + 1) - f k) = f n - f 0

theorem V7.ResidualAlgebra.sum_shift_end {E : Type u_1} [AddCommMonoid E] (n : ℕ) (f : ℕ → E) : f 0 + ∑ k ∈ Finset.range n, f (k + 1) = ∑ k ∈ Finset.range n, f k + f n

theorem V7.ResidualAlgebra.pairing_add_right {d : ℕ} (a b c : Point d) : O3.pairing a (b + c) = O3.pairing a b + O3.pairing a c

theorem V7.ResidualAlgebra.pairing_finset_sum_left {ι : Type u_1} {d : ℕ} (s : Finset ι) (f : ι → Point d) (z : Point d) : O3.pairing (∑ i ∈ s, f i) z = ∑ i ∈ s, O3.pairing (f i) z

theorem V7.ResidualAlgebra.sum_pairing_by_parts {d : ℕ} (n : ℕ) (u : ScalarSeq) (A X : VectorSeq d) : ∑ k ∈ Finset.range (n + 1), u k * O3.pairing (A k - A (k + 1)) (X k) = u 0 * O3.pairing (A 0) (X 0) + ∑ k ∈ Finset.range n, O3.pairing (A (k + 1)) (u (k + 1) • X (k + 1) - u k • X k) - u n * O3.pairing (A (n + 1)) (X n)

theorem V7.ResidualAlgebra.shifted_pairing_sum {d : ℕ} (n : ℕ) (dw : ScalarSeq) (A B : VectorSeq d) (hB0 : B 0 = 0) (hdwn : dw n = 0) : ∑ k ∈ Finset.range n, dw k * O3.pairing (A k) (B k) = ∑ k ∈ Finset.range n, dw (k + 1) * O3.pairing (A (k + 1)) (B (k + 1))

theorem V7.ResidualAlgebra.primal_abel {d : ℕ} (n : ℕ) (u dw : ScalarSeq) (A B X s : VectorSeq d) (hX0 : X 0 = 0) (hB0 : B 0 = 0) (hAn : A (n + 1) = 0) (hdwn : dw n = 0) (hs : ∀ k < n, s k - s (k + 1) = dw k • A k) (hx : ∀ k < n, u (k + 1) • X (k + 1) - u k • X k = dw (k + 1) • B (k + 1) + dw k • (B (k + 1) - B k)) : ∑ k ∈ Finset.range n, O3.pairing (s k - s (k + 1)) (B (k + 1)) - ∑ k ∈ Finset.range (n + 1), u k * O3.pairing (A k - A (k + 1)) (X k) = ∑ k ∈ Finset.range n, dw k * O3.pairing (A k - A (k + 1)) (B (k + 1) - B k)

theorem V7.ResidualAlgebra.inverse_map {d : ℕ} (n : ℕ) (u : ScalarSeq) (hu_pos : ∀ i ≤ n, 0 < u i) (C D : VectorSeq d) : BelowResidualMap n u (inverseA n u C) (fun (i : ℕ) => D (n - i)) C D

theorem V7.ResidualAlgebra.map_determined_inverse {d : ℕ} (n : ℕ) (u : ScalarSeq) (hu_pos : ∀ i ≤ n, 0 < u i) (A B C D : VectorSeq d) (hmap : BelowResidualMap n u A B C D) : SameOnHorizon n A (inverseA n u C) ∧ SameOnHorizon n B fun (i : ℕ) => D (n - i)

theorem V7.ResidualAlgebra.norm_block {d : ℕ} (p : ℝ) (hp : 1 < p) (n : ℕ) (u : ScalarSeq) (hu_pos : ∀ i ≤ n, 0 < u i) (A B C D : VectorSeq d) (hmap : BelowResidualMap n u A B C D) : ∑ k ∈ Finset.range n, u k / 2 * lpNorm (conjugateExponent p) (A k - A (k + 1)) ^ 2 = ∑ k ∈ Finset.range n, 1 / u (n - (k + 1)) / 2 * lpNorm (conjugateExponent p) (C k - C (k + 1)) ^ 2

noncomputable def V7.ResidualAlgebra.freeX {d : ℕ} (b : ScalarMatrix) (B : VectorSeq d) : VectorSeq d

The sequence starting at B 0 and subtracting the next weighted sum at each step.

Equations

• V7.ResidualAlgebra.freeX b B k = Nat.rec (B 0) (fun (j : ℕ) (previous : V7.Point d) => previous - V7.weightedSum (j + 2) (b (j + 1)) B) k

theorem V7.ResidualAlgebra.freeX_recurrence {d : ℕ} (n : ℕ) (b : ScalarMatrix) (B : VectorSeq d) : BelowXRecurrence n b B (freeX b B)

theorem V7.ResidualAlgebra.shifted_pairing_telescope {d : ℕ} (q : VectorSeq d) (g : Point d) (j m : ℕ) : ∑ l ∈ Finset.range m, O3.pairing g (q (j + l) - q (j + l + 1)) = O3.pairing g (q j - q (j + m))

theorem V7.ResidualAlgebra.dualP_pairing_path {d : ℕ} (n : ℕ) (hn : 1 ≤ n) (u : ScalarSeq) (G q : VectorSeq d) : ∑ k ∈ Finset.range n, O3.pairing (dualP n u G k) (q k - q (k + 1)) = ∑ k ∈ Finset.range n, 1 / u (n - (k + 1)) * O3.pairing (G (k + 1)) (q k - q (k + 1)) - ∑ j ∈ Finset.range n, (1 / u (n - (j + 1)) - 1 / u (n - j)) * O3.pairing (G j) (q j - q n)

theorem V7.ResidualAlgebra.function_value_cancel (n : ℕ) (w F : ScalarSeq) : w 0 * (F 0 - F n) - ∑ k ∈ Finset.range n, (w (k + 1) - w k) * (F n - F k) - ∑ k ∈ Finset.range n, w (k + 1) * (F k - F (k + 1)) = 0