ResidueProjectionSides.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative side blocks of the sparse residue projection

theorem OAI.Ostmann.centered_spectral_affine_energy line 11
theorem OAI.Ostmann.residue_uniform_coefficient_sq line 19
theorem OAI.Ostmann.residue_compl_coefficient_sq line 37

theorem OAI.Ostmann.residueProjection_side_energy line 57

Source documentation

Either uniform-support side of the projection is O(epsilon/sqrt(p)), in the squared-energy form used to bound the local block matrix.

theorem residueProjection_side_energy {p : ℕ} [NeZero p]
    (S E : Finset (ZMod p)) (hS : S.Nonempty) (hSp : S.card < p) (hE : 0 ∉ E)
    (hlo : (1 / 3 : ℝ) ≤ residueDensity S) (hhi : residueDensity S ≤ 2 / 3)
    (ε : ℝ)
    (herr : (∑ x, ‖normalizedResidueIndicator S x -
      finiteSpectralProjection E (normalizedResidueIndicator S) x‖ ^ 2) ≤ ε ^ 2 * p) :
    (∑ x, ‖centeredSupportProjection (Finset.univ \ S)
      (finiteSpectralProjection E (uniformResidueVector S)) x‖ ^ 2) ≤ 2 * ε ^ 2 / p ∧
    (∑ x, ‖centeredSupportProjection S
      (finiteSpectralProjection E (uniformResidueVector (Finset.univ \ S))) x‖ ^ 2) ≤ 2 * ε ^ 2 / p := by
…

Mentions: OAI.Ostmann.residueDensity, OAI.Ostmann.normalizedResidueIndicator, OAI.Ostmann.finiteSpectralProjection, OAI.Ostmann.centeredSupportProjection, OAI.Ostmann.uniformResidueVector