Formalizing arXiv:2212.08956

theorem Superorthogonal.pointwise_estimate {ι : Type u_1} [Countable ι] {k : ℕ} (hk : 2 ≤ k) (a : Fin k → ι → ℂ) (ha : ∀ (i : Fin k), Summable fun (j : ι) => ‖a i j‖) : ‖Q a - ∏ i : Fin k, s (a i)‖ₑ ≤ (↑k.factorial - 1) * B hk a ^ 2 * max (A hk a) (B hk a) ^ (k - 2)

Proposition 2 from arXiv:2212.08956. This is the key pointwise estimate used in the proof of the main theorem.