SymmetricBlockEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The numerical two-block estimate used in Lemma 5.2

theorem OAI.Ostmann.symmetric_block_energy line 11

Source documentation

A gap of 1/20 in the second diagonal block means that off-diagonal size r costs only 20*r^2 in the operator bound.

theorem symmetric_block_energy (s d r x y : ℝ) (hs : 0 ≤ s) (hd : 0 ≤ d)
    (hgap : d + 1 / 20 ≤ s) :
    (s * x + r * y) ^ 2 + (r * x + d * y) ^ 2 ≤
      (s + 20 * r ^ 2) ^ 2 * (x ^ 2 + y ^ 2) := by
…