Pointwise real inequalities for the commutator pairings

Abstract-real lemmas on Fin 2-indexed families, used to bound the first- and second-order commutator densities by the energy densities.

theorem AVenhance.Infra.FullTheorem.Separation.abs_triple_le_young {κ Lu m p q : ℝ} (hκ : 0 < κ) (hm : |m| ≤ Lu) : |m * p * q| ≤ κ / 4 * p ^ 2 + Lu ^ 2 / κ * q ^ 2

theorem AVenhance.Infra.FullTheorem.Separation.abs_triple_le_half {Lu m p q : ℝ} (hm : |m| ≤ Lu) : |m * p * q| ≤ Lu / 2 * (p ^ 2 + q ^ 2)

theorem AVenhance.Infra.FullTheorem.Separation.abs_quadForm_le {Lu : ℝ} (m : Fin 2 → Fin 2 → ℝ) (a : Fin 2 → ℝ) (hm : ∀ (i k : Fin 2), |m i k| ≤ Lu) : |∑ i : Fin 2, ∑ k : Fin 2, a i * (m i k * a k)| ≤ 2 * Lu * ∑ i : Fin 2, a i ^ 2

First-order quadratic form: |∑ a_i m_{ik} a_k| ≤ 2 Lu ∑ a_i².

theorem AVenhance.Infra.FullTheorem.Separation.abs_secondForm_le {κ Lu : ℝ} (hκ : 0 < κ) (m : Fin 2 → Fin 2 → ℝ) (p : Fin 2 → Fin 2 → Fin 2 → ℝ) (t2 : Fin 2 → Fin 2 → ℝ) (a : Fin 2 → ℝ) (hm : ∀ (i k : Fin 2), |m i k| ≤ Lu) : |∑ j : Fin 2, ∑ i : Fin 2, ∑ k : Fin 2, (-(m i k * p j j i * a k) + t2 j i * m j k * t2 i k)| ≤ κ / 2 * ∑ l : Fin 2, ∑ j : Fin 2, ∑ i : Fin 2, p l j i ^ 2 + 4 * (Lu ^ 2 / κ) * ∑ k : Fin 2, a k ^ 2 + 2 * Lu * ∑ j : Fin 2, ∑ i : Fin 2, t2 j i ^ 2

Second-order bound after the single integration by parts.