ResidueBlockEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Two-by-two control of the actual finite residue blocks

theorem OAI.Ostmann.residue_block_energy line 13

Source documentation

Cauchy--Schwarz and the vector triangle inequality reduce the finite kernel block to its scalar matrix of bounds, without a dimension factor.

theorem residue_block_energy {p : ℕ} [NeZero p]
    (a : ℂ) (row col : ZMod p → ℂ) (C : (ZMod p → ℂ) → ZMod p → ℂ)
    (s d r : ℝ) (hs : 0 ≤ s) (hd : 0 ≤ d)
    (hgap : d + 1 / 20 ≤ s)
    (ha : ‖a‖ ≤ s) (hrow : residueVectorNorm row ≤ r)
    (hcol : residueVectorNorm col ≤ r)
    (hC : ∀ f, residueVectorNorm (C f) ≤ d * residueVectorNorm f)
    (z : ℂ) (f : ZMod p → ℂ) :
    ‖a * z + ∑ x, conj (row x) * f x‖ ^ 2 +
      residueVectorNorm (fun x => z * col x + C f x) ^ 2 ≤
      (s + 20 * r ^ 2) ^ 2 * (‖z‖ ^ 2 + residueVectorNorm f ^ 2) := by
…

Mentions: OAI.Ostmann.residueVectorNorm